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 …