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	Refines	Implementation relation
w:[P,Q]	—	Specification	From P establish Q
wp	—	Weakest precondition	Dijkstra's wp
:=	—	Assignment	Deterministic
:∈	—	Choose	Nondeterministic
⊓	U+2293	Meet	Greatest common refinement
⊔	U+2294	Join	Least common abstraction

Metatheory. Refinement is a preorder (reflexive, transitive). Programs form a complete lattice under refinement. Nondeterminism: more nondeterministic = less refined. Miracles (wp(S,false)=true): not implementable, but allow specification. Feasibility: specification is implementable if not miraculous.

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. Requires formal specification skills. Manual refinement steps need human creativity. Proof obligations can be complex. Tool support (Atelier B, Rodin) has learning curve. Doesn't directly handle real-time or probability. Refinement strategy is not algorithmic.