Refinement calculi for imperative programs provide an integrated framework for programs and specifications and allow one develop programs from specifications in a systematic fashion. The semantics of these calculi has traditionally been defined in terms of predicate transfoermers and poses several challenges in defining a state transformer semantics in the denotational style. We define a novel semantics in terms of sets of state transformers and prove it to be isomorphic to positively multiplicative predicate transformers. The semantics disagrees with the traditional semantics in some places and the consequences of the disagreement are analyzed.
H. Yang and U. S. Reddy. On the Semantics of Refinement Calculi. In Foundations of Software Science and Computation. 359 - 374 Springer-Verlag, 2000.
Click here to retrieve a compressed PostScript file containing a copy of this paper. A slightly longer version is here.