Multialgebras, Power Algebs and Complete Calculi of Identities and Inclusions

Abstract: After motivating the introduction of nondeterministic operators into algebraic specifications, a language L with two primitive predicates, identity and inclusion, for specifying nondeterministic operations is introduced. It is given a multialgebraic semantics which captures the singular (call-time-choice) strategy of passing nondeterministic parameters. A calculus NEQ, with restricted substitutivity rules, is introduced. NEQ is sound and complete wrt. the multialgebraic semantics.

A language L+ is obtained by a slight modification of L admitting plural (run-time-choice) parameters. The multialgebraic semantics is not sufficient for modeling such parameters and it is generalized to power algebras. Augmenting NEQ with one rule for unrestricted substitutivity for the plural variables yields NEQ+ which is sound and complete wrt. to the power algebra semantics.

In the conclusion, we point out that the singular-plural distinction has two, relatively indepdent facets. It may be applied to the semantics of parameter passing but may also be restricted to the kinds of variables used in the specification language. The latter increases the expressiveness of the language even if one applies only the singular semantics of parameter passing.