Issue 6549: Satisfaction of Operation Specifications (2) (ocl2-rtf) Source: (, ) Nature: Uncategorized Issue Severity: Summary: Author: Achim D. Brucker (brucker@inf.ethz.ch), Burkhart Wolff (wolff@informatik.uni-freiburg.de) Description: Change Definition A.34 to allow the precondition to be weakened Rationale: 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 specification S if the restriction of S to the domain of R (denoted S|_dom(R)) is included in R, i.e. S|_dom(R) \subseteq R. This is equivalent to: \forall x, y. x:dom(R) & (x,y):S --> (x,y):R. In particular, S may be a program, i.e. a computation function in the sense of total correctness. Resolution: Revised Text: Actions taken: November 11, 2003: received issue Discussion: Deferred for timing reasons End of Annotations:===== atisfaction of Operation Specifications (2) Author: Achim D. Brucker (brucker@inf.ethz.ch), Burkhart Wolff (wolff@informatik.uni-freiburg.de) Description: Change Definition A.34 to allow the precondition to be weakened Rationale: 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 specification S if the restriction of S to the domain of R (denoted S|_dom(R)) is included in R, i.e. S|_dom(R) \subseteq R. This is equivalent to: \forall x, y. x:dom(R) & (x,y):S --> (x,y):R. In particular, S may be a program, i.e. a computation function in the sense of total correctness.