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
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.223.40 with SMTP id qr8mr2500020pbc.0.1340349822825;
        Fri, 22 Jun 2012 00:23:42 -0700 (PDT)
Path: 
 l9ni6043pbj.0!nntp.google.com!news1.google.com!goblin2!goblin.stu.neva.ru!aioe.org!.POSTED!not-for-mail
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Newsgroups: comp.lang.ada
Subject: Re: about the new Ada 2012 pre/post conditions
Date: Fri, 22 Jun 2012 09:23:44 +0200
Organization: cbb software GmbH
Message-ID: <1jvy3elqtnd1j.1sjbk32evhp1f$.dlg@40tude.net>
References: <jrsjr7$uuo$1@speranza.aioe.org>
 <1hgo6aks03zy.by4pq4xbjsgf$.dlg@40tude.net> <jrsmfh$6fq$1@speranza.aioe.org>
 <npdjip6ohqlt$.1x6bxc9jsaago$.dlg@40tude.net> <js00co$clj$1@munin.nbi.dk>
Reply-To: mailbox@dmitry-kazakov.de
NNTP-Posting-Host: FbOMkhMtVLVmu7IwBnt1tw.user.speranza.aioe.org
Mime-Version: 1.0
X-Complaints-To: abuse@aioe.org
User-Agent: 40tude_Dialog/2.0.15.1
X-Notice: Filtered by postfilter v. 0.8.2
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
Date: 2012-06-22T09:23:44+02:00
List-Id: <comp.lang.ada>

On Thu, 21 Jun 2012 15:32:21 -0500, Randy Brukardt wrote:

> "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.

If you take a stance on #1, then checking stack full is no more evaluation
of the precondition, which does not depend on the stack state anymore, as
it of course should be. So the "true" precondition is just: True. Then why
on earth anybody would denote it as:

   Pre => not Is_Full (S)

And implementations leaking into declarations is certainly a very bad idea.
An even worse idea is to slice implementations into parts of unclear
purpose. Instead of one package body, the maintainer will have to inspect
the body, and so-.called pre-/post-conditions slices.

Neither #1 nor #2 is defendable.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de