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,start
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 pp10mr22683457pbc.1.1340199595533;
        Wed, 20 Jun 2012 06:39:55 -0700 (PDT)
Path: 
 l9ni72506pbj.0!nntp.google.com!news2.google.com!goblin2!goblin.stu.neva.ru!aioe.org!.POSTED!not-for-mail
From: "Nasser M. Abbasi" <nma@12000.org>
Newsgroups: comp.lang.ada
Subject: about the new Ada 2012 pre/post conditions
Date: Wed, 20 Jun 2012 08:39:50 -0500
Organization: Aioe.org NNTP Server
Message-ID: <jrsjr7$uuo$1@speranza.aioe.org>
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-20T08:39:50-05:00
List-Id: <comp.lang.ada>

I never used contract programming, but looking at

http://www.adacore.com/uploads/technical-papers/Ada2012_Rationale_Chp1_contracts_and_aspects.pdf

I can see already that they will be useful to have.

But since I did not use them before, I am just wondering
what rules of thumbs are there for using them, as I can
see already I might end up not using them correctly.

Here is a simple example of what I mean:

-----------------------------
pragma Assertion_Policy(Check);

procedure Push(S: in out Stack; X: in Item)
   with
     Pre => not Is_Full(S),
     Post => not is Empty(S);
   is
     ....
end Push;
---------------------

One thing to notice right away, is that the pre/post checks
can be disabled or enabled by the pragma.

In the old days, (i.e. now with no pre/post), I would code
the above, by adding an explicit check myself at the
start of the Push() to check if the stack is full, and
if so, I would return an error code (I do not think I'll
throw an exception for this).

Hence Push() will be a function that is called like this

   status = push(S,element)
   if status = success  -- Ok, was pushed ok
      etc....
   else
      -- stack is full, do something else
   end;

But now with pre there, this means the program will
throw an assertion if the stack is full. Ok, may be
this indicate logic error by the user of the stack,
but may be not.

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.

Keep the pre/post on all the time? do not make sense,
they are meant for testing time only, right?

They seem to definitely be something good to have.
Just need to figure the right way to use them (just like
with exceptions). May be more examples using contract
programming with Ada 2012 will be good to see.

--Nasser