# Nondeterministic "functions" in OCL and implications

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
```