Book excerpts:

This book teaches elementary programming in the style that specifications and code are all programs; that there is a refinement order between programs; and that there is a specially restricted sub­language called 'code' that allows programs written in it to be executed with 'no thought at all'. The thinking is necessary elsewhere, to find the code that refines a given specification.

The approach rests on the work of Dijkstra, Hoare, and Floyd; and the programming language is Dijkstra's guarded commands, extended with specification constructs. The language itself is pre­sented in the early chapters, and each of its constructs is characterised by the refinement laws that it satisfies. The effect on a computer is described informally, as an aid to the intuition.

Later chapters are split between case studies and more advanced programming techniques. Each case study treats a programming example from beginning to end, using the methods available at that point, and is well known rather than especially intricate. The more advanced programming techniques are procedures, recursion, recursive data structures, modules and finally state transformation (including data refinement).

The book is intended to be useful both to those learning to program and to those who --- programmers already --- would like to make the link between their existing skill and the specifications from which their programs (should) spring. Experience based on nearly 10 years' exposure to second­-year computing undergraduates sug­gests, however, that the best approach is at first to exercise a fairly light touch on the refinement laws. For beginning programmers they should assist, not prescribe: at that stage, the list of refinement laws is for reference, not for certification. And learning to use invariants for iterations is work enough on its own.

Light touch or no, the underlying theme of specification, refinement and code is one that students respond to, and it informs their approach to other courses and to computing generally. More experienced programmers may recognise some of those features in specification and development methods such as Z and VDM, for parts of which the refinement calculus forms an adjunct or even an alternative.