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=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Newsgroups: comp.lang.ada
Subject: Re: Tests in a software release
Date: Fri, 3 Nov 2017 09:16:52 +0100
Organization: Aioe.org NNTP Server
Message-ID: <oth8lk$1q81$1@gioia.aioe.org>
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>
 <oth5k4$eih$1@dont-email.me>
NNTP-Posting-Host: lKHBldubgAWx1EqbQpQ5LQ.user.gioia.aioe.org
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
X-Complaints-To: abuse@aioe.org
User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:52.0) Gecko/20100101
 Thunderbird/52.4.0
X-Notice: Filtered by postfilter v. 0.8.2
Content-Language: en-US
Xref: news.eternal-september.org comp.lang.ada:48713
Date: 2017-11-03T09:16:52+01:00
List-Id: <comp.lang.ada>

On 03/11/2017 08:24, G.B. wrote:
> On 31.10.17 09:32, Dmitry A. Kazakov wrote:
> 
>> 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(*).

Yes, as with any bug, the programmer has an undeniable right to 
introduce it.

>> This is called optimization.
> 
> Optimization means that a compiler translates
> source text using different algorithms.

No.

Optimization is varying the implementation within the braces of the 
contract in order to achieve certain goal, e.g. to reduce memory usage.

> Contracts between clients and suppliers do not
> need a compiler.

Removing checks is not related to enforcement of contracts. It is tuning 
the implementation. So long the contract is not violated by that, it is 
all OK. If it gets violation it is a bug. No rocket science here.

>>  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.

Has it been explained that some hardware has instruction ADD? Does it 
mean that "+" has no implementation? Whichever way calls to the caller 
are translated is irrelevant. Again, all effect is the implementation. 
There is no anything else.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de