Glossary

Abstract Model: see B model

B project: all the activities using B, starting from requirements and leading to a system complying with these requirements.

B development: see B project

B model: a mathematical description which represents some real entities of the target system or of its context. In a B project, several mathematical modellings are used to either represent several aspects of a system, or an aspect at various levels of detail. B models are written down into B components (abstract machines, refeinements), but are independent entities.

B modelling: activity of creating B models

B specification: set of B components and relationships that are equivalent to initial requirements.

Basic machine: Compenent that is specified in B but implemented manually. The specification component is only used to generate a skeleton that needs to be completed by manual/third-party code.

B0: subset of the B language that is directly implementable: sequence, if-then-else, loop, operation call, scalar type, tables. This subset depends on the code generator.

B0 checker: tool to verify that an implementation complies with B0 constraints, that it is effectively implementable

Component : a component is at least made of a specification (MACHINE) and a refinement (IMPLEMENTATION). When the transformation from the specification to the implementation generates too many proof obligations, one or several intermediate refinements might be needed (MACHINE -> REFINEMENT -> ... -> IMPLEMENTATION).

Implementation: final refinement of a MACHINE. An implementation makes only use of B0 language.

Machine: abstract machine that describes services (OPERATIONS) provided by a component. OPERATIONS signature have to be the same (name, returned values, input parameters name, type and order) among specification, refinement and implementation.

Mathematical modelling: in a B project, see B modelling

Refinement: a model that is less abstract (more concrete) than the component specification.

PatchProver: A file containing user rules that enriches the RB used to process the proof obligations of a project.

Pmm: A file containing user rules that enrich the RB used to process the proof obligations of a component.

Proof obligation: logic predicate produced by Atelier B from a component (machine, refinement, implementation), written in the B language and that needs to be proved to guarantee the soundness of this component.

Rule base: Set of mathematical rules written in the theory language that are necessary for the prover to achieve proofs.

System level properties modelling: idem B modelling, while putting the stress on the property-based approach