Legacy Issue Number: 6550
Author: Hubert Baumeister (firstname.lastname@example.org),
Rolf Hennicker (email@example.com),
Alexander Knapp (firstname.lastname@example.org)
Description: Change Definition A.34 to allow the precondition to be weakened
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 possibility 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:
DEFINITION A.34 (SATISFACTION OF OPERATION SPECIFICATIONS)
An 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.
Reported: OCL 2.0b2 — Tue, 11 Nov 2003 05:00 GMT
Updated: Thu, 8 Oct 2015 14:12 GMT