zbMATH — the first resource for mathematics

Binary multirelations. (English) Zbl 1203.68035
de Swart, Harrie (ed.) et al., Theory and applications of relational structures as knowledge instruments. COST Action 274, TARSKI. Revised papers. Berlin: Springer (ISBN 3-540-20780-5/pbk). Lect. Notes Comput. Sci. 2929, 256-271 (2003).
Summary: Relational models for imperative programming languages provide a representation of commands in terms of binary input-output relations over states. Various relational models have arisen from modelling decisions on the distinction between angelic and demonic nondeterminism, and have been shown to be isomorphic to disjunctive or conjunctive predicate transformer semantics. For commands with both angelic and demonic nondeterminism it is known that monotone unary operators provide a predicate transformer semantics but there is no conventional relational model. In this paper we propose a novel relational representation, in terms of binary multirelations, for such commands. Then we show that binary multirelations and monotone unary operators are intertranslatable.
For the entire collection see [Zbl 1029.00017].

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
08A02 Relational systems, laws of composition
08A70 Applications of universal algebra in computer science
Full Text: DOI