Vol. 139 (2001), Nos. 3-4, pp. 197--220
In the discipline of derivation of programs from specifications by refinement the demonic calculus of relations is a well-established tool, which allows to use demonic operators on relations considered as specifications of a program's input-output-behaviour together with the standard relation algebraic operators to reason about specifications ordered by the refinement ordering.
The central contribution of this paper is the introduction of a demonic product operator that embodies a natural concept of parallel composition of specifications. Of course, this raises the question of parallel decomposition, which in turn motivates the introduction of demonic implication and totalisation operators. Finally, we also present first results concerning parallel decomposition.
Keywords: Demonic calculus of relations, relation algebra, specification and refinement, direct product, demonic product, parallel decomposition