OCL 2.4 RTF Avatar
  1. OMG Issue

OCL24 — non(not(X)) should be X

  • Key: OCL24-5
  • Legacy Issue Number: 17531
  • Status: closed  
  • Source: Model Driven Solutions ( Dr. Edward Willink)
  • Summary:

    In http://www.linkedin.com/redirect?url=http%3A%2F%2Fwww%2Ebrucker%2Ech%2Fprojects%2Fhol-ocl%2FFeatherweight-OCL%2Foutline%2Epdf&urlhash=vacm&_t=tracking_anet Burkhart Wol ff argues that lopgical consistency requires that not(not(X)) is X.

    OCL 2.3.x does not satisfy this for 'null'.

    Similary null and true = null not invalid ...

  • Reported: OCL 2.3.1 — Fri, 27 Jul 2012 04:00 GMT
  • Disposition: Resolved — OCL 2.4
  • Disposition Summary:

    Issue 14197 for OCL 2.3 rationalized the vague equivalences between undefined and null/invalid.
    In OCL 2.0, it was left for the implementer to determine how "not null" and "not invalid" were computed given the specification that "not undefined = undefined".
    In OCL 2.3, we have clarity: "not null = invalid" and "not invalid = invalid". However this leads to the identified inconsistency that "not not X = X" is not true for all X (not not null = invalid).
    The clarification of "not undefined" should have partitioned the two cases for "not undefined = undefined" so that "not null = null" and "not invalid = invalid"
    Similarly other logical operations involving null but not invalid should yield null rather than invalid results. "null and true = null", "null or false = null", "null xor false = null".
    We should extend this to the forAll and exists iterations that are defined as iterated and/or. Making the exists/forAll returns clear highlights that many iterator returns are only partially specified; these need expanding.
    Introduction of null highlights a redundancy in the non-standard implies postcondition: (not self) or (self and b) rather than the standard (not self) or b. The standard gives the consistent result "null implies true = true" whereas the current non-standard postcondition gives null. The non-standard postcondition is already wrong for invalid.
    The If expression specification words omit consideration of a non-valid condition; a null or invalid condition is of course invalid.
    For arithmetic operations there is an apparently free choice between two alternate consistent logics in which "1 + null = null" or "1 + null = invalid".
    "1 + null = null" is plausible if "null" denotes "don't know"; an object/value that exists but with unspecified value.
    "1 + null = invalid" is plausible if "null" denotes "missing"; the absence of an object/value.
    However UML provides the interpretation of "null" as "missing". UML-alignment of OCL therefore requires OCL to take the "1 + null = invalid" alternative, which is what the Issue 14197 clarification specified. So no change required for arithmetic operations.

  • Updated: Fri, 6 Mar 2015 20:57 GMT