Refinement Calculus

Origin. Back and Morgan developed refinement calculus (1980s). Extends Dijkstra's weakest preconditions to program derivation. Programs derived by stepwise refinement from specifications. Specification statements as primitive. Foundation for B-Method and Event-B.

Models. Deriving programs from specifications. Specification: what the program should do (relation). Implementation: how it does it (executable code). Refinement: specification ⊑ implementation means implementation meets spec. Stepwise: refine in stages, preserving correctness.

Formalism.

Specification statement: w:[pre, post] "Assuming pre, establish post, modifying only w."

Refinement ordering: S ⊑ S' — S' refines S Meaning: every behavior of S' is allowed by S.

Weakest precondition: wp(S, Q) = weakest P such that {P} S {Q} S ⊑ S' iff ∀Q. wp(S, Q) ⇒ wp(S', Q)

Refinement laws:

Skip: w:[pre, pre] ⊑ skip
Assignment: w:[pre, post] ⊑ w := e if pre ⇒ post[e/w]
Sequence: S ⊑ S₁; S₂ if appropriate weakest preconditions
Conditional: S ⊑ if b then S₁ else S₂ if both branches refine
Loop: S ⊑ while b do S₁ with variant and invariant

Data refinement: Change data representation. Abstraction relation R links abstract and concrete states. Simulation: concrete simulates abstract via R.

Monotonicity: If S ⊑ S' then C[S] ⊑ C[S'] for any context C. Allows local refinement.

Symbols.

Symbol	Unicode	Name	Meaning
⊑	U+2291	Square image of or equal to / Refinement	S ⊑ S′ : S′ implements S
w:[P,Q]	—	Specification statement	Assuming P establish Q, changing only w
wp	—	Weakest precondition	Dijkstra's transformer, the semantics of ⊑
:=	—	Assignment	Deterministic update
:∈	—	Nondeterministic choice	Assign some value from a set
∈	U+2208	Membership	The set from which :∈ draws
⊓	U+2293	Square cap / Meet	Demonic choice; greatest common refinement
⊔	U+2294	Square cup / Join	Angelic choice; least common abstraction
⇒	U+21D2	Implication	Entailment between predicates
∀	U+2200	Universal quantifier	∀Q in the wp characterization of ⊑
post[e/w]	—	Substitution	e replaces w in the postcondition
R	—	Abstraction relation	Links abstract and concrete states in data refinement
C[S]	—	Program context	Site of a local refinement step

Metatheory. Refinement is defined semantically: S ⊑ S′ iff wp(S, Q) ⇒ wp(S′, Q) for every postcondition Q, so it is the pointwise order on predicate transformers, a preorder on syntax and a partial order on transformers. The essential structural theorem is Back and von Wright's: once Dijkstra's law of the excluded miracle and continuity are dropped and only monotonicity is retained, the monotone predicate transformers on a fixed state space form a complete lattice under ⊑, with abort as the bottom, magic as the top, ⊓ as demonic choice, and ⊔ as angelic choice — the specification statement w:[P, R] is then simply the conjunctive transformer P ∧ ∀w′. (R ⇒ Q[w′/w]). Every program construct is monotone with respect to ⊑, which is exactly what licenses refining a subcomponent in place. A specification is feasible, that is implementable, precisely when it is non-miraculous: wp(S, false) = false. Data refinement is sound by forward (downward) simulation, but forward simulation alone is incomplete; adding backward (upward) simulation makes the pair complete, a result established by Hoare, He, and Sanders and given a single-rule formulation by Gardiner and Morgan (1993).

Applies to. B-Method and Event-B (safety-critical systems). Correct-by-construction development. Protocol derivation. Concurrent program development (Action Systems). Security protocol refinement. Hardware derivation.

Limitations. The lattice contains elements no machine realizes. Magic and every miraculous statement above it are perfectly good transformers, and angelic choice ⊔ has no executable counterpart in a deterministic sequential language, so a derivation is not finished when it terminates in program syntax — a separate feasibility obligation wp(S, false) = false must be discharged. Forward simulation, the rule actually used in practice, is incomplete for data refinement; there are refinements provable only by backward simulation. The refinement order is defined by wp and therefore preserves only what wp records: the relation between initial and final states. It does not preserve timing, resource consumption, or observable intermediate behaviour, so it is the wrong notion for real-time, probabilistic, and reactive systems without changing the semantic domain, and it is unsound for security. This last point is the refinement paradox: noninterference is a property of pairs of executions, refinement removes nondeterminism, and a legitimate refinement of a secure specification can therefore be insecure. Loop refinement still needs an invariant and a variant, and the resulting obligations are first-order and undecidable.