OCL25 — Exception of strict evaluation (=)

Author: Thomas Baar (thomas.baar@epfl.ch)
Description: contradiction for evaluation of navigation expression
Rationale: Suppose to have two classes A, B and an association with multiplicity
0..1 on B
between them.
The invariant context
A inv: self.b = self.b
is evaluated for an instance of A not having an associated instance of B to
i) true, when the expression self.b has the type Set(B), because self.b is evaluated to emptyset and emptyset = emptyset is evaluated to true
ii) undef, when the expression self.b has the type B, because self.b is evaluated to undef and undef = undef is evaluated to undef thanks to strict evaluation of '='
This is a contradiction since the expression self.b can be both of type set(B) and B!
The examples also shows, that x = x is not a tautology unlike in almost all other logics including classical predicates logic. This is especially confusing because OCL claims to be based on classical predical logic!