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: border2.nntp.dca1.giganews.com!nntp.giganews.com!newspeer1.nac.net!newsfeed.xs4all.nl!newsfeed2a.news.xs4all.nl!xs4all!feeder.erje.net!1.eu.feeder.erje.net!news-2.dfn.de!news.dfn.de!news.uni-weimar.de!medsec1.medien.uni-weimar.de!lucks From: Stefan.Lucks@uni-weimar.de Newsgroups: comp.lang.ada Subject: Re: {Pre,Post}conditions and side effects Date: Tue, 12 May 2015 10:37:01 +0200 Organization: Bauhaus-Universitaet Weimar 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: medsec1.medien.uni-weimar.de Mime-Version: 1.0 Content-Type: MULTIPART/MIXED; BOUNDARY="8323329-1906213066-1431419822=:17718" X-Trace: pinkpiglet.scc.uni-weimar.de 1431420222 17325 141.54.178.228 (12 May 2015 08:43:42 GMT) X-Complaints-To: news@pinkpiglet.scc.uni-weimar.de NNTP-Posting-Date: Tue, 12 May 2015 08:43:42 +0000 (UTC) X-X-Sender: lucks@debian In-Reply-To: User-Agent: Alpine 2.11 (DEB 23 2013-08-11) Xref: number.nntp.giganews.com comp.lang.ada:193142 Date: 2015-05-12T10:37:01+02:00 List-Id: This message is in MIME format. The first part should be readable text, while the remaining parts are likely unreadable without MIME-aware tools. --8323329-1906213066-1431419822=:17718 Content-Type: TEXT/PLAIN; charset=ISO-8859-15; format=flowed Content-Transfer-Encoding: QUOTED-PRINTABLE On Mon, 11 May 2015, Randy Brukardt wrote: > wrote in message > news:alpine.DEB.2.11.1505111113020.12062@debian... >> So the above specifies properly what I want to have. But this is also >> terribly slow. [...] >> I.e., this is a valid specification, but a useless test. > > Correct. If it hurts, don't write that. :-) Firstly, have to write that. Somehow! Otherwise, my documentation would be= =20 seriously incomplete. Either I write it as a second-class precondition in the form of a comment,= =20 or as a fist-class precondition using the "pre" attribute, or something=20 similar ("unchecked_pre" or whatever). I'd prefer the second, because the= =20 compiler will tell me if my precondition is syntactically correct. Yes, I claim that Ada12-style pre- and postconditions are helpful, even if= =20 they are neither verified statically nor verified at run time. I have seen too many informal specifications that didn't fit. As an=20 example, consider function Divide (Dividend, Divisor: Num) return Num; -- Precondition: Y /=3D To_Num(0). This example is simple and harmless. One can easily guess that at some=20 point of time, the parameter "Y" has been renamed to "Divisor", but the=20 comment has not been updated. Similar cases can be a lot more complicated.= =20 Having a precondition parsed by the compiler is a big win, even if the=20 compiler does nothing beyond parsing with the precondition. Secondly, the compiler or prover may need need such "believe me, this is=20 true" properties to verify other properties it *can* verify. > I don't begin to believe that all program properties can be proved. Ah! Some of your previous posts left me with the impression that you where= =20 proposing an "either prove everything, or don't prove anything" approach. >> In practice, people usually call the Miller_Rabin primality test: >> >> function MR_Is_Prime(N: Num; Repetitions: Natural :=3D 500) >> return Boolean with >> post =3D> Miller_Rabin_Prime'Result =3D Is_Prime(N); >> >> As a specification, the postcondition is useful. > > I disagree, actually. I think any useful postcondition has to be reasonab= ly > executable. Else there is no difference from a comment, See above. > and you would be better served using a comment as won't throw out all of= =20 > the easy checks with this silly one. Firstly, see my above writing on comments versus compiler-parsed=20 specifications. Secondly, this property may actually be relevant to statically verify=20 other program properties, under the assumption that the "believe me" claim= =20 is true. > No, by my logic, *writing* a test that you can't actually execute is bad,= as > it tells no one anything useful. I think, this is the core point of our disagreement -- or your=20 misunderstanding, as I would put it. ;-) You can check a precondition or a postcondition or an invariant for=20 testing purposes. But neither *is* a test, and either can have other=20 purposes than just testing. > I don't think anyone would ever want a system that *required* proving > everything. The important thing IMHO is that you can find out what wasn'= t > proven so you can determine whether to fix it (via additional > specifications) or whether to ignore it (the obvious case being that the > unproven case is on a non-executable path). We are in violent agreement here. But this is precisely the reason why I am trying to advertise a=20 fine-grained way to separate between things proven at compile time or=20 checked at run time (and maybe checked at testing versus also checked in=20 production code) from things claimed. I don't care much about the syntax,= =20 some "unchecked_pre", "unchecked_post" attributes would be perfectly fine. > I want to bring this tool to people that would not go out of their way to > use it. (I.e., me. :-) That means it has to be in the compiler so that th= ey > get the benefits automatically, because there is no way I'm going out and > buying (plus learning) a separate tool to do those things. I suspect that > many (perhaps most) programmers are like me. 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! Stefan ------ I love the taste of Cryptanalysis in the morning! ------ uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-lucks --Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universit=E4t Weimar, Germany-- --8323329-1906213066-1431419822=:17718--