From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: "G.B." <bauhaus@notmyhomepage.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Tests in a software release
Date: Fri, 3 Nov 2017 08:24:57 +0100
Organization: A noiseless patient Spider
Message-ID: <oth5k4$eih$1@dont-email.me>
References: <osqoph$1ves$1@gioia.aioe.org> <oss2c3$1p2m$1@gioia.aioe.org>
 <osvsjs$t4b$1@dont-email.me> <osvvds$s97$1@gioia.aioe.org>
 <ot19fo$7mi$2@dont-email.me> <ot1bvm$ub7$1@gioia.aioe.org>
 <ot82v3$h2c$1@dont-email.me> <ot83l0$1rb1$1@gioia.aioe.org>
 <ot981s$7m5$1@dont-email.me> <ot9cfr$1k6s$1@gioia.aioe.org>
Reply-To: nonlegitur@notmyhomepage.de
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Fri, 3 Nov 2017 07:24:52 -0000 (UTC)
Injection-Info: reader02.eternal-september.org;
 posting-host="034133ee984e6593545e7701ab721e77";
	logging-data="14929"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX19RWWKThSeaDmpFdt6skR93DGveNA6j4qE="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.12; rv:52.0)
 Gecko/20100101 Thunderbird/52.4.0
In-Reply-To: <ot9cfr$1k6s$1@gioia.aioe.org>
Content-Language: en-US
Cancel-Lock: sha1:8asTerLiQCKjPzYWT0nJFOryPv0=
Xref: news.eternal-september.org comp.lang.ada:48712
Date: 2017-11-03T08:24:57+01:00
List-Id: <comp.lang.ada>

On 31.10.17 09:32, Dmitry A. Kazakov wrote:

> Implementation of bounds check = implementation of contract on bounds check.

To declare that the different names of different
things shall mean the same is one way of cutting
the Gordian knot.


> Checks can be removed only when statically proven not to fail.

Programmers may remove checks whenever they think
they should. No fancy proof is required(*).

> This is called optimization.

Optimization means that a compiler translates
source text using different algorithms.

Contracts between clients and suppliers do not
need a compiler. They do not require source text.
They need a lawyer. No, I am not joking.

>  The point is that any run-time check is behavior of the callee and cannot be argued something belonging to the caller or to whatever else.

Checks have actually belonged to something else,
on useful hardware, as has been explained in the past.

But your description of typical translations of
Ada programs that carry checks is about today's checks
in GNAT output. It's not even about contracts, which
are a purely legal thing between parties.

__
(*) It has been proven is that programs proven correct
will of necessity be rare or impractical.