The refinement calculus is a formalisation of the stepwise refinement method of program construction. The required behaviour of the program is specified as an abstract, possibly non-executable, program which is then refined by a series of correctness-preserving transformations into an efficient, executable program.
We give an introduction to the application of the refinement calculus by using it to derive a few example programs. You may need to take a quick look at the
used in this tutorial, before going on to the
Note that the specification notation used here is closer to the style of Back and Morris, rather than that of Morgan, though the differences are minor.
In the refinement calculus, specifications are written as abstract programs usually in the form of specification statements. For example, a program that assigns x an arbitrary element from set S, provided S is not empty, may be specified as:
{ ~(S = {}) } x := x' | x' in S.
We write
P1 [= P2
to say that program P1 is refined by program P2. This means that P2 is a correct implementation of P1. Since refinement is transitive, a refinement step can always be broken up into a number of smaller steps, i.e.,
P1 [= P2 /\ P2 [= P3 -------------------------- P1 [= P3
Also, if a program consists of some sub-programs, e.g., P1;P2, then the sub-programs can be refined separately, in order to refine the composite program.
At each stage in the refinement process, the current program, or some sub-program of the current program is transformed by applying a refinement law to it. You do not need to study the list of refinement laws before proceeding, as their effect will become clear as you go through the examples. At each refinement step in the example derivations, there is a link to the law that is being applied.
The aim in the following examples is to refine the specifications into programs in a Pascal-like subset of the programming notation which has simple assignment, sequential composition, IF-statements, DO-loops, integers (along with basic integer arithmetic such as addition and multiplication), arrays, and records. The example derivations are:
A more comprehensive list of refinement laws and there application to several interesting case studies may be found in Morgan's book.
A prototype tool, called the Refinement Calculator, which supports the type of refinement used in this tutorial has been developed by a group at Åbo Akademi University in Finland.
Prepared by Michael Butler.
Last updated: 16 Jan 1996.