In this paper we present an algebraic construction of the category of monotonic predicate transformers from the category of relations which is similar to the standard algebraic construction of the integers from the natural numbers. The same construction yields the category of relations from the category of total functions. This provides a mechanism through which the rich type structure of the category of total functions can be promoted to successively weaker ones in the categories of relations and predicate transformers. In addition, it has exposed two complete rules for the refinement and composition of specifications in Morgan’s refinement calculus.
CITATION STYLE
Gardiner, P., Martin, C., & de Moor, O. (1993). An algebraic construction of predicate transformers. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 669 LNCS, pp. 100–121). Springer Verlag. https://doi.org/10.1007/3-540-56625-2_10
Mendeley helps you to discover research relevant for your work.