## Program Derivation in the Refinement Calculus: An Introduction

**CS-TR-94-21**
**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]