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: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: {Pre,Post}conditions and side effects Date: Thu, 7 May 2015 21:55:23 +0200 Organization: cbb software GmbH Message-ID: <12gipcoheoucz.15ckvrgi11h3a.dlg@40tude.net> 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> <121ytg16vbxsk$.18dxo1h7daxty.dlg@40tude.net> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: evoS9sCOdnHjo0GRLLMU1Q.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Xref: news.eternal-september.org comp.lang.ada:25766 Date: 2015-05-07T21:55:23+02:00 List-Id: On Thu, 7 May 2015 14:01:34 -0500, Randy Brukardt wrote: > wrote in message > news:alpine.DEB.2.11.1505071909280.16448@debian... > ... >> One property of a proper precondition (or postcondition or ...) is that >> disabling the check does not change the functional behaviour of correct >> programs. > > Sure, but this is irrelevant. There are no "correct" programs (in all > possible senses). How do you know that you have a correct program? You don't need to know it, to have it existing. (If a tree falls in a forest and no one is around to hear it, does it make a sound?) A correct program exists in the sense that there exist a combination of characters that represents this program. Whether anybody is capable to write this combination down is no matter. Moreover, the program exists in strictly constructive terms. You can enumerate all possible programs and some them will be correct. Even correctness proof is constructive because the number of states of any program is finite. So you can always find a correct program given enough time. > If you > use some prover program, it too may have bugs. Yes, but every programmer deals with partially correct program, he knows which parts of the program are correct, which parts are known to be incorrect and which parts are neither. > Or there might be bad data (cosmic rays?) Bad data do not make program incorrect. (If "bad" means "inputs I forgot to think about" that is lousy problem analysis) > Or the specification might be incomplete. Oh, but that does not make its implementation incorrect. Incompleteness of specification is not the program's property. (Be careful what you wish for, it might come true) > Consider the latest > Dreamliner issue; that probably wouldn't have been caught by a prover simply > because no one would have included an appropriate assertion. It is an infinite recursion, which is why it is meaningless to define correctness, as you seem do, as some absolute. There cannot be such thing. The program is correct when it agrees with the specified behavior. Period. Whether the specification is itself correct, or if behavior is desired, legal, moral, safe, haram etc is outside the scope. > Ergo, I don't believe that "proper preconditions" really exist. In the sense you try to put into it, yes, they do not exist. They do not because you could not formalize it. There is no formal framework where you could consistently formulate that idea. It is inherently inconsistent. > And in the > rare cases that they do (perhaps because of an immediately preceding > postcondition), a compiler would have eliminated them anyway, so you're not > paying anything for the supposed runtime check. (After all, Ada compilers > have been aggressively removing checks since 1983; that's nothing new to an > Ada compiler writer.) The point is that these are fundamentally different things. Correctness is outside. Behavior is inside. You cannot convert one into another keeping the program. Checks elimination is strictly about behavior, merely a program transformation, optimization. Correctness evaluation is not behavior, it is not the program at all. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de