Re: comments on OCL



Date view Thread view Subject view Author view

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 operations have to be read operationally because reading in this declarative 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


Date view Thread view Subject view Author view