Refinement Calculus Tutorial

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

Logical Notation and Mathematical Notation

used in this tutorial, before going on to the

Specification and Programming Notation.

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:

• Swapping Variables: Swaps two variables around.
• Maximum: Finds the maximum of two numbers.
• Factorial: Finds the factorial of a non-negative integer.
• Searching: Searches for an entry in a look-up table.

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.

Useful References

1. R.J.R. Back. Correctness Preserving Program Refinements: Proof Theory and Applications. Tract 131, Mathematisch Centrum, Amsterdam, 1980.
2. ___. A calculus of refinements for program derivations. Acta Informatica, 25:593-624, 1988.
3. E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.
4. D. Gries. The Science of Programming. Springer-Verlag, 1981.
5. E.C.R. Hehner. The Logic of Programming. Prentice-Hall, 1984.
6. C.C. Morgan. The specification statement. ACM Transactions on Programming Languages and Systems. 10(3), 1988.
7. ___. Programming from Specifications (2nd Edition). Prentice-Hall, 1994.
8. J.M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9(3):287-306, 1987.

Prepared by Michael Butler.

Last updated: 16 Jan 1996.