ABSTRACT

A nondeterministic command is useful when the order of execution of a number of commands affects the outcome in a way that is not of interest at the present level of abstraction. For example, the following operation assembles the ingredients for a drink without specifying the order, though that may have a detectable effect on the result (see Appendix C.1).