Parallel composition and decomposition of specifications

In the discipline of derivation of programs from specifications by refinement the demonic calculus of relations is a well-established tool, which allows the use of 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.