10 - Refinement Calculus

Summary

Binary relations on states are not the only semantic domain for representing sequential, nondeterministic programs. Since Dijkstra published his first paper on weakest preconditions in 1975 ([Dij75]), a rich theory based on monotone functions mapping sets of states to sets of states has emerged. Such functions are called predicate transformers. For instance, one models programs as functions mapping each postcondition to the corresponding weakest precondition. One branch of this theory concentrates on our primary subject, namely, the stepwise refinement of programs, possibly using data refinement techniques [B80, MV94, Mor89a, vW90]. The major drawback of predicate transformer as models of programs is that they are more complicated than binary relations because the domain of predicate transformers is richer than what we intend to model, i.e., not every predicate transformer represents one of our programs. But the predicate transformer approach also has its advantages. Several main results achieved in previous chapters, especially the completeness theorems (Chapters 4 and 9) and the calculation of maximal simulators (Chapters 7 and 9), require rather complicated proofs. The aim of this chapter is to demonstrate that more elegant and succinct proofs for these and also some new results exist, such as, for instance, isomorphism theorems between the relational and predicate transformer world for various forms of correctness and the use of Galois connections.