The Least Conjunctive Refinement and Promotion in the Refinement Calculus
Brendan P. Mahony · Formal Aspects of Computing · 1999
Abstract. A syntactic calculation of Morgan's least conjunctive refinement operator for predicate transformers is developed. The operator is used to develop a general approach to lifting relational operators to predicate transformer operators. Predicate transformer versions of the relational conjunction and disjunction operators are considered in detail. The Z-based technique of program promotion is considered in a refinement calculus setting. A standard Z promotion example is recast in the refinement calculus.