B Method

Origin. Jean-Raymond Abrial, developed through the 1980s and set out in The B-Book: Assigning Programs to Meanings (Cambridge, 1996). Descends from Abrial's earlier Z notation but replaces Z's schema calculus with a calculus of generalised substitutions, giving specification and code a single semantics. Industrialized as Atelier B. Superseded for reactive systems by Event-B, which keeps the set theory and discards the operation-call model.

Models. Two languages layered on one another. The lower is typed set theory with first-order logic — every datum is a set, and relations, functions, sequences, and trees are defined rather than primitive. The upper is the Generalised Substitution Language, in which a substitution S denotes not a state change but the predicate transformer R ↦ [S]R, the weakest precondition guaranteeing R afterwards. An abstract machine packages state, an invariant, and operations; correctness is that the initialisation establishes the invariant and each operation preserves it. Refinement is a relation between machines, and a chain of refinements ending in the implementable subset B0 is translated to Ada or C.

Formalism.

Abstract machine: MACHINE M SETS S CONSTANTS c PROPERTIES P VARIABLES v INVARIANT I INITIALISATION T OPERATIONS op = ... END

Components: SETS: carrier sets. CONSTANTS: fixed values. VARIABLES: state. INVARIANT: state predicate. OPERATIONS: state transitions.

Substitution notation: x := E (simple assignment). x :∈ S (non-deterministic choice). PRE P THEN S END (precondition). P ⟹ S (guard). S [] T (bounded choice). @x·S (unbounded choice). ANY x WHERE P THEN S END.

The substitution calculus: A substitution is its weakest-precondition transformer. [skip]R ≡ R [x := E]R ≡ R[E/x] [PRE P THEN S END]R ≡ P ∧ [S]R [P ⟹ S]R ≡ P ⇒ [S]R [S [] T]R ≡ [S]R ∧ [T]R [@x·S]R ≡ ∀x·[S]R Note the asymmetry: a precondition conjoins, a guard implies. Outside P, PRE aborts and guarantees nothing; ⟹ is miraculous and guarantees everything.

Termination and feasibility: trm(S) ≡ [S]true — the substitution terminates. fis(S) ≡ ¬[S]false — the substitution can do something. false ⟹ S guarantees every R, so it is infeasible: the miracle, excluded from implementations.

Machine consistency obligations: Initialisation: [T]I. Each operation: I ∧ P ⇒ [S]I. Generated automatically from the machine text.

Refinement: REFINEMENT R REFINES M. Abstract variables v, concrete variables w, gluing invariant J(v, w). Obligation, for abstract S and concrete T: I ∧ J ∧ trm(S) ⇒ trm(T) ∧ [T]¬[S]¬J The inner ¬[S]¬J is the conjugate of S — "S is able to establish J". Forward simulation: the concrete may reduce nondeterminism, never introduce it.

Layering: MACHINE → REFINEMENT → IMPLEMENTATION. B0: the implementable subset, deterministic and loop-bearing. Structuring clauses INCLUDES, SEES, USES, IMPORTS, restricted to keep obligations local.

Tools: Atelier B: industrial prover and B0 code generator. ProB: animator and model checker, finding counterexamples the prover cannot. Rodin: Event-B platform.

Symbols.

Metatheory. The B-Book's organizing decision is that a substitution is a predicate transformer, so specification and program inhabit one semantic domain and refinement is a relation within it rather than between two formalisms. The transformers are monotone and conjunctive, which is what makes the two derived notions definable rather than postulated: trm(S) ≡ [S]true and fis(S) ≡ ¬[S]false, and the excluded miracle is the demand that implementations be feasible. Refinement is proved by forward simulation against a gluing invariant, the obligation using the conjugate ¬[S]¬J to say the abstract operation is able to match what the concrete one did; soundness gives transitivity, so a chain of refinements composes and the final B0 layer is correct by construction with respect to the top machine. Obligation generation is syntactic and complete for the machine-consistency conditions; discharging them is not, since the underlying logic is set theory. The method's standing evidence is METEOR, the driverless Paris Métro Line 14 signalling software, about 100,000 lines of B refined to Ada and deployed in 1998 (Behm, Benoit, Faivre, Meynadier, 1999).

Applies to. Railway signaling. Smartcard. Industrial verification. Safety-critical.

Limitations. The substitution calculus characterizes the relation between initial and final states, so nothing about intermediate states is expressible — concurrency, interleaving, timing, and reactivity all fall outside it, and the method's own response was to be replaced by Event-B rather than extended. Refinement is forward simulation against a gluing invariant, which is incomplete: refinements in which the concrete machine must resolve a choice earlier than the abstract one require backward simulation and cannot be discharged. The PRE construct is a precondition and not a guard, so an operation invoked outside its precondition aborts and its specification constrains nothing, which places the burden of establishing preconditions on the caller and outside the machine's own obligations. Proof obligations are sentences of typed set theory with unbounded quantification, whose validity problem is undecidable, so automatic discharge is necessarily partial. The structuring clauses carry visibility restrictions precisely because unrestricted sharing of state invalidates the locality that makes the obligations checkable machine by machine.

© 2026 Lingenic LLC