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=-0.8 required=5.0 tests=BAYES_00,INVALID_DATE
	autolearn=no autolearn_force=no version=3.4.4
Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!pacific.mps.ohio-state.edu!linac,att!ucbvax!IBM.COM!NCOHEN
From: NCOHEN@IBM.COM ("Norman H. Cohen")
Newsgroups: comp.lang.ada
Subject: Pre-condition vs. Post-condition
Message-ID: <9103181658.AA10945@ajpo.sei.cmu.edu>
Date: 18 Mar 91 15:47:34 GMT
Sender: daemon@ucbvax.BERKELEY.EDU
Organization: The Internet
List-Id: <comp.lang.ada>

For exceptions raised by predefined basic operations, it is generally
impossible to write a precondition guaranteeing that the exception WILL
be raised.*  In such cases it is clearly appropriate to incorporate in
the precondition sufficient conditions to guarantee that no predefined
exception** will be raised.

For programmer-defined exceptions raised under predictable circumstances,
it is reasonable to incorporate in formal specifications the conditions
under which a subprogram completes normally, the circumstances under
which such exceptions are raised, and the effect on the program state
in each case.  The approach I've adopted in developing proof rules for
Ada is to assume a separate precondition/postcondition pair for each such
case:

   function CAPITAL (COUNTRY: STRING) return STRING;

   -- Let Country_Map be the mapping { "USA" -> "Washington",
   -- "Mongolia" -> "Ulan Bator", ... }.

   -- Precondition for normal completion:
   --    COUNTRY in domain Country_Map
   -- Postcondition for normal completion:
   --    function_result = Country_Map(COUNTRY)
   --
   -- Precondition for completion with COUNTRY_ERROR raised:
   --    COUNTRY not in domain Country_Map
   -- Postcondition for completion with COUNTRY_ERROR raised:
   --    TRUE  [no change of state]

It is certainly possible to incorporate all this in a postcondition:

   -- Precondition: TRUE
   -- Postcondition:
   --      (    COUNTRY in domain Country_Map
   --       and exception_raised=none
   --       and function_result=Country_Map(COUNTRY))
   --   or (    COUNTRY not in domain Country_Map
   --       and exception_raised=COUNTRY_ERROR)

However, I find this presentation more obscure for the human reader.
The first approach more naturally decomposes the behavior of the function
into separate cases of interest.  For mechanical program analysis (e.g.
for the generation of verification conditions) the first approach is also
clearly preferable, because it allows proof rules to refer to the
exception status at the end of a statement.  For example, if Pre(S,P,E)
is the precondition for statement S to complete with postcondition P and
exception status E, then the proof rule for a sequence of two statements
is:

  (1) Pre(S1;S2, P, normal) = Pre(S1, Pre(S2, P, normal), normal)

  (2) If E is the raising of some exception,
         Pre(S1;S2, P, E) =
            Pre(S1, P, E) or Pre(S1, Pre(S2, P, E), normal)

(In the exception-raising case, case (2), the left operand of "or"
corresponds to the case where S1 raises the exception and the right
operand corresponds to the case where S1 completes normally and then
S2 raises the exception.)

----------

*-Among the reasons for this are the liberty provided by RM 4.5.7(7) to
  ignore real overflow, by RM 11.6(6) to use a wider type for computation
  of intermediate results, and by RM 11.6(7) to delete an operation whose
  "only possible effect is to propagate a predefined exception."  Also
  there are cases in which DIFFERENT exceptions may be raised for
  implementation-dependent reasons, such as the order in which
  subexpressions are evaluated or an implementation's adherence to
  nonbinding interpretation AI-00387, which recommends the raising of
  CONSTRAINT_ERROR wherever the  RM calls for NUMERIC_ERROR to be raised.

**-This really means "no predefined exception other than STORAGE_ERROR
   and IO_EXCEPTIONS.DEVICE_ERROR."  These two exceptions occur for
   reasons that cannot be expressed in terms of the abstract program
   state.  The raising of one of these exceptions is best viewed as an
   unpredictable event that causes the underlying abstract machine to
   break.  It is possible to factor the possibility of such unpredictable
   events into a formal proof of program behavior, but a simpler and
   equally useful approach is to reason about program behavior under the
   assumption that such events will not occur and to prominently
   document the fact that this assumption has been made.