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" Newsgroups: comp.lang.ada Subject: Re: Tests in a software release Date: Tue, 31 Oct 2017 09:32:58 +0100 Organization: Aioe.org NNTP Server Message-ID: References: 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:48684 Date: 2017-10-31T09:32:58+01:00 List-Id: On 2017-10-31 08:17, G.B. wrote: > On 30.10.17 21:56, Dmitry A. Kazakov wrote: >> On 2017-10-30 21:44, G. B. wrote: >>> Dmitry A. Kazakov 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. > > So, Ada programs will check theirs checks? Implementation of bounds check = implementation of contract on bounds check. It is called tautology. > Expectations can be stated in comments, > or be part of accompanying documentation and still > be part of a contract. > >> There is nothing that is not behavior. > > Checking is behavior. However, let SPARK check conditions > of a contract, and let the result be Truth. Then they > have been checked before the program even runs, and > turning *off* Ada checks is, therefore, justified. That is what I said. Checks can be removed only when statically proven not to fail. This is called optimization. If in the IF-statement the condition is proven statically true, the ELSE-part can be removed. Just same. Ada could have a pragma to remove all ELSE parts of all IF-statements. Would anybody argue for that? (:-)) > Disabling Ada checks means to rely on this contract. It relays on proven properties of the program. >> There is nothing that may not fall under the contract. > > There are very many things, even in a program, > that do exist, exhibit behavior, but are not > part of any known, non-fictional contract, such as > the transitive closure of an unspeakable hypothesis. Sure. Contract only limits behavior it does not specify it. 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. Body may be not all behavior, e.g. if the check happens on the caller's side of the call. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de