Skip to content

Refinement-Calculus Derivation

Formal derivation method — instantiates Specification-to-Execution Lowering

Derives a program from its specification by a chain of small, individually correctness-preserving refinement steps, each licensed by a law of the calculus — so the code is correct by construction.

Refinement-Calculus Derivation grows an implementation out of a specification by rewriting rather than writing. You begin with an abstract specification statement — a precondition and postcondition describing what the code must achieve — and repeatedly replace it, one law at a time, with something more concrete, until nothing abstract remains and what is left is executable code. Its defining move is that each replacement is a refinement (written ⊑): a step is legal only if the more-concrete version delivers everything the more-abstract one promised, guaranteed by the law that licensed it.[1] Correctness is therefore not tested at the end but accumulated along the way — the final program is correct by construction because every link in the chain preserved the specification. Where the archetype's compilers lower automatically, this is the by-hand, law-governed version of the same descent, and its product is as much the derivation as the code.

Example

A developer needs a routine that, given a sorted array and a target, returns an index of the target or reports its absence. Rather than write and debug a binary search — notorious for off-by-one and overflow bugs — they derive it. The specification is a precondition (the array is sorted) and a postcondition (the returned index holds the target, or a flag says it is absent). Applying the calculus, they introduce a loop by choosing an invariant — "the target, if present, lies within the current bounds lo..hi" — a law-sanctioned step that splits the spec into initialization, a loop body that must maintain the invariant while shrinking the interval, and a termination argument. Each later step refines one of those pieces under a law: the interval-halving update is derived to preserve the invariant, and that is exactly where the correct midpoint computation and boundary moves fall out — forced by the invariant rather than guessed. The result is a binary search whose correctness is a byproduct of how it was built, with the invariant standing as documentation of why it works.

How it works

  • Write the spec as pre/post. Capture intent as a precondition–postcondition pair over the program state — the top of the chain.
  • Apply refinement laws. Replace a specification statement with a more concrete construct (sequence, conditional, loop-with-invariant, assignment) using a law that guarantees the replacement refines what it replaced.
  • Discharge each law's side-conditions. A law applies only if its obligations hold (the invariant is maintained, the variant strictly decreases); meeting them is what makes the step legal.
  • Descend until executable. Repeat until no specification statements remain; the residue is code, and the chain of steps is its correctness argument.

Tuning parameters

  • Refinement granularity — big, intuition-guided steps vs. small, fully-justified ones. Fine steps are auditable and mechanizable but slow; coarse steps move fast and hide where an error could slip in.
  • Formality level — full proof of every side-condition vs. a rigorous-but-informal argument. More formality buys stronger assurance at real derivation cost; calibrate it to how critical the code is.
  • Data-refinement depth — how far to refine abstract data (a set) into a concrete structure (a hash table). Deeper data refinement yields more efficient code and lengthens the derivation.
  • Which law to apply — the creative dial. The invariant or decomposition you choose shapes the whole descent: a good choice makes the rest fall out; a poor one still yields a correct program, just a clumsy one.

When it helps, and when it misleads

Its strength is that it produces code that is correct by construction with a derivation explaining every decision; it turns debugging into a design activity, where errors are prevented rather than hunted; and it is unmatched where a bug is unacceptable and the algorithm is subtle enough that testing would never find the corner.

Its failure modes are the cost and the scope. It is labour-intensive and demands fluency in the calculus, so it does not scale to large systems and is reserved for a critical kernel. And refinement guarantees the code meets the specification: if the spec is wrong, the derivation faithfully delivers a wrong-but-provably-conformant program, and the sheer effort can lend false confidence to an unvalidated spec. The classic misuse is deriving elaborate proofs for code whose specification nobody validated — polishing the how while the what goes unchecked. The discipline is to validate the specification independently, before investing in refining it.

How it implements the components

  • refinement_chain — its essence: the ordered sequence of ⊑-steps from specification to code, which is both the method and its durable output.
  • admissible_transformation_rule_set — the calculus's laws, the fixed vocabulary of steps each guaranteed to preserve the specification.
  • precondition_postcondition_pair — the form intent takes at the top of the chain and at every intermediate specification statement along the way.

It does not choose among equivalent implementations for speed (optimization_freedom_budget, intermediate_representation_ladder — that's Query-Plan Lowering and Optimization), nor package a re-checkable certificate for an untrusted consumer (lowering_provenance_record, assurance_strength_profile — that's Proof-Carrying Transformation); it derives the implementation, correctness included, by hand.

Notes

The deliverable is the derivation, not only the code. Checking in the final routine and discarding the chain throws away the correctness argument and the ability to re-derive cleanly when the specification changes — the very things that justified deriving instead of writing. Keep the derivation as a first-class artifact beside the code.

References

[1] The refinement calculus (developed by Back, Morgan, and von Wright, among others) formalizes program construction as a sequence of steps under a refinement relation ⊑, where S ⊑ T means T satisfies every specification S does. Morgan's Programming from Specifications is the standard exposition. Correct-by-construction derivation is the direct payoff of the relation being transitive: chain the refinements and the endpoint refines the start. ↩