Abstract.
In the refinement calculus, program statements are modelled as predicate transformers. A product operator for predicate transformers was introduced by Martin [18] and Naumann [25] using category theoretic considerations. In this paper, we look more closely at the refinement-oriented properties of this operator and at its applications. We also generalise the definition of the product operator to form what we call a fusion operator. Together, the fusion and product operators provide us with algebraic ways of composing program statements in the refinement calculus in order to model effects such as conjunction of specifications, simultaneous execution, and embedding of smaller programs into larger contexts.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
Author information
Authors and Affiliations
Additional information
Received: 12 February 1996 / 25 August 1998
Rights and permissions
About this article
Cite this article
Back, RJ., Butler, M. Fusion and simultaneous execution in the refinement calculus. Acta Informatica 35, 921–949 (1998). https://doi.org/10.1007/s002360050148
Issue Date:
DOI: https://doi.org/10.1007/s002360050148