Inv, Undefinedness, etc.



Inv, Undefinedness, etc.

From: Achim D. Brucker ^lt;brucker@spamfence.net>
Date: Thu 20 Apr 2006 - 15:30:02 BST
Message-ID: <slrne4f6na.8s1.brucker@nakagawa.inf.ethz.ch>
We also see serious problems with the latest OCL 2.0 standard document
at the OMG web site (ptc/05-06-06). We reference this document as
OCL2.0-2005.

As reference for building HOL-OCL, i.e. our own a proof environment
for OCL striving for compliance with the standard (see
http://www.brucker.ch/projects/hol-ocl/index.en.html), we still consider
as basis "The OCL Standard 2.0" Final Adopted Specification (03-10-14),
2003. We reference this as OCL2.0-2003.

While OCL2.0-2003 is also far from being perfect from the standpoint
of an academic tool-builder seriously concerned with semantic issues, it
has at least a clear, consistent vision for the intended semantics of
OCL. The  more recent standard proposal OCL2.0-2005 is an attempt to
integrate the OCL with more recent features in UML entirely on syntactic
grounds; as such, it represents a considerable step backwards with
respect to semantic consistency. Rather, it is a re-proof of the fact
that specification languages can not be designed entirely by renaming
and cut-and-paste, unfortunately.

One big issue in recent discussions was the role of the null-object vs.
no-value vs. undefined, which has to be clarified before any further
attempt to define the language. In OCL2.0-2005, they have been mingled
in an inconsistent manner, and we advocate to separate these issues
since they have different semantic properties.

1) Undefinedness:
=================

OCL2.0-2003 had an explicit value "oclUndefined" which is handled
deeply inside the (Strong-Kleene-) Logic of OCL. The crucial text blocks
over the logic had been copied; thus, it must be assumed that
OCL2.0-2005 still assumes a Strong-Kleene-Logic ("anything or'ed with
true is true").

In OCL2.0-2003, strictness was assumed for any basic operation, for
example:
        
             oclUndefined + 3 '=' oclUndefined

With '=', we mean her strong equality, i.e.
(oclUndefined '=' oclUndefined) '=' true in  contrast to OCL2.0-2003
assumption that = is strict.

A number of operations in OCL2.0-2003 are explicitly stated as
non-strict, among them a.oclIsDefined(), but also the logical operators.

Undefinedness in this sense can be interpreted as "exception" (like in
"1 div 0" or, more  crucially, in self.a where self has a reference not
defined in the store) or, as had been done in previous documents (as
"The OCL Manifesto"), as non-terminating computations in a
recursive operation.

Consistency of an invariant can be understood in this semantics as the
existence of states  such that the invariant is true, i.e. neither
false nor undefined.


Explicit undefinedness in this sense had been criticized by members of
the theorem proving community as too complex to be handled; rather,
implicit undefinedness by underspecification  is suggested. However, in
this point we disagree with Peter Schmitt, since we see that
undefinedness is omnipresent in an object-oriented  specification
language built over path-expressions describing constraints over
object-structures. Thus, the treatment of undefinedness must be handled,
in our view, more transparently and also inside the logic  in order to
make its effects transparent to the specifying software-engineer. The
treatment in an automated deduction system is clearly a challenge, but
appears feasible in the OCL context.

   SUGGESTION: We therefore propose to LEAVE undefinedness as it is in
   OCL2.0-2003. However,  the standard should make more precise that
   collection types are "smashed", i.e.  Set{oclUndefined,a,b} '='
   oclUndefined, and generators of sets (or other collections)
   are strict functions as is the default in the OCL semantics.

2) "No Value"
=============

At certain points in modelling, situations arise where an explicit
dummy-element is added to a type.

At some places, OCL2.0-2005 suggests to add "No Value"-elements into
*all* types. However, NoValue + 3 simply makes no sense; one could,
of course, also handle  strictness principles for this element, but
this would further complicate the logic,

SUGGESTION: The parametric collection type "Option(A)" should be
added (analogously so "Set(A)") which adds to the set of elements
for A a distinct element "noValue". Distinct means, that
Option(Option(A)) has to distinct "noValue" elements - as usual
in libraries for functional programming languages.

Multiplicities could then be modelled as a pair of "Option(Natural)"
instead of the type InfiniteNatural.

NoValue + 3 is simply an ill-typed expression.

3) "Null Objects"
=================

The authors of OCL2.0-2005 suggest null-objects, perhaps to to
facilitate test like "self = null" known from programming language
practice. If this is the only reason, than one could simply view
this "test" as syntactic synonym to "self.oclIsUndefined()" and
forget about it.

So far, the OCL2.0-2003 had the semantic vision that there is a
"one-to-one correspondence between objects and references" in a
state; this is clearly quite far away from programming language
reality, but such a "fully sharing" semantics for constructors of
a method language is at least possible. An alternative approach
--- that we call a "referential object universe" --- would mean
that constructors store also the reference generated for an
object into the object itself as additional (hidden) attribute.
Establishing the "one-to-one-correspondence" is then easy, even
with conventional operational semantics for object constructors.
Associating referential types "ref(A)" to all object types (as
in programming languages such as C++) or explaining referential
equality is also easy in this model; other issues (like the
@pre-construct) could be treated in a drastically simpler way in
the semantics.

However, the null-objects destroy this "one-to-one" correspondance.
If this is desired in order to pave the way towards referential
types etc., well, this is unavoidable, and could still be semantically
defined in a referential universe. However, we are talking about a
completely different semantic foundation of OCL as OCL2.0-2003.

SUGGESTION: Either define a syntactic synonym self.isNull() to
"self.oclIsUndefined()", which allows for keeping the semantics
chapter of OCL in OCL2.0-2003 (possible short term), or build a
completely new semantics on the basis of a referential universe
construction (as the situation stands, this is only possible
mid-term to long-term). In this world, null-objects would be distinct
from undefined such that Set{null, A} is defined provided that A is.



We hope that helps to clarify the discussion,


Burkhart Wolff and Achim Brucker
Received on Thu Apr 20 15:30:36 2006