The 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
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 C ...
, 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, ). In the latter case, the motivation was to link
Abrial's specification notation
Z, via a rigorous relation of behaviour-preserving
program refinement
Refinement is a generic term of computer science that encompasses various approaches for producing correct computer programs and simplifying existing programs to enable their formal verification.
Program refinement
In formal methods, program re ...
, to an executable programming notation based on
Dijkstra's language of
guarded commands. ''Behaviour-preserving'' in this case means that any
Hoare triple 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.
References
Formal methods
Formal specification languages
Logical calculi
{{formalmethods-stub