A calculus of refinements for program derivations (Q1111362): Difference between revisions

This paper presents a semantic formalization of the stepwise refinement programming method. It extends earlier work of the same author, but it is selfexplanatory. The basic notion of the author's refinement calculus is the relation of correct refinement between programs: A program S is said to be correctly refined by another program S' if S' satisfies any specification that S satisfies. Specifications are treated as (non- executable) program statements, which determine a well-defined effect on the program state. Since a specification may be restricted to some of the properties, it acts like a nondeterministic statement. The approach is based on predicate transformers (Section 2) and is illustrated using a simple programming language (Section 3). In Section 4, the precise definition of a correct refinement is given. Then, the author shows that sequential and conditional composition, iteration and recursion are monotonic with respect to the refinement relation. (In an appendix, the author proves monotonicity in the case of unbounded nondeterminism.) The main result is a characterization of a correct refinement by reducing it to a specific pre-/\(post\)-condition formula that depends only on the statement being refined. Section 7 analyses the special case that the refinement does not introduce new variables. Finally, context-dependent refinements are considered. A small example rounds off this clearly written paper.