On the Semantics of Renement Calculi
Hongseok Yang, Uday S. Reddy · 2000
Renement calculi for imperative programs provide an in- tegrated framework for programs and specications and allow one to develop programs from specications in a systematic fashion. The seman- tics of these calculi has traditionally been dened in terms of predicate transformers and poses several challenges in dening a state transformer semantics in the denotational style. We dene a novel semantics in terms of sets of state transformers and prove it to be isomorphic to positively multiplicative predicate transformers. This semantics disagrees with the traditional semantics in some places and the consequences of the dis- agreement are analyzed.