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

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 ...

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.