From: NCOHEN@IBM.COM ("Norman H. Cohen")
Subject: Pre-condition vs. Post-condition
Date: 18 Mar 91 15:47:34 GMT [thread overview]
Message-ID: <9103181658.AA10945@ajpo.sei.cmu.edu> (raw)
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.
next reply other threads:[~1991-03-18 15:47 UTC|newest]
Thread overview: 29+ messages / expand[flat|nested] mbox.gz Atom feed top
1991-03-18 15:47 "Norman H. Cohen" [this message]
-- strict thread matches above, loose matches on Subject: below --
1991-03-24 21:23 Pre-condition vs. Post-condition stt
1991-03-25 16:00 ` Arthur Evans
1991-03-25 17:05 ` Michael Feldman
1991-03-26 4:31 ` Jim Showalter
1991-03-26 10:21 ` Richard A. O'Keefe
1991-03-26 16:44 ` Michael Feldman
1991-03-26 22:03 ` Richard A. O'Keefe
1991-03-26 23:36 ` Michael Feldman
1991-03-27 21:34 ` Jim Showalter
1991-03-28 2:54 ` Michael Feldman
1991-03-29 3:28 ` Jim Showalter
1991-03-27 3:12 ` Jim Showalter
1991-03-15 3:57 Chris M. Little
1991-03-15 19:07 ` Michael Feldman
1991-03-17 12:26 ` George C. Harrison, Norfolk State University
1991-03-18 15:04 ` Joe Hollingsworth
1991-03-18 19:51 ` Marlene M. Eckert
1991-03-19 19:07 ` Michael Feldman
1991-03-21 3:01 ` Jim Showalter
1991-03-21 18:40 ` Michael Feldman
1991-03-19 20:38 ` Charles H. Sampson
1991-03-21 3:06 ` Jim Showalter
1991-03-19 21:07 ` Jim Showalter
1991-03-19 7:38 ` Jim Showalter
1991-03-19 14:46 ` Joe Hollingsworth
1991-03-21 2:46 ` Jim Showalter
1991-03-22 15:18 ` Brad Balfour
1991-03-19 18:17 ` Mike Gilbert
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox