Path: utzoo!utgpu!watserv1!watmath!att!occrsh!uokmax!apple!usc!zaphod.mps.ohio-state.edu!swrinde!ucsd!hub.ucsb.edu!eiffel!bertrand
From: bertrand@eiffel.UUCP (Bertrand Meyer)
Newsgroups: comp.lang.eiffel
Subject: Re: Exceptions and Assertions
Message-ID: <404@eiffel.UUCP>
Date: 4 Sep 90 19:17:57 GMT
References: <723@tetrauk.UUCP>
Organization: Interactive Software Engineering, Santa Barbara CA
Lines: 56

This is not an extensive answer, but a reaction to one specific
point of Rick Jones's posting. He notes that:

> A feature may be written with a precondition such as:
>  
> /1/        doit (param: CLASS) is
>                 require
>                      not param.Void
>                 do
>                      ...
> 
> A client of this feature should therefore test the proposed argument
> before calling doit, as in: (...)
>  
> /2/         if not arg.Void then c.doit (arg) end
> 
> (...)
> 
> This of course begs the question: why not leave the precondition checks
> activeand save the redundancy of checking for the same thing twice in
> different ways and different places? A precondition violation will
> effectively raise an exception in the same place.

A precondition is a requirement on clients, telling them what
they must achieve before a call if they want the call to execute
as advertized (i.e. ensure the postcondition on exit). 

A good client will ``do its homework'' before every call, that is
to say, ensure the precondition. But there is more than one
method to do this. /2/ is one such method; it is nice because of its
universality - it will work regardless of the precondition
(although it leaves open the question of what to do when the
precondition is not satisfied; in practice, the ``if'' will
usually need to have an ``else'', not shown in the above version).
But in many cases you will enforce the precondition by means other
than testing for it. In simple (but frequent) cases the precondition
is simply enforced by the context; a trivial example is the call

	p (x ^ 2 + y ^ 2)

where the precondition of p (a: REAL) is a >= 0.

To take a more common example, assume `l' is a list and you call `l.r',
where the precondition of `r' is that l be a non-empty list.
Assume further that the instruction executed just before the call
was was `l.insert (...)', where `insert' guarantees (as
part of its postcondition) that the list will be non-empty.
Then you do not need to use form /2/. One may go further and
state that you should not.

This is only a step towards answering Mr. Jones's broader question.
Should we tend towards a situation where precondition checking
will always be on, even in a released software product?
-- 
-- Bertrand Meyer
bertrand@eiffel.com