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!newsfeed0.kamp.net!newsfeed.kamp.net!newsfeed.freenet.ag!feeder.erje.net!1.eu.feeder.erje.net!weretis.net!feeder4.news.weretis.net!gandalf.srv.welterde.de!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: {Pre,Post}conditions and side effects
Date: Thu, 7 May 2015 14:01:34 -0500
Organization: Jacob Sparre Andersen Research & Innovation
Message-ID: <migcqf$k21$1@loke.gir.dk>
References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com>
 <AnYlw.957256$Rp.242412@fx23.iad>
 <0a718b39-ebd3-4ab5-912e-f1229679dacc@googlegroups.com>
 <wccoaqucn51.fsf@shell01.TheWorld.com>
 <9ee5e186-5aaa-4d07-9490-0f9fdbb5ca18@googlegroups.com>
 <alpine.CYG.2.11.1412231747100.4196@WIL414CHAPIN.vtc.vsc.edu>
 <wccegrpq2om.fsf@shell01.TheWorld.com>
 <87tww5296f.fsf@adaheads.sparre-andersen.dk> <871tj9dp5b.fsf@theworld.com>
 <ce4af31e-d491-479f-a5b3-0b3eedea2a68@googlegroups.com>
 <midvq5$2u3$1@loke.gir.dk> <alpine.DEB.2.11.1505071103310.14859@debian>
 <121ytg16vbxsk$.18dxo1h7daxty.dlg@40tude.net>
 <alpine.DEB.2.11.1505071909280.16448@debian>
NNTP-Posting-Host: rrsoftware.com
X-Trace: loke.gir.dk 1431025295 20545 24.196.82.226 (7 May 2015 19:01:35 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Thu, 7 May 2015 19:01:35 +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:25762
Date: 2015-05-07T14:01:34-05:00
List-Id: <comp.lang.ada>

<Stefan.Lucks@uni-weimar.de> 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? If you 
use some prover program, it too may have bugs. Or there might be bad data 
(cosmic rays?) Or the specification might be incomplete. 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.

Ergo, I don't believe that "proper preconditions" really exist. 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.)

                                            Randy.