Program Derivation in the Refinement Calculus: An Introduction


Author: Lindsay Groves
Source: GZipped PostScript (64kb); Adobe PDF (291kb)

The refinement calculus is a formal calculus for deriving imperative programs from logical specifications, which formalises program construction by stepwise refinement. This paper introduces the basic concepts underlying the refinement calculus: a wide-spectrum language including non-executable constructs for expressing specifications, a refinement ordering on specifications/programs in this language, and a set of rules embodying laws about certain refinements that are always valid. The paper also shows how data refinement is formalised within the refinement calculus, presents some important theoretical results, and illustrates the techniques by deriving an algorithm to find the minimum and maximum elements of a set, using only 3n/2 comparisons, and then data refining this to an array representation.

[Up to Computer Science Technical Report Archive: Home Page]