OCL 2.5 RTF Avatar
  1. OMG Issue

OCL25 — Satisfaction of Operation Specifications

  • Key: OCL25-44
  • Legacy Issue Number: 6548
  • Status: open  
  • Source: Anonymous
  • Summary:

    Author: Hubert Baumeister (baumeist@informatik.uni-muenchen.de),
    Rolf Hennicker (hennicke@informatik.uni-muenchen.de),
    Alexander Knapp (knapp@informatik.uni-muenchen.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 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.
    Comment by Daniel Jackson (dnj@mit.edu)
    i'd be very wary of linking any particular notion of refinement to a modelling language. different circumstances might need different notions, and there's no reason that the language should be tied to one.
    i wonder, for example, if you've considered the difference between preconditions as disclaimers and preconditions as firing conditions.
    even for the standard notion of preconditions as disclaimers, your particular definition seems too narrow to me. requiring the program to be a function will rule out many reasonable implementations that are non-deterministic – hash tables, for example.

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