B Method

Origin. Jean-Raymond Abrial (1980s). Abstract machines. Refinement-based. Set-theoretic specification. Foundation of Event-B.

Models. Abstract Machine Notation. Set theory specification. Refinement to code. Proof obligations. Industrial application.

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. ANY x WHERE P THEN S END.

Proof obligations: Initialization establishes invariant. Each operation preserves invariant. Refinement preserves invariant. Generated automatically.

Refinement: REFINEMENT R REFINES M. Concrete variables. Gluing invariant. Data refinement.

Proof obligations: Abstract → concrete correspondence. Concrete operations refine abstract. Forward or backward simulation. Verified by theorem prover.

Tools: Atelier B: industrial prover. ProB: animator and model checker. Rodin: Event-B platform. Automated + interactive.

Symbols.

Keyword	Meaning
MACHINE	specification
INVARIANT	state property
OPERATIONS	transitions
REFINEMENT	implementation step

Metatheory. Set theory. Substitution calculus. Refinement. Proof obligations.

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

Limitations. Learning curve. Proof effort. Tool dependencies. Sequential focus.