Download Atelier B Translators

Chapter 4
Operating scenarios
4.1
4.1.1
Developing a native B project
Principle
This section provides an example of a native B project, used to illustrate the following
aspects of the development of such a project:
• Influence of the translation into Ada on the architecture of the written B code.
• Unitary translation of B project modules.
• Project linking.
• Compiling and executing the generated code.
The detailed operating information for the Translator will be given by the screen captures
of the Atelier B GUI∗ .
4.1.2
Informal Example Specifications
The purpose is to test the handling of an integer stack. To do this, several modules are
written:
• A module that initializes a stack of a given size and which allows to push an element
on the stack, or to pop it from the stack.
• A module that displays a stack.
The example will have to create two stacks of different sizes and use the display of their
contents to prove that the stacks are correctly initialized and that the push and pop
procedures work.
Important remark: This example, and the B source codes presented below for its implementation, do not pretend to be perfect examples of B language. It is not intended as a
B language design style example, but simply a complete project creation example, with
translation into a target language followed by the execution of the product code.
19