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: border2.nntp.dca1.giganews.com!nntp.giganews.com!newspeer1.nac.net!newsfeed.xs4all.nl!newsfeed1a.news.xs4all.nl!xs4all!feeds.phibee-telecom.net!eternal-september.org!feeder.eternal-september.org!mx02.eternal-september.org!.POSTED!not-for-mail From: "G.B." Newsgroups: comp.lang.ada Subject: Re: {Pre,Post}conditions and side effects Date: Fri, 24 Apr 2015 14:10:19 +0200 Organization: A noiseless patient Spider Message-ID: References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com> <0a718b39-ebd3-4ab5-912e-f1229679dacc@googlegroups.com> <9ee5e186-5aaa-4d07-9490-0f9fdbb5ca18@googlegroups.com> <87tww5296f.fsf@adaheads.sparre-andersen.dk> Reply-To: nonlegitur@futureapps.de Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 7bit Injection-Date: Fri, 24 Apr 2015 12:09:16 +0000 (UTC) Injection-Info: mx02.eternal-september.org; posting-host="b96887e80893c84a90c3007226ca0d1c"; logging-data="26278"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18inhRRsN6XPql8vFQ9URV8ESu2dfnMasw=" User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:31.0) Gecko/20100101 Thunderbird/31.6.0 In-Reply-To: <87tww5296f.fsf@adaheads.sparre-andersen.dk> Cancel-Lock: sha1:xYkOHcznq+eh6F+Se0Qwqq3jD3s= Xref: number.nntp.giganews.com comp.lang.ada:192898 Date: 2015-04-24T14:10:19+02:00 List-Id: On 24.04.15 10:59, Jacob Sparre Andersen wrote: > But I dislike banning "essential program logic" in assertions, as any > assertion is program logic. And if it isn't essential, why should it be > there? This definition involving "essential" does not reflect "contract" properly, IMHO. And it is fallacious in that it fails to reflect the particulars that make assertions, as in "assertion as per contract", different from just program logic. To see this, I think it is helpful to free oneself of the limitations of looking at assertions from just a programmer's point of view. Assertions (of the contract) should never, ever be understood to be consequences of the program text with or without the assertions, insofar as they are agreed upon by humans to be true about the program to be, its intent in particular. They cover a program that may even have to be written yet. They do share some of the properties of agreements manifest in specifications. For contracts' clauses, possibly supported by assertions as part of source text, there isn't even a conceptual necessity to have proper assertions tested in the very same environment as the program proper: a copy will do in many cases of proper assertions, as these are pure Boolean functions. The fact that assertions can be expressed in Ada is purely accidental; SPARK shows that a different language can be used, and may even be more expressive. Comments do count, too, such as RM statements about O(op). The latter can be understood as a part of contract between any user of Ada and the implementer of Ada. An improper assertion (if I may call it that for reasons of delineation) will modify that part of program's data which is covered by the contract, data to be handled solely by the program which would yield the same effects that are stated in the contract, with or without assertion checking. So, using improper assertions, you'd be making a mess, even though results might come out right (only deferring proof obligations having to do with the improper assertion). OTOH, whenever testing an assertion requires computation, it is essential to keep its doings separate from what the program needs to compute to fulfill the contract. So, the idea of considering assertions of contracts (as opposed to plain old debugging asserts) from the viewpoint of their implementation is misleading. Illustration: Company X agrees this is in a contract: If, before calling Binary_Search, input is sorted, then the result of calling Binary_Search will be ... That's a statement that can be made part of a contract, and it may be formally reflected in Ada aspects, if possible. It is expressing the idea that Source is sorted. Last but not least, a precondition should never be anything but an assumption. As not checking it at run-time is a valid way of handling preconditions, the outcome of not tesing should still not create havoc; so, the caller needs to make sure that assertion of the contract is always true, and never depend on how it is tested, or on that it is tested.