Structured Spifications and Implementation of Nondetermiistic Data Types

Abstract: The use of nondeterminism in specifications, as distinct from underspecification, is motivated by an example in the context of data refinement. A simple formalism for specifying nondeterministic data types is introduced. Its semantics is given in terms of the existing formalisms of relations, multialgebras, sets of functions and oracles by means of appropriate translation rules.

Nondeterministic data refinement is studied from the syntactic and semantic perspective, and the correctness of the suggested proof obligations is proved. More general implementation relation and parameterisation of nondeterministic data types are discussed and the standard theorems of vertical and horizontal composition are generalised to the nondeterministic case.