RE: Invariants evaluating to undefined



RE: Invariants evaluating to undefined

From: Waldin, Earl ^lt;Earl.Waldin@paranor.ch>
Date: Mon 03 Apr 2006 - 18:44:01 BST
Message-ID: <1DE41A26EA92CA4FB831A9449AB0841E5DBE78@srv-par2.paranor.ch>
What a coincidence! I also was looking at this just a few days ago and
had considered opening up a thread on this. After much digging through
the spec I came to the same conclusion. It appears that the new
interpretation of "x.y -> isEmpty()" is not consistent with the old
version of OCL. I also looked at the finalization task force's report
(OMG document ptc/2005-06-05), issue 5972, "Can collections  contain
void/undefined objects". This is the issue cited in sections 11.2.3 and
11.2.4 which specify OclVoid and OclInvalid. Here is the committe's
resolution:

The notion of OclUndefined is splitted (sic) into two notions:
LiteralNull and OclInvalid to distinguish between the situations where
we have an absence of value (LiteralNull) and an invalid events (such as
division of zero). Collection can contain null values but cannot contain
Oclinvalid values. 

Apart from making more flexible the usage of OCL as a query language,
this resolution aligns OCL with UML2 in which the "absence of value" is
already modeled by the notion of null literal which is not considered
being an invalid value.

Note that the finalized version did not introduce a corresponding
literal "null".  So you can't yet write "self.wife = null". You have to
write "self.wife.oclIsUndefined()". However, even that is underspecified
because x.a.oclIsUndefined() means that x.a is either null or invalid
(see definition of oclIsUndefined in section 11.2.5). So, as far as I
can tell you would have to write something like
    self.wife.oclIsUndefined() and not self.wife.oclIsInvalid()
Given that the abstract syntax contains a class NullLiteralExp, one
would expect to find a corresponding literal "null" in the concrete
syntax. But this won't help you anyway, as I'll describe later w.r.t.
the meaning of equality.

What is most disturbing however, is that "The type OclVoid conforms to
all other types (see section 11.2.3), which means that the value null
conforms to all types. To me this means that every defined type, e.g.,
Integer, implicitly contains the null value. That is, any property,
regardless of its type, may have the value null. Consequently, the
association-end property "wife" described in D H. Akehurst's email could
have multiplicity 1 and still have the value null. In previous versions
of the specification a multiplicity of 1 for a property meant that the
property always had a defined (i.e., non-null) value.

OCL appears to be explicity introducing pointers as values and the type
of every property is implicitly a pointer type. This may be consistent
with OO programming languages, but it is less useful as a logic. It may
be perfectly reasonable to have a null value in the semantics, but not
in the language itself.

And even more disturbing is the meaning of equality. '=' is an operation
of type OclAny. And the syntax "x = y" is shorthand for "x.=(y)". So
"x.=" is a property call and, according to the specification, "Any
property call applied on null results in OclInvalid, except for the
operation oclIsUndefined()" (section 11.2.3). So, if "self.wife" really
were null, then "self.wife = anything" would result in invalid. And in
any case applying '=' to null (i.e., x.=(null)) would also result in
invalid. So the expression "self.wife=null" is meaningless. In addition,
this treatment of equality makes it difficult to assert that two
properties are either both undefined or have the same value (e.g., x.a =
y.b), something that would be natural to say if both of the properties
'a' and 'b' had multiplicity 0..1. This occurs quite commonly in the
case where x is a new object (i.e. x.oclIsNew() ) and I want to assert
that x's 'a' property is the same as some existing object y's 'b'
property. You might try to write this as
       if y.b.oclIsUndefined() then x.a.oclIsUndefined() else x.a = y.b
endif
However, x.a.oclIsUndefined() is underspecified (see above). So, as far
as I can tell you would have to write something like
      if y.b.oclIsUndefined() then x.a.oclIsUndefined() and not
x.a.oclIsInvalid() else x.a = y.b endif
This assumes of course that y is not null.

Similar problems already existed with the final adopted version of the
OCL spec, before the type OclInvalid was introduced (I'm referring here
to a thread started by John Daniels in May of 2004). Splitting
OclUndefined into OclUndefined and OclInvalid seems to have just
introduced one more indirect level of confusion. The problem hasn't gone
away, it's only become more confusing.

    -Earl Waldin

----------------------------------------------------------------------
Earl Waldin                             tel: +41 31 828 9222
Paranor AG                              fax: +41 31 828 9299
Juraweg 14                              email: earl.waldin@paranor.ch
CH-3046 Wahlendorf
Switzerland
----------------------------------------------------------------------


-----Original Message-----
From: puml-list-request@cs.york.ac.uk
[mailto:puml-list-request@cs.york.ac.uk] On Behalf Of D H. Akehurst
Sent: Monday, 03 April, 2006 16:32
To: puml-list@cs.york.ac.uk
Subject: FW: Invariants evaluating to undefined



Having had a little time to look at the v2.0 of OCL2.0 I have some
questions regarding the new 'null' and OclInvalid values wrt the old
OclUndefined value and the discussion a few weeks ago under this thread.
 
consider a model containing class Person, with andassociation to itself
with end named 'wife' and an attribute 'name'.
 
if a person is not married are the following correct?
 
context Person
 
self.wife = null
self.wife.name = OclInvalid
Set{ null }->size() = Set{self.wife}->size() = 1
Set{ OclInvalid }->size() = Set{self.wife.name}->size() = 0
 
they seem to make sense, I'm not sure about the following
 
self.wife->isEmpty() = 1  -- ?? this is consistent with the above, but
not with old versions of OCL!
 
Have I missed something?
Received on Mon Apr 03 18:44:13 2006