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: buffer2.nntp.dca1.giganews.com!border2.nntp.dca1.giganews.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!goblin3!goblin.stu.neva.ru!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: Thu, 7 May 2015 13:52:25 -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> <871tj9dp5b.fsf@theworld.com> NNTP-Posting-Host: rrsoftware.com X-Trace: loke.gir.dk 1431024746 20264 24.196.82.226 (7 May 2015 18:52:26 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Thu, 7 May 2015 18:52:26 +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: number.nntp.giganews.com comp.lang.ada:193068 Date: 2015-05-07T13:52:25-05:00 List-Id: wrote in message news:alpine.DEB.2.11.1505071103310.14859@debian... ... >> I don't believe that checks in Ada (of any kind) should ever be turned >> off. > >Here, I heavily disagree. Often, checking relevant properties is much to >expensive to perform the checks them in production code. > >A simple example is binary search over a sorted array. The precondition >requires the array to be sorted. If the compiler succeeds in optimising >the test away, it is equivalent to a static program verifier proving the >precondition holds when the binary search is called. Exactly! That's the entire idea; the compiler *should* be doing these optimizations, indeed one major branch of static program verification comes from enhancing compiler optimizer technology (CodePeer is an example of that). I think that technology should simply have stayed in the compiler. >If the compiler fails to optimise the check away, the execution time goes >up >from logarithmic to linear. If you can live with that, you don't need >binary search! If the compiler fails to optimize the check away, your program is wrong in some sense, and you should have gotten an error or warning (depending on the compiler mode and exception contracts) to that effect. You ought to fix your program (probably by adding an appropriate predicate) so that the check *can* be eliminated (or pushed to somewhere where the cost is irrelevant). >Turning off the checks just hides the problem. There is no value to that, >IMHO. >The semantic of a plain precondition is essentially: > > * If I a True, the postcondition will hold. > Never call the subprogram if I am false!!! > Otherwise, the subprogram might do anything. "anything" => erroneous. >This is a precondition in the "Design by Contract" sense. Ada 2012 does not have these sorts of preconditions. (We've discussed it numerous times.) The theory is that adding a precondition NEVER makes a program less safe. Ergo, preconditions can be ignored, but violating an ignored precondition is not erroneous in the sense that violating a suppressed check is. There's a reason that we didn't call this "suppressing" preconditions! Thus, there is no circumstance where the "subprogram might do anything". I've thought a bit about having some additional Assertion_Policy "suppress" that would allow the semantics you describe above, but we haven't talked about that at the language level. > A typical example for this would be "the array is sorted" when calling > binary search. If you call a binary search routine with an unsorted array, > you will likely get false results. And you deserve the blame! That's not "anything". That's a well-defined (but useless) result. Be careful about your terminology! > The semantic of a precondition with something like "else raise > This_Exception" is > > * If I am True, the postcondition will hold > when the subprogram terminates. > If I am False, the subprogram will not do anything, > except for raising This_Exception. This the meaning of all Ada 2012 preconditions. "This_Exception" just defaults to "Assertion_Error". Anyway, the Assertion_Policy can be changed locally, and the policy in effect at the point of the declaration determines what policy is used for calls. Plus the policy can be set separately for different kinds of assertions. Thus, you can get the effect you want with the existing policies, so long as you don't try to write two different kinds of assertions on the same subprogram. Note that there is some debate about the value of the fine-grained policy setting, it's unclear that GNAT implements it correctly. If some of their customers showed concern about the correct implementation of those rules, that certainly would change. Randy.