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!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.lang.ada
Subject: Re: {Pre,Post}conditions and side effects
Date: Tue, 12 May 2015 11:39:11 -0700
Organization: A noiseless patient Spider
Message-ID: <8738311vzk.fsf@jester.gateway.sonic.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>
	<migc9a$jp8$1@loke.gir.dk>
	<alpine.DEB.2.11.1505072052570.16448@debian>
	<mijen0$1hj$1@loke.gir.dk>
	<alpine.DEB.2.11.1505111113020.12062@debian>
	<mirjho$lqh$1@loke.gir.dk>
	<alpine.DEB.2.11.1505120951500.17718@debian>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: mx02.eternal-september.org;
 posting-host="631d4aa67102f56712a7d69e4aea5bbf";
	logging-data="15470"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX18/OjiGuDf9ESGfjtJiYuTa"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (gnu/linux)
Cancel-Lock: sha1:MkHLm3sri83rDGdwPvXCZnRN+gs=
	sha1:4X/kiXt2BZcXEQEanV1OKXdCcmg=
Xref: news.eternal-september.org comp.lang.ada:25845
Date: 2015-05-12T11:39:11-07:00
List-Id: <comp.lang.ada>

Stefan.Lucks@uni-weimar.de writes:
> Either I write it as a second-class precondition in the form of a
> comment, or as a fist-class precondition using the "pre" attribute, or
> something similar ("unchecked_pre" or whatever). I'd prefer the
> second, because the compiler will tell me if my precondition is
> syntactically correct.

I'd say the first-class precondition (if executable) is also better
because even if a runtime check (say for an array being sorted) is too
expensive to use in a deployed application, you can still enable the
check during testing and pay the runtime cost, possibly finding some
bugs that way.

>> I disagree, actually. I think any useful postcondition has to be
>> reasonably executable. Else there is no difference from a comment,

Don't you want {pre,post}conditions to be able to quantify over infinite
ranges, and therefore not always be executable?  For example, consider a
compiler optimization pass expressed as a function that takes a code
fragment and returns a new code fragment: the postcondition is that both
fragments have the same semantics, which means for all inputs, both
fragments compute the same result.  That postcondition is not executable
but it is (example: CompCert) potentially provable.  So wanting to state
and prove it is a legitimate desire.

> I don't care much about the syntax, some "unchecked_pre",
> "unchecked_post" attributes would be perfectly fine.

You could have a static precondition that accepts proof by assertion,
like in Coq where you can say "admitted".

>> Like everyone, I want it all, for free, right now. :-) Only Ada comes
>> close, and I just want to make it closer.
> Violent agreement, again!

Do you use other verification systems like Coq?  Are the ones used with
Ada comparable at all?