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=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,b78c363353551702
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.68.219.170 with SMTP id pp10mr919463pbc.1.1340310747444;
        Thu, 21 Jun 2012 13:32:27 -0700 (PDT)
MIME-Version: 1.0
Path: 
 l9ni4398pbj.0!nntp.google.com!news1.google.com!goblin3!goblin.stu.neva.ru!gandalf.srv.welterde.de!news.jacob-sparre.dk!munin.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: about the new Ada 2012 pre/post conditions
Date: Thu, 21 Jun 2012 15:32:21 -0500
Organization: Jacob Sparre Andersen Research & Innovation
Message-ID: <js00co$clj$1@munin.nbi.dk>
References: <jrsjr7$uuo$1@speranza.aioe.org>
 <1hgo6aks03zy.by4pq4xbjsgf$.dlg@40tude.net> <jrsmfh$6fq$1@speranza.aioe.org>
 <npdjip6ohqlt$.1x6bxc9jsaago$.dlg@40tude.net>
NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net
X-Trace: munin.nbi.dk 1340310744 12979 69.95.181.76 (21 Jun 2012 20:32:24 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Thu, 21 Jun 2012 20:32:24 +0000 (UTC)
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2900.5931
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157
X-RFC2646: Format=Flowed; Original
Date: 2012-06-21T15:32:21-05:00
List-Id: <comp.lang.ada>

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:npdjip6ohqlt$.1x6bxc9jsaago$.dlg@40tude.net...
...
> This is what constitutes the core inconsistency about dynamic
> pre-/post-conditions. If they #1 implement behavior (e.g the stack 
> contract
> to raise something when full), then they cannot be suppressed and do not
> describe the contract. If they do describe the contract #2, they may not
> implement it and thus shall have no run-time effect.

You're right, but I don't see any inconsistency. They are clearly #1, and 
that includes all of the existing Ada checks as well. And you are right, it 
*never* makes logical sense in Ada to suppress or ignore anything. They 
*are* part of the contract. The old saw about wearing seatbelts in the 
garage and taking them off when you leave is totally in operation here.

The *only* reason to suppress or ignore checks is for performance reasons, 
and those are clearly outside of any program logic. Moreover, this should be 
very rare, since this should only happen in the very narrow band when the 
program is too slow with the checks on and fast enough with them off (most 
programs will be fast enough always, and most of the rest will be too slow 
always).

I know Bob and some others disagree with this, and they're just outright 
wrong. (In part because I don't believe in requiring any checks as part of 
the contract that are too expensive to leave on always. The sorts of 
assertions that you might want to suppress because they are too expensive 
should *never* be part of the contract and I think they should be 
categorized differently from those that are part of the contract. But I 
found no traction for that idea, unfortunately.)

                                             Randy.