Daniel Jackson (dnj@lcs.mit.edu)
Mon, 13 Dec 1999 08:58:39 -0800

```
hubert,

> In my opinion, you have missunderstood the use of OCL-
> constraints. They are not intended to be executable, nor are they
> intended to be interpreted operationally. OCL-constraints are
> constraining the possible UML models.

we understand that OCL is supposed to be declarative and not operational:
our complaint is precisely that it isn't!

> In this case the constraint on
> allParents contraints all possible implementations of the allParents
> operation in a way to satisfy the above equation.

indeed, it seems to me that allParents should never be called an "operation"
at all: it's just a defined relation. but since OCL doesn't have transitive
closure, such relations need to be defined in this operational fashion.

> Consider three classes A, B, and C. The parent of A is B and the
> parent of B is C and the parent of C is again A. Let allParents return
> for A, B, and C the same set {A,B,C}. Then (in class A) we get the
> equations:
>
> allParents = {A,B,C}
>
> and
>
> self.parent->union(self.parent.allParents)
>           = {B}->union(B.allParents)
>   = {B} \cup {A, B, C}
>   = {A, B, C}
>
> Thus the OCL-constraint is defined and the model satisfies the
OCL-constraint.

i agree entirely that this is how we'd like to read the OCL constraint, and
this is just how constraints in Alloy are read. we've been assuming that OCL
way doesn't work. in short, the problem is that you can't axiomatize
transitive closure in first-order logic, so there can be no equations that
say exactly what you want. viewed as axioms, the OCL operations have the
form

r+ = r.parent U (r.parent)+

where r+ is the transitive closure of r that we're trying to define. as you
point out, the transitive closure of r will satisfy this axiom. the problem
is that many other relations will too, in particular the universal relation.
in your example, if we started by assuming

allParents = {A, B, C, D}

for A, B, C and D -- that is, allParents is the universal relation over
{A,B,C,D} -- the equation will still check.

what we need is not _any_ solution to the equation, but the _smallest_
solution. one way to get this is to construe the constraint operationally:
first we add A's parent, then we call the operation recursively. i quite
agree with you that this is very undesirable in a modelling language, but we
guessed that this was probably what the OCL authors had in mind -- why else
would they have called it an operation? given that you construe it
operationally, you now have to make sure that there are no cycles in the
parents relation, otherwise the recursion doesn't terminate.

so if there is a cycle in the parent relation, then allParents is not well
defined, and its use to rule out circularity is circular!

does this make sense?

/daniel
```