Nondeterministic "functions" in OCL and implications



Date view Thread view Subject view Author view

Perdita Stevens (Perdita.Stevens@dcs.ed.ac.uk)
Fri, 25 Feb 2000 17:28:20 +0000 (GMT)


If the intention was to make sure that sortedBy is deterministic -- that given a collection, that there is a unique sequence which sortedBy may return -- I think there's a condition missing in the definition of sortedBy which would make Mark's example illegal. In UML1.3 it says: UML1.3> sortedBy(expr : OclExpression) : Boolean UML1.3> Results in the Sequence containing all elements of collection. The UML1.3> element for which expr has the lowest value comes first, and so on. UML1.3> The type of the expr expression must have the < operation defined. UML1.3> The < operation must be transitive i.e. if a < b and b < c then a < UML1.3> c. UML1.3> post: It sounds as though the intention is for < to be a total order, i.e. irreflexive, antisymmetric and transitive, and such that for any two elements a and b we have one of a < b, b < a and a = b. (And the latter has to be "identically equal", none of your user-defined equality functions that can make two objects with different identity "equal".) JW> We could argue that it is a matter of good style, to not write JW> nondeterminsitic OCL. However, I do not know whether you can check this JW> from the text of the constraint. We'd need a good definition of what nondeterministic OCL is -- I haven't thought carefully about this but I bet there's a question about at what level you look -- you'd expect to find cases where there's nondeterminacy in the middle but it "comes out in the wash" when something "later" gives the same answer whichever nondeterministic choice was made. In some cases you probably wouldn't want to rule this out? (If you do rule them all out I suspect you have to get rid of iterate on sets and bags altogether.) For some sensible definition, you could certainly find syntactic conditions that would be _sufficient_ to ensure there was no non-determinacy (not using sets or bags would be a good initial candidate :-) but I'm not sure whether there would be such conditions that wouldn't be too restrictive for modellers. I'd bet a small amount that, for such a sensible definition, finding _necessary_ and sufficient conditions -- i.e., so that a tool would let you write exactly the deterministic expressions -- is impossible in principle. If anyone really wants to know I guess I could try to code up some relevant kind of machine and its halting problem in OCL but I think it would be a boring exercise. This isn't a curiosity though, as there are "interesting" knock on effects. Nondeterminacy spreads: e.g. suppose we have two sequences which could be the value of some expression, and that that expression was then tested in some way which would come out true for one of the possibilities and false for the other. Now that boolean test is nondeterministic, and so on... This kind of thing has the potential to make reasoning with OCL a non-starter. The waters are deep and I don't know them too well. I remember some discussion of related problems in EML, though (Extended ML, Don Sannella et al: http://www.dcs.ed.ac.uk/home/dts/eml/). It's tempting to throw in some implicit quantification, e.g. to say "ah, this is false because there's some legal value for which it's false". But that gets really really hairy quite fast: we don't want to do that! Do you want me to write up any of this as an issue, or will this discussion do? Perdita -- Dr. Perdita Stevens Division of Informatics, University of Edinburgh www.dcs.ed.ac.uk/home/pxs Fax: +44 131 667 7209


Date view Thread view Subject view Author view