refinement calculus

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.{{cite web |last1=Butler |first1=Michael |title=Refinement Calculus Tutorial |url=https://www.southampton.ac.uk/~mbutler/refcalc-tut/home.html |accessdate=22 April 2020}}

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 [http://web.comlab.ox.ac.uk/oucl/publications/books/PfS/ 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 triple satisfied by a program should also be satisfied by any refinement of it, which notion leads directly to [http://www.ecs.soton.ac.uk/~mjb/refcalc-tut/home.html#morgan specification statements] as pre- and postconditions standing, on their own, for any program that could soundly be placed between them.