# 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


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://b-method.gitbook.io/training-resources-for-atelier-b/additional-resources/glossary.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.