Re: Pre-condition vs. Post-condition

[holly@python.cis.ohio-state.edu (Joe Hollingsworth)]

In article <2865@sparko.gwu.edu> mfeldman@seas.gwu.edu () writes:
>>Say we have a function CAPITAL which, given a country's name, returns its
>>capital city.  If the given country does not exist, an exception COUNTRY_ERROR
>>is raised.  Should the given country's presence be listed as a pre-condition
>>for this function, or should its absense (it doesn't exist) and the raising
>>of COUNTRY_ERROR be listed as a post-condition?
>>
>>I brought this question up in class today and the outcome was a split decision.
>>I think exception raising and/or handling is as valid an outcome of a function
>>or procedure as any other outcome, so I'm tempted to cover the issue in the
>>post-condition comment.  My opponents believe that a function's pre-conditions
>>should be the conditions under which it would complete "normally", that is,
>>without any exceptions being raised.
>
>Hmmm. Interesting question. I have always taught - and thought of - pre-
>conditions as a set of "contract terms" which, if they are met, would
>obligate the function writer to write code that delivers the right results.
>From a verification point of view, I think you are correct that raising
>an exception is a _valid_ outcome of the function, and so the function has
>to be tested with cases of "bad" input to check that the exception indeed
>is raised under those conditions. If the pre- and post-conditions are used
>to drive tests (or formal verification), I agree that _explicit_ exception-
>raising by the function is a post-condition matter: it needs to be tested.
....stuff deleted.....
>Mike Feldman

I'm glad you raised the point of formal verification.  I'd like to point
out how the use of exception handling complicates verification (be it
formal or informal).

Examine the following possible implementation for Pop (popping a stack).

procedure pop(s: stack)
-- this pop doesn't return the top of the stack, just discards it.
begin
   if(not empty(s)) then
      -- pop the stack
   else
      raise underflow
end pop;

The point here is that there are 2 distinct paths through the procedure
which will have to be verified with respect to the pre and post conditions
(pre and post conditions not given).  The two paths are easy to spot.

Now look at another implementation of Pop based on Booch's stack package:

procedure pop(s: stack)
-- this pop doesn't return the top of the stack, just discards it.
begin
   stack.top := stack.top - 1;
   exception
      when Constraint_Error => raise underflow
end pop;

Here there are also two paths through the procedure, but it's not so
obvious to the reader (verifier) how the path through the exception
handler gets taken.  The verifier has to realize that the variable
stack.top has been defined as Natural and that a Constraint_Error
will be raised by the run time system when trying to set it to -1.

Since the control flow in this example is not explicit, let's call
it implicit.  I believe that verifying (formally or informally) code
written using implicit control flow is harder than code using explicit
control flow.  If this point is valid, one might then believe that 
code written using implicit control flow stands a better chance of NOT
being verified correctly, especially if it is informally verified.  What's
more I also believe that using exceptions leads one toward this kind
of programming (i.e. depending on implicit control flow).

I'm a follower of many of the rules found in Kernighan & Plauger's
"The Elements of Programming Style", two of those rules reads as follows:

"Write clearly - don't be too clever."
"Say what you mean, simply and directly."

I believe that exception handling leads one to writing programs that are not
as clear as they could be (see the second example above which doesn't
say what it means simply and directly).

With respect to verification, if the verifier is mechanical, then it probably
doesn't matter if the code uses implicit or explicit control, the
verifier will be able to handle it.  But, when was the last time any of
us used a mechanical verifier on our Ada programs?  Chances are
the verifier is the person writing the code, and that person is doing it
informally.  All the more reason to "Write clearly..." and "Say what you
mean, simply and directly."

The above arguments lead me to believe that exception handling should be used
only sparingly (if at all)!

(Mike, you wanted to get a debate going on this?  The above opinions
should help!)

Joe 

Joe Hollingsworth  Computer and Information Science @ OSU
holly@cis.ohio-state.edu