On correct refinement of programs

摘要

The stepwise refinement technique is studied from a mathematical point of view. A relation of correct refinement between programs is defined, based on the principle that refinement steps should be correctness preserving. Refinement between programs will therefore depend on the criterion of program correctness used. The application of the refinement relation in showing the soundness of different techniques for refining programs is discussed. Special attention is given to the use of abstraction in program construction. Refinement with respect to partial and total correctness will be studied in more detail, both for deterministic and nondeterministic programs. The relationship between these refinement relations and the approximation relation of fixpoint semantics will be studied, as well as the connection with the predicate transformers used in program verification.