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.228.227 with SMTP id sl3mr9048095pbc.5.1340223405447;
        Wed, 20 Jun 2012 13:16:45 -0700 (PDT)
Path: 
 l9ni88pbj.0!nntp.google.com!news1.google.com!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
From: "Jeffrey R. Carter" <ggsub@pragmada.co.cc>
Newsgroups: comp.lang.ada
Subject: Re: about the new Ada 2012 pre/post conditions
Date: Wed, 20 Jun 2012 13:16:44 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: <4f0d55a9-83e1-44fe-8943-0c73a34a594d@googlegroups.com>
References: <jrsjr7$uuo$1@speranza.aioe.org>
NNTP-Posting-Host: 184.20.201.198
Mime-Version: 1.0
X-Trace: posting.google.com 1340223405 7493 127.0.0.1 (20 Jun 2012 20:16:45
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Wed, 20 Jun 2012 20:16:45 +0000 (UTC)
Cc: nma@12000.org
In-Reply-To: <jrsjr7$uuo$1@speranza.aioe.org>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=184.20.201.198;
 posting-account=uInPWgoAAAD9VvUJDc0jNwDhBg_137JZ
User-Agent: G2/1.0
Content-Type: text/plain; charset=ISO-8859-1
Date: 2012-06-20T13:16:44-07:00
List-Id: <comp.lang.ada>

On Wednesday, June 20, 2012 6:39:50 AM UTC-7, Nasser M. Abbasi wrote:
> 
> throw an exception for this).

In Ada, one raises an exception.

> 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;

Decades of experience show that it will usually be used as:

Dummy := Push (S, Element);
etc...

This is part of the reason exceptions exist.

If Push raises an exception, rather than returning an error code/flag, then the caller either has to handle that exception, or write

if Is_Full (S) then
   -- stack is full, do something else
else
   etc...
end if;

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

Any checks worth having during testing are worth having after testing. This is why you want a way to ensure they're always done.

For your own use, the answer is to keep the checks on. The real problem is for reusable code. The caller may not be you, and so may have turned off the checks, so such code should not have the precondition, but should have the hard-coded checks.

--
Jeff Carter
jrcarter commercial-at-sign acm (period | full stop) org