Re: Pre-condition vs Post-condition

[nwebre@polyslo.CalPoly.EDU (Neil Webre)]

When the questions of exceptions and pre- and post-conditions came up,
I answered by mail to the poster. Since there have been some replies
via news, I am posting my reply which follows:

To: cml8@robin.cs.uofs.edu
Subject: Re: Pre-condition vs. Post-condition
Organization: Cal Poly State Univ,CSC Dept,San Luis Obispo,CA 93407

   If a pre-condition is not met, the result of execution is undefined
   (maybe unspecified is a better word). In the case of exceptions, if
   you write the fact that an exception will occur in certain cases,
   in your postcondition, then it seems to me that you have written
   a specification of results if the "error" condition happens. Therefore
   the error condition was not a precondition since your algorithm
   has a well defined and specified result for that case. 

   I am in the process of writing a textbook. What we have done is to
   write the specs of procedures and functions in the following form:

   procedure kaboom(...);
   -- precondition : ....
   -- postcondition : ....
   -- exceptions : ...

   Properly speaking, the exceptions clause is part of the postcondition.
   However, since exceptions are a standard way of handling "errors"
   in Ada, we broke them out into a separate clause.
   Preconditions are reserved to screen out conditions that truly have no
   defined results. It is the job of the client to assure that the
   precondition is met prior to execution of the procedure or function.