OCL 2.0 FTF Issues: Satisfaction of Operation Specifications

Date view Thread view Subject view Author view Attachment view

From: Hubert Baumeister (baumeist@informatik.uni-muenchen.de)
Date: Thu 30 Oct 2003 - 17:36:14 GMT

Dear all,

please find attached an issue for the OCL 2.0 finalization process.


Dr. Hubert Baumeister, Institut fr Informatik, Universitt Mnchen
phone (x49-89)2180-9375  * fax -9175

Satisfaction of Operation Specifications

Author: Hubert Baumeister, Rolf Hennicker, Alexander Knapp {baumeist,hennicke,knapp}@informatik.uni-muenchen.de

Description: Change Definition A.34 to allow the precondition to be


It is commonly accepted that a program S satisfying an operation
specification may weaken the precondition. This corresponds to
Bertrand Meyer's view of software specifications as contracts between
clients of a program and program provider. This is in accordance with
the explanation following Def. A.34: "In other words, the program S
accepts each environment satisfying the precondition as input and
produces an environment that satisfies the postcondition." This
sentence admits the possiblity that S may be defined for environments
not satisfying the precondition.

However Def. A.34 requires S to be defined exactly on the environments
for which the precondition holds. Therefore, we propose to replace
Def. A.34 by:

operation specification with pre- and postconditions is satisfied by a
program S in the sense of total correctness if the computation of S is
a function fS such that the restriction of fS to the domain of R is a
total function fS|_dom(R): dom(R) -> im(R) and graph(fS|_dom(R))
\subseteq R.

Date view Thread view Subject view Author view Attachment view