OCL 2.5 RTF Avatar
  1. OMG Issue

OCL25 — Satisfaction of Operation Specifications (2)

  • Key: OCL25-146
  • Legacy Issue Number: 6549
  • Status: open  
  • Source: Anonymous
  • 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
    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:
    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.

  • Reported: OCL 2.0b2 — Tue, 11 Nov 2003 05:00 GMT
  • Updated: Thu, 8 Oct 2015 14:12 GMT