Refinement calculus

A refinement calculus is a formal framework for transforming abstract specifications into concrete implementations through mathematically justified steps. The core idea is that a program or system can be developed not by writing code and then testing it, but by starting with a precise description of desired behavior and progressively replacing abstract constructs with concrete ones, each step preserving correctness. The concept originated in the work of Edsger Dijkstra on predicate transformers and was developed systematically by Carroll Morgan and others in the 1980s. Refinement calculi underpin the B method and VDM, where proof obligations guarantee that each refinement step maintains the observable properties of the original specification. The calculus typically treats programs as predicate transformers: a program maps a postcondition to the weakest precondition that guarantees it. Refinement then becomes logical implication — one program refines another if it satisfies stronger postconditions under weaker preconditions. The power of this approach is that it makes program development a form of directed proof construction. The weakness is that it requires developers to think in terms of logical predicates rather than computational processes, a shift that has limited its adoption outside specialist communities. Refinement calculus is not merely a technical apparatus; it is a philosophical commitment to the idea that software can be correct by construction, not merely correct by coincidence.