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: border1.nntp.dca1.giganews.com!nntp.giganews.com!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!feeder.erje.net!1.eu.feeder.erje.net!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, 8 May 2015 17:52:15 -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 1431125536 1587 24.196.82.226 (8 May 2015 22:52:16 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Fri, 8 May 2015 22:52:16 +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:193083 Date: 2015-05-08T17:52:15-05:00 List-Id: wrote in message news:alpine.DEB.2.11.1505072052570.16448@debian... > On Thu, 7 May 2015, Randy Brukardt wrote: ... >> 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). > >Why do I need to fix the program, if I know it is correct? Just because >the compiler isn't good enough at theorem proving? Because there is no such thing. There is no real way for you to know that it is correct. I have plenty of examples of supposedly correct programs that turned out to have serious bugs. The only way for a program to be "correct" is for it to be proven that way by the compiler. (And even then, the compiler algorithm might have problems.) Because if any other tool does it, the compiler might disagree (because either tool has bugs), and thus the actual code might still in fact be incorrect. >>> Turning off the checks just hides the problem. > >*IF* there is a problem at all. See above. There is *always* a problem; the only question is whether you are willing to defend against it or not. For example, in this "Is_Sorted" example, if you are assuming that some object is sorted, then it should have a predicate to that effect. In such a case, the compiler would be able to eliminate all of the precondition checks on calls, the only time the predicate would be checked is when the object is initially created (which certainly should not be on any critical path), or if it is modified by a routine that doesn't include Is_Sorted in its postcondition (which is clearly the source of potential bugs as well). In the absence of those sorts of things, you are just hiding potential flaws. Randy.