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!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!feeder.erje.net!1.eu.feeder.erje.net!gandalf.srv.welterde.de!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail
From: Jacob Sparre Andersen <sparre@nbi.dk>
Newsgroups: comp.lang.ada
Subject: Re: {Pre,Post}conditions and side effects
Date: Mon, 18 May 2015 11:49:36 +0200
Organization: Jacob Sparre Andersen Research & Innovation
Message-ID: <87oali5i6n.fsf@adaheads.sparre-andersen.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>
 <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>
 <alpine.DEB.2.11.1505121319240.25376@debian>
NNTP-Posting-Host: 109.57.170.100.mobile.3.dk
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
X-Trace: loke.gir.dk 1431942578 15494 109.57.170.100 (18 May 2015 09:49:38
 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Mon, 18 May 2015 09:49:38 +0000 (UTC)
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.4 (gnu/linux)
Cancel-Lock: sha1:oGPBNaQ87G7fterKweHsuCe2JvI=
Xref: number.nntp.giganews.com comp.lang.ada:193209
Date: 2015-05-18T11:49:36+02:00
List-Id: <comp.lang.ada>

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?

I am aware that we currently don't have as fine-grained control of
assertions as that would require to work well, but I assume that this is
something that can be discussed with the ARG and the compiler vendors.

Greetings,

Jacob
-- 
There really was only one way to make a person unlearn something ...