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!newsfeed.fsmpi.rwth-aachen.de!newsfeed.straub-nv.de!news-1.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: Mon, 18 May 2015 14:10:08 +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> <87oali5i6n.fsf@adaheads.sparre-andersen.dk> NNTP-Posting-Host: medsec1.medien.uni-weimar.de Mime-Version: 1.0 Content-Type: MULTIPART/MIXED; BOUNDARY="8323329-315433173-1431951009=:4352" X-Trace: pinkpiglet.scc.uni-weimar.de 1431951421 12679 141.54.178.228 (18 May 2015 12:17:01 GMT) X-Complaints-To: news@pinkpiglet.scc.uni-weimar.de NNTP-Posting-Date: Mon, 18 May 2015 12:17:01 +0000 (UTC) X-X-Sender: lucks@debian In-Reply-To: <87oali5i6n.fsf@adaheads.sparre-andersen.dk> User-Agent: Alpine 2.11 (DEB 23 2013-08-11) Xref: news.eternal-september.org comp.lang.ada:25904 Date: 2015-05-18T14:10:08+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-315433173-1431951009=:4352 Content-Type: TEXT/PLAIN; charset=ISO-8859-15; format=flowed Content-Transfer-Encoding: QUOTED-PRINTABLE On Mon, 18 May 2015, Jacob Sparre Andersen wrote: > Stefan.Lucks@uni-weimar.de wrote: > >> Thirdly, even if it would be way too expensive to check this >> specification at run time, it may be possible to verify it statically >> at run time. But I can only find that out by writing the specification >> and then running my tool (the compiler or whatever). Again, it would >> be a terrible idea for the compiler to insert expensive checks just >> because the theorem prover failed to prove the condition. > > Why? Wouldn't it be better to have the check enabled by default, and > only disable it once profiling has shown that it is prohibitively > expensive? Well, as a very simmple example, consider this: =09(for all I in 2 .. N-1 =3D> (N mod I) /=3D 0) You don't need a profiler to figure out that this is prohibitively slow=20 for largish N, do you? > I am aware that we currently don't have as fine-grained control of=20 > assertions as that would require to work well, but I assume that this is= =20 > something that can be discussed with the ARG and the compiler vendors. This is precisely my point! 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-315433173-1431951009=:4352--