Read more
This volume collects the work accomplished at Oxford on the refinement calculus: the rigorous development, from state-based assertional specifications, of executable imperative code. 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 light-weight treatment of types in simple imperative programs. State-based assertional specification - in the Z style - was established at Oxford by J.-R. Abrial and much developed during the 1980's. Its principal effects on the minds of those who encountered it were: first, an exhilaration that one, at last, could be both abstract and yet precise;
Second the realization that its mathematical nature allowed rigorous reasoning about and exploration of proposed designs; and third, a desire to proceed rigorously from such specifications to executable code. 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 undergraduate degree course in computer science, which started in 1985. On the Refinement Calculus gives one view of the development of the refinement calculus and its attempt to bring together - among other things - Z specifications and Dijkstra's programming language. It provides excellent reference material for all t hose seeking the background and mathematical underpinnings of the refinement calculus.
