Carroll Morgan, Trevor Vickers.
On the Refinement Calculus.
Springer. 1992
The refinement calculus is a notation and set of rules for deriving imperative programs from their specifications. It is distinguished from earlier methods (though based on them) because the derivations are carried out within a single ‘programming’ language: there is no separate language of specifications. So far, it has uncovered ‘miracles’, novel techniques of data refinement, a simpler treatment of procedures, ‘conjunction’ of programs, and a lightweight treatment of types in simple imperative programs.
The integration of specifications and code was proposed by R.-J. R. Back in the late 1970’s, when he inserted specifications into Dijkstra’s language based on weakest preconditions. At Oxford, this same idea, although much later, was amplified both by the strong research tradition in specification and by the challenge offered by the University’s new undergraduate degree course in computer science.
On the Refinement Calculus gives one view of the development of the refinement calculus and its attempt to bring together – among other thinqs – Z specifications and Dijkstra’s programming language. It is an excellent source of reference material for all those seeking the background and mathematical underpinnings of the refinement calculus.