Refinement Calculus
Encyclopedia
Refinement calculus is a formalized approach to stepwise refinement for program construction. The required behaviour of the final executable program is specified as an abstract and perhaps non-executable "program", which is then refined by a series of correctness-preserving transformations into an efficiently executable program.
Proponents include Ralph-Johan Back
, who originated the approach in his 1978 PhD thesis On the Correctness of Refinement Steps in Program Development, and Carroll Morgan
, especially with his book Programming from Specifications (Prentice Hall, 2nd edition, 1994, ISBN 0-13-123274-6). In the latter case, the motivation was to link Abrial
's specification notation Z
, via a rigorous relation of behaviour-preserving program refinement, to an executable programming notation based on Dijkstra's language of guarded commands. Behaviour-preserving in this case means that any Hoare logic
satisfied by a program should also be satisfied by any refinement of it, which notion leads directly to specification statements as pre- and postconditions standing, on their own, for any program that could soundly be placed between them.
Proponents include Ralph-Johan Back
Ralph-Johan Back
Ralph-Johan Back is a Finnish computer scientist.Back originated the refinement calculus, an important approach to the formal development of programs using stepwise refinement, in his 1978 PhD thesis at the University of Helsinki, On the Correctness of Refinement Steps in Program Development. He...
, who originated the approach in his 1978 PhD thesis On the Correctness of Refinement Steps in Program Development, and Carroll Morgan
Carroll Morgan (academic)
Carroll Morgan is an Australian computer scientist. An Australian Professorial Fellow at the University of New South Wales, his primary research interests are probabilistic models for security and concurrency. He is also the author of numerous papers and active member of a number of IFIP working...
, especially with his book Programming from Specifications (Prentice Hall, 2nd edition, 1994, ISBN 0-13-123274-6). In the latter case, the motivation was to link Abrial
Jean-Raymond Abrial
Jean-Raymond Abrial is a French computer scientist and inventor of the Z and B formal methods.J.-R. Abrial is the father of the Z notation , during his time at the Programming Research Group within the Oxford University Computing Laboratory, and later the B-Method , two leading...
's specification notation Z
Z notation
The Z notation , named after Zermelo–Fraenkel set theory, is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer-based systems in general.-History:...
, via a rigorous relation of behaviour-preserving program refinement, to an executable programming notation based on Dijkstra's language of guarded commands. Behaviour-preserving in this case means that any Hoare logic
Hoare logic
Hoare logic is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician C. A. R. Hoare, and subsequently refined by Hoare and other researchers...
satisfied by a program should also be satisfied by any refinement of it, which notion leads directly to specification statements as pre- and postconditions standing, on their own, for any program that could soundly be placed between them.