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=2.0 required=5.0 tests=BAYES_00,FORGED_MUA_MOZILLA,
	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.196.232 with SMTP id ip8mr22769196pbc.6.1340202294055;
        Wed, 20 Jun 2012 07:24:54 -0700 (PDT)
Path: 
 l9ni72622pbj.0!nntp.google.com!news2.google.com!goblin3!goblin.stu.neva.ru!usenet.pasdenom.info!aioe.org!.POSTED!not-for-mail
From: "Nasser M. Abbasi" <nma@12000.org>
Newsgroups: comp.lang.ada
Subject: Re: about the new Ada 2012 pre/post conditions
Date: Wed, 20 Jun 2012 09:24:48 -0500
Organization: Aioe.org NNTP Server
Message-ID: <jrsmfh$6fq$1@speranza.aioe.org>
References: <jrsjr7$uuo$1@speranza.aioe.org>
 <1hgo6aks03zy.by4pq4xbjsgf$.dlg@40tude.net>
Reply-To: nma@12000.org
NNTP-Posting-Host: KdJUrTuvv3Zv/s8pPxNluw.user.speranza.aioe.org
Mime-Version: 1.0
X-Complaints-To: abuse@aioe.org
User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64;
 rv:13.0) Gecko/20120614 Thunderbird/13.0.1
X-Notice: Filtered by postfilter v. 0.8.2
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Date: 2012-06-20T09:24:48-05:00
List-Id: <comp.lang.ada>

On 6/20/2012 9:13 AM, Dmitry A. Kazakov wrote:
> On Wed, 20 Jun 2012 08:39:50 -0500, Nasser M. Abbasi wrote:
>
> [...]
>> But, and here is the problem, when I turn off assertions, I am
>> now left with the push() function with no check at all for
>> the case of the stack is full.
>>
>> So, what is one to do? use pre/post AND also add
>> an extra check for full stack in the code as before?
>> does not make sense.
>
> 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.
>

That is what I was thinking. So, I guess I am not alone.

>> They seem to definitely be something good to have.
>
> Not everything is what it seems...
>

Since I myself have no experience in contract programming,
I have to wait and see how they work out. I assume they
must be good thing to have, to make the program more
robust,but if used correctly.

I do  not want to end up using them as substitute for
actual logic that I would use in the code itself.

When exceptions were new thing, many started using them in
place of the old fashioned if/then to check for
error in logic and just return an error code. Everyone
started just throwing exceptions everywhere, i.e. misused
them. I can see this might happen with pre/post as they
are new thing.

Will have to wait for gnat Ada 2012 to come out and start
using them to find out.

--Nasser