> For the complete documentation index, see [llms.txt](https://b-method.gitbook.io/training-resources-for-atelier-b/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://b-method.gitbook.io/training-resources-for-atelier-b/additional-resources/glossary.md).

# 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