Refinement: When an Implementation Satisfies a Specification

A specification and its implementation are two descriptions of the same behaviour at different levels of detail, and the question of whether one satisfies the other has a precise answer. The answer is refinement: an implementation refines a specification when every observable sequence of the implementation is permitted by the specification. Not when the code was derived from the specification, not when the tests pass, and not when a reviewer agreed they match.

The definition needs a notion of observation. Take the specification as a set of traces, finite or infinite sequences of externally visible events, and the implementation as a set of traces over the same alphabet. The implementation refines the specification when its trace set is a subset. Every behaviour the implementation can exhibit is a behaviour the specification allows; the implementation may allow fewer, never more.

That subset direction is the source of a common confusion. An implementation is more constrained than its specification, so an implementation that does nothing at all, with the empty trace set, refines every specification. Refinement alone does not establish usefulness. It establishes safety relative to a document, and the document is where usefulness lives. The empty implementation refines the specification and satisfies no requirement, which is why the specification must also say something about what must happen, not only what may.

Why the abstract state does not appear in the code

A specification typically mentions state that the implementation does not have. An abstract bank account has a balance; the implementation has a row with a version column and a ledger of entries. The balance is a function of the ledger, not a stored value. To compare the two, the proof needs a mapping from concrete state to abstract state, called an abstraction function, or more generally a simulation relation when the mapping is not a function.

def abstract_balance(ledger):
    # Sum of signed entries; the abstract balance has no separate storage.
    return sum(e.amount for e in ledger if e.committed)

The function above is total over concrete states, and the refinement proof obligation is that every concrete step preserves it: for each concrete transition from $c$ to $c’$, either the abstract state is unchanged, or there is an abstract transition from $\alpha(c)$ to $\alpha(c’)$ that the specification permits. The first case is a stuttering step, and it is the one that trips up people writing their first refinement proof.

Stuttering is unavoidable. The implementation performs steps the specification does not model: logging, cache updates, retries of an internal call, a two-phase commit’s prepare phase. None of these is observable at the abstract level, so each is a step where the abstract state stays put. A refinement relation that requires every concrete step to correspond to an abstract step is therefore unsatisfiable for any real system. The relation must allow the implementation to stutter, and the specification’s own behaviour must be insensitive to stuttering. That insensitivity is why specifications are usually written to be stutter-invariant, treating any number of unobservable internal steps as a no-op.

The choice of abstraction function is a design act, not a discovery. Two implementations that store the same data differently need different functions, and a function that maps to the wrong abstract state produces a proof obligation that is false rather than a proof that fails. In practice the function is written alongside the implementation, and it doubles as documentation of what each concrete field means — the ledger’s committed flag exists precisely because the abstract balance does not count uncommitted entries.

Refinement forbids more than it requires

The subset definition has a sharp consequence: an implementation that behaves in a way the specification does not mention is not a refinement, even if the behaviour is an improvement. The direction is what saves the common case. An implementation that never fails refines a specification that permits failure, because dropping failure traces still leaves a subset. An implementation that fails in a new way, or returns an error the specification did not list, adds traces and is therefore not a refinement at all.

The practical form of this rule is that adding behaviour is a breaking change to the refinement relation. A new error path, a new field in a response, a new state in a state machine — each adds traces. Whether that matters depends on what the specification says about observation. If the specification declares the response fields as an open set, adding one is permitted; if it enumerates them, adding one is a violation. Specifications that leave the observation alphabet implicit get the worst of both: nobody can tell whether a change is a refinement, so every change is argued case by case.

This is also why the requirement to document error taxonomies in function contracts is not pedantry. An unlisted error is a trace the specification did not permit, and the caller’s handling code is refined against a document that says the error cannot occur.

Downward and upward simulation

The simple case is an abstraction function: each concrete state maps to exactly one abstract state. When the mapping is one-to-many — several concrete states correspond to the same abstract state, and the choice depends on history — the proof needs a simulation relation instead, and the direction of the relation determines the proof method.

Downward simulation relates concrete and abstract states and requires that each concrete step be matched by an abstract step from a related abstract state. Upward simulation runs in the other direction: it starts from an abstract state and finds a concrete state that can match the remaining abstract behaviour. Downward simulation is easier to write and is complete for many systems, but not for all: implementations whose behaviour depends on information not present in the abstract state, such as a scheduler’s internal choice, may require upward simulation or a combination of the two.

The practical consequence is that refinement proofs sometimes fail for a reason that has nothing to do with correctness: the chosen simulation is too weak. Strengthening the relation — adding a conjunct that records more about the concrete state — usually repairs it, at the cost of a larger invariant to maintain. This is the same strengthening manoeuvre as in inductive invariants, applied to a relation between two machines rather than to a property of one.

Refinement across versions

The relation generalises to time. When version 2 of a service must remain compatible with clients written against version 1, the requirement is that version 2’s observable behaviour refines version 1’s specification for every request those clients can send. New requests, new fields, and new capabilities are outside version 1’s alphabet, so they do not enter the comparison. Changed behaviour on an old request does.

That framing resolves most compatibility arguments. Adding an optional field to a response is a refinement if the client’s specification treats the response as a record with known fields plus an unconstrained remainder; it is not a refinement if the client’s parser rejects unknown fields. Neither behaviour is wrong, and the specification has to pick one. The same reasoning covers error codes, ordering guarantees, and default values: compatibility is a statement about the trace set of the old interface, and every claim about it is a claim that a particular set of traces is unchanged.

The relation also explains why internal refactoring is unconstrained while interface change is not. A refactoring that preserves the abstract state and adds only stuttering steps is a refinement by construction, because the observable traces are identical. A change that alters a timing guarantee is not, even when the values are the same, because timing is part of the alphabet when the specification includes it. Which brings the argument back to the boundary between what a specification observes and what it leaves free — the same boundary that partial failure semantics draws when it decides whether a caller can observe an intermediate state.