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