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: Mon, 30 Oct 2017 21:56:02 +0100
Organization: Aioe.org NNTP Server
Message-ID: <ot83l0$1rb1$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>
NNTP-Posting-Host: MajGvm9MbNtGBKE7r8NgYA.user.gioia.aioe.org
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
X-Complaints-To: abuse@aioe.org
User-Agent: Mozilla/5.0 (Windows NT 10.0; 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:48677
Date: 2017-10-30T21:56:02+01:00
List-Id: <comp.lang.ada>

On 2017-10-30 21:44, G. B. wrote:
> Dmitry A. Kazakov <mailbox@dmitry-kazakov.de> wrote:
>> On 2017-10-28 08:53, G.B. wrote:
>>> On 27.10.17 20:54, Dmitry A. Kazakov wrote:
>>>> The contract requires Constraint_Error propagation.
>>>
>>> Checks require Constraint_Error propagation.
>>
>> Checks ensure Constraint_Error as a part of implementation.
> 
> Implementation of checks, not of contracts.

This is exactly same.

Note that all run-time effect of the syntactic language construct named 
"call of a subroutine X" is the implementation of X.

There is nothing that is not implementation of. There is nothing that is 
not behavior. There is nothing that may not fall under the contract. It 
is irrelevant if and which parts of the implementation are inlined and 
which are re-entrant. It is irrelevant how they are ordered to the 
machine instruction "CALL", "JSB", whatever. It is irrelevant how they 
are associated with the stack frame if any. All this is the implementation.

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