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=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no 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: Georg Bauhaus <bauhaus@futureapps.invalid>
Newsgroups: comp.lang.ada
Subject: Re: {Pre,Post}conditions and side effects
Date: Thu, 07 May 2015 23:29:03 +0200
Organization: A noiseless patient Spider
Message-ID: <miglcs$6gp$1@dont-email.me>
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>
Reply-To: nonlegitur@futureapps.de
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Thu, 7 May 2015 21:27:56 +0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="7af0ebc34d55cbc312a7591190144f98";
	logging-data="6681"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX18bdmZbsNeSvaui8r0kMEJkIVIquh2WUro="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9;
 rv:31.0) Gecko/20100101 Thunderbird/31.6.0
In-Reply-To: <migc9a$jp8$1@loke.gir.dk>
Cancel-Lock: sha1:+GDNzYaYpT73gCKvNz/P3n7t/o4=
Xref: news.eternal-september.org comp.lang.ada:25768
Date: 2015-05-07T23:29:03+02:00
List-Id: <comp.lang.ada>

On 07.05.15 20:52, Randy Brukardt wrote:
> If the compiler fails to optimize the check away, your program is wrong in
> some sense, and you should have gotten an error or warning (depending on the
> compiler mode and exception contracts) to that effect.

With respect, this attitude towards manipulating a program's
meaning during translation makes a compiler assume responsibility
where it really is the programmers' responsibilities (as per
contract), as expressed in clauses like Pre and Post.

Why then is the *program* somehow buggy, as you say,
because some compiler's optimizers can't follow the math that
has been done already, and expressed as a truth in Pre?

As Stefan Lucks explains in his reply, why would a compiler
override what the programmer has stated as a proven truth?
That's not Ada.  That's more like a compiler getting in the way.

I think that

   Pre'__unchecked__ =>

might be in order, then, with the understanding that it's not
real, but conveying the idea.

Thus, if the compiler puts checks where the programmer has
shown they are superfluous, that's not Ada. At least it used
not to be like that.

  "Design your program by obeying our optimizer, be defensive,
   don't bother with logic and proofs! We'll take care.
  "Doing so prevents bugs (if possible)."

That's not Ada. That's another sales strategy.

Are we supposed to forget such contracts entirely because this kind
of formally proven programming is, as you say, not meant by Ada's
new "contracts"?