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!news.swapon.de!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail
From: Niklas Holsti <niklas.holsti@tidorum.invalid>
Newsgroups: comp.lang.ada
Subject: Re: {Pre,Post}conditions and side effects
Date: Thu, 07 May 2015 22:29:00 +0300
Organization: Tidorum Ltd
Message-ID: <cr1snsF60hoU1@mid.individual.net>
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> <migcqf$k21$1@loke.gir.dk>
Mime-Version: 1.0
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Transfer-Encoding: 7bit
X-Trace: individual.net Nvrl/lV2zA/ig4AqGDn8jA8BX6yYv72AsEvQLcgwrBg3uwB1vU
Cancel-Lock: sha1:yqA8QBrcwM6OF10yBGt9+wCnneA=
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8;
 rv:31.0) Gecko/20100101 Thunderbird/31.6.0
In-Reply-To: <migcqf$k21$1@loke.gir.dk>
Xref: news.eternal-september.org comp.lang.ada:25764
Date: 2015-05-07T22:29:00+03:00
List-Id: <comp.lang.ada>

On 15-05-07 22:01 , Randy Brukardt wrote:
> <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?)

Those are practical problems, not problems of principle. If you would 
take the same attitude to mathematics, you would claim that there are no 
correct theorems. So I disagree with you.

> 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.

If it was an overflow problem (and not wrap-around of a modular type) 
CodePeer would probably have complained that it could not prove absence 
of overflow. That is, many failures result from violations of general 
assertions that one does not have to write explicitly.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .