# 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.

**: 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.**

*Basic machine***: 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***: tool to verify that an implementation complies with B0 constraints, that it is effectively implementable**

*B0 checker*

*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).**

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

*Implementation***: 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.**

*Machine***Mathematical modelling**: in a B project, see B modelling

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

*Refinement***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

****