Re: OCL challenge



Date view Thread view Subject view Author view

Mark Richters (mr@Informatik.Uni-Bremen.DE)
07 Dec 2000 11:30:29 +0100


Daniel Jackson <dnj@lcs.mit.edu> writes: > 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? Yes, it is USE syntax. The OCL grammar is embedded as a subset. I think that it's much easier to work with a single human-readable (i.e., not XMI) textual specification, allowing me to use standard tools for editing, parsing, etc. > 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). The reason for using sequences was indeed to capture the list structure more precisely. Sets would have also been fine. Note, however, that there is no flattening involved. Flattening only applies to nested collections. The sequences used in the specification are always flat, in that their elements are never collections but object types. > 3. the frequent uses of asSet are presumably because of your view > (in your ER98 paper) that there should be no implicit flattenings? No, this is not related to flattening (see above). A conversion to sets is not strictly necessary. There are only two places, where a conversion is done with asSet. (1) In invariant NoDuplicates it is a convenient way to remove duplicates from a sequence. (2) In the first invariant it is used because there is no intersection operation for sequences in OCL. > 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? Yes, although, I think, this invariant could be expressed shorter in context of Map as context Map inv: self.list.closure()->forAll(l | l.oclAsType(NonEmptyList).elt.oclIsKindOf(Pair)) > 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? Unfortunately, no. In fact, evaluation of the invariant NoCycles will not terminate if there is a cycle, because the recursive tail() call will not terminate. In this case, the USE tool will complain with Stack overflow. The expression is probably nested too deep or contains an infinite recursion. In general, recursive operations should be written with an explicit condition that guarantees termination. The tail() operation would have to be modified accordingly. The UML/OCL standard mentions recursive operation calls only for use in postconditions (p. 7-12) without giving a semantics. The semantics in USE is an operational one based on assignment not on equation. The Amsterdam Manifesto on OCL discusses this issue in more depth. > 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. We have a simple spring embedder algorithm that helps to get a first sketch. However, the final layout seen in the screen shot has been manually adjusted. Our tool can also generate graph files for the VCG tool in order to get something looking like a class diagram from a textual specification. > finally, your question about static typing. [...] > 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? Your Alloy specification really looks nicer and more concise for this model. But I wonder, whether your approach to the typing issue is still manageable in context of large specifications. For example, we have translated the UML 1.3 metamodel together with the well-formedness rules into a USE specification. The specification contains 151 invariants and 41 additional operations some of which are quite complex. A large number of type errors could be found with our tool thanks to the strong type checking rules of OCL (details are in our UML'2000 paper). How are your experiences with larger Alloy specifications? Regards, Mark -- Mark Richters (mr@informatik.uni-bremen.de)


Date view Thread view Subject view Author view