RE: OCL challenge



Date view Thread view Subject view Author view

Daniel Jackson (dnj@lcs.mit.edu)
Wed, 6 Dec 2000 10:17:53 -0500


mark, thank you! your spec is very helpful. i'd like to confirm that i understand some features of it: 1. presumably the structuring sublanguage in which you declare classes and relations is not official OCL? i've criticized this feature of UML/OCL before, as it seems to me essential to be able to have a fully textual spec, as you do. is this USE syntax? 2. why do you create sequences and then flatten them to sets, rather than just use sets all along? is it because you want to reflect the true list structure? (this is something that can't currently be expressed in Alloy, by the way). 3. the frequent uses of asSet are presumably because of your view (in your ER98 paper) that there should be no implicit flattenings? this does seem to eliminate ambiguity in OCL, but i'm bothered that it makes navigations more complicated. in Alloy, the dot operator is just relational image, so that x.p.q.r is ((x.p).q).r). in the new version of the language, we're making it more general, and dot will be relational composition, so it can be viewed also as x.(p.(q.r)). 4. the non-emptiness checks, for example in: -- Lists contained in Maps have Pairs as their elements -- Map.list.*next.elt in Pair context List inv ListsInMapsHavePairs: self.map->notEmpty implies self.closure()->forAll(l | l.oclAsType(NonEmptyList).elt.oclIsKindOf(Pair)) are presumably to guard against undefinedness? 5. in defining the closure operation, is there some way to know that the operation terminates, beyond doing a semantic analysis? is there a syntactic check that can determine that an operation definition corresponds to a relation that's uniquely defined? by the way, you misinterpreted one of my constraints: -- no object is both a key of some Pair and a val of some Pair -- no Pair.key & Pair.val context Pair inv NoObjectKeyAndVal: self.key <> self.val the Alloy constraint (no Pair.key & Pair.val) takes the set of all keys of all pair objects (the image of the set Pair under the relation key), and intersects it with the set of all vals of all pair objects. so presumably, the OCL version would be context Pair inv: Pair.allInstances->forAll(p1, p2 | p1.key <> p2.val) your visual output is impressive. what tool are you using to layout the object diagrams? we currently use AT&T's dot, but we'd like to find something simpler. on the diagram question: your correction to my diagram seems necessary from what i understand of UML. what i try to do in the paper i mentioned is to allow this situation without having to make every class a subclass of object, which for a large diagram would be a big nuisance. i also allow uses of lists in different contexts to be distinguished (as different boxes). finally, your question about static typing. Alloy is statically typed, and it has a rudimentary type inference mechanism so you can often omit types. but it has no notion of subtyping, so a class and its subclasses are modelled as sets of the *same* type. so, for example, if i have two subclasses Man and Woman of Person Man, Woman: Person i can write in Alloy no (Man & Woman) which says that no Person is both a Man and a Woman, where the intersection is well typed because both sets have type Person. but if i declare a set Name and a relation name : Person -> Name the expression Man.name & Woman for example, would be ill-typed, since the first subexpression has type Name, and the second has type Person. the basic types are associated with the sets that have no supersets, which i call "domains" in Alloy. i prefer this approach because it allows much more succinct constraints than OCL allows, since type casts are never needed. i'm also not convinced that the subtyping mechanism in OCL brings benefit in proportion to its complexity. do you have any experience detecting subtype errors? regards, /daniel ....I have tried to write a specification with OCL for your model. It is ....availabe as .... .... http://db.informatik.uni-bremen.de/~mr/Lists.use .... ....This specification can be checked with the USE tool (see ....http://db.informatik.uni-bremen.de/projects/USE). For ....example, a valid ....snapshot can be generated with the following script .... .... http://db.informatik.uni-bremen.de/~mr/Lists.cmd .... ....A screenshot showing this state is here .... .... http://db.informatik.uni-bremen.de/~mr/lists_state.gif .... .... ....> it's not clear exactly how to draw this, since not all ....Lists contain ....> Pairs, but the Lists contained by Maps do. one of the issues my ....> paper addresses is how to make solve this problem, so thoughts on ....> that also welcome. .... ....I have changed the model, so that Object is the parent of all other ....classes. The element of a NonEmptyList now is an Object. If the list ....is part of a map, then the element's class must be Pair which is a ....subclass of Object. This way, you can also put lists into ....lists, etc. ....The resulting class diagram can be seen in .... .... http://db.informatik.uni-bremen.de/~mr/lists_classes.jpg .... ....(not exactly UML, it has been automatically generated from ....the textual ....specification). .... ....I don't claim that my solution is elegant. There are a ....number of type ....casts required making the constraints hard to read. These don't seem ....to be necessary in Alloy. To what degree does Alloy provide static ....type checking? I first stumbled across the expression "list.*next" ....which appeared strange to me, because next is defined only for ....NonEmptyLists. .... ....Regards, Mark ....-- ....Mark Richters (mr@informatik.uni-bremen.de) .... .... .... ....To remove yourself from this list please mail ....puml-list-request@cs.york.ac.uk ....with a message containing the word "unsubscribe". ....


Date view Thread view Subject view Author view