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!mx02.eternal-september.org!feeder.eternal-september.org!gandalf.srv.welterde.de!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: {Pre,Post}conditions and side effects Date: Fri, 24 Apr 2015 18:46:27 -0500 Organization: Jacob Sparre Andersen Research & Innovation 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> <87oamdlhd3.fsf@adaheads.sparre-andersen.dk> NNTP-Posting-Host: rrsoftware.com X-Trace: loke.gir.dk 1429919187 24815 24.196.82.226 (24 Apr 2015 23:46:27 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Fri, 24 Apr 2015 23:46:27 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Xref: news.eternal-september.org comp.lang.ada:25606 Date: 2015-04-24T18:46:27-05:00 List-Id: "Jacob Sparre Andersen" wrote in message news:87oamdlhd3.fsf@adaheads.sparre-andersen.dk... > "G.B." wrote: > > [...] > >> 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. > > Taking that view, there isn't any point combining the contract notation > of Ada 2012 and SPARK 2014, as it would prevent you from writing a > single source text which was valid for both languages. > > SPARK would complain about your in-subprogram check (mirroring the > precondition), as raising an exception is illegal in SPARK (and dead > code probably is as well). Besides, Ada 2012 has a mechanism to ensure that preconditions are in fact evaluated; that exists for this very reason. If you have a local Assertion_Policy of Check, that applies to the declarations and the precondition ought to be evaluated no matter what policy is in effect at the point of the call. (Whether GNAT actually gets this right is unknown.) Otherwise, one could not "hoist" the various rules for I/O, containers, and the like into preconditions. Which would seem like madness. Certainly checking the same thing twice (which is what would happen if you put the condition into the precondition and then manually checked it a second time in the body) is madness. There is a camp that thinks that ignoring contract assertions is very similar to suppressing checks, and anything that happens after doing that is effectively erroneous. (That's NOT the wording in the Standard.) For that group, hoisting things into preconditions is fine. Otherwise, one needs to take steps to ensure that they're evaluated. Randy.