Abstract:
A language for specifying nondeterministic operations which
generalizes the equational specification language is introduced. Then,
various notions of generated multimodels are discussed and sufficient
conditions for the existence of quasi-initial semantics of
nondeterministic specifications are given. Two calculi are introduced:
NEQ and NIP. The former is sound and complete with respect to the
class of all multimodels. The later is an extension of the former with
the omega-rule. It is sound and complete with respect to one of the
classes of the generated multimodels. The calculi reduce to the
respective deterministic calculi whenever the specification involves
only deterministic operations.