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.