History of the Versions

Versions...

• Atelier B 4.0
• Atelier B 4.0 beta
• Atelier B 3.7.2
• Atelier B 3.7.1
• Atelier B 3.7.

Atelier B 4.0

Date of diffusion: february 2009
New Functionalities / Characteristics:

• Availability of the tool in Linux, Solaris, Mac OS X and Windows, thanks to the development of the graphic interface in the Qt environment and the transfer of the Atelier B core tools.
• New graphic interface that offers, in particular:
• An all-in-one overview of the projects and their status, a better integration of error messages.
• The inclusion of a task distributor: the development tasks (type verification, generation of proof obligations, automatic proof, code generation) can be distributed among a pool of servers. The interface allows for the adding, deleting and interrupting of these tasks.
• A reworked proof interface with better management of the proof arborescence, simplified access to proof commands, the addition of user rules and the syntaxic analysis of formulas.
• An editor with browsing and automatic completion that supports the B Language and Event-B.
• Integration of the proof of the proper definition of models: automatic, integrated creation of a proper definition project associated with a main project to validate the proper definition of models
• Addition of improved proof tools for rules
• Addition of an automatic refinement tool (BART)
• Addition of a B0 implementation translator towards the language (ComenC)
• Event-B support with syntaxic controls and the generation of specific proof obligations
• Addition of a simple, effective means of interfacing with external tools.

Atelier B 4.0 beta

Date of diffusion: september 2008
New Functionalities / Characteristics:

• New supported operating systems: Mac OS X and Windows (in addition to Linux and Solaris)
• New graphical interface proposing:
• the integration of the parallelisor (tasks are distributed over networked computers)
• a redesigned proof interface
• an editor with navigation and automatic completion
• Integration of the well-definedness proof obligations
• Addition of an automatic refiner tool (BART)

Atelier B 3.7.2

Date of diffusion : may 2008
New Functionalities / Characteristics:

The future version 3.7.2 is currently under development and is announced for early May 2008... A new translator ComenC will be added to Atelier B. ComenC allows for B0 implementations to be translated into C language.

This translator is a result of a convergence between industrial translators and research works, such as the RNTL BOM (optimized B memory) project.

In comparison to prior translators, the ComenC translator offers a simple translation for a more efficient code, closer to the original B0.

Atelier B 3.7.1

Date of diffusion : 07/03/2008
New Functionalities / Characteristics:

Version 3.7.1 corrects certain anomalies present in version3.7. The corrections introduced are as follows:

• Graphics interface: duringexit from the proof interface, the dialogue box asking if the demonstration should be saved blocked the interface.
• EMACSPRI interface: compatibility problems with version 3.7 have been corrected.
• Prover: the "search rule" command now correctly searches for the rules in the .pmm files.
• Type checker: Duringthe adhesion of constant abstracts via homonymy, the type-checker picked up an error, whilst this construction is permitted by the B language.
• User tracking moderules: in certain instances the use of the user tracking mode rules were able to finish off the prover.
• The BASIC-IO machine from the LIBRARY project does not allow generation of the code.

Atelier B 3.7

Date of diffusion: 07/18/2007
Characteristics:

Atelier B 3.7 offers numerous improvements with major Atelier B functionalities in order to facilitate the developer’s work:

• User interface: size of project names, improvement of the make command, more permissive project archiving, changes in the user interface banner, refreshing of project and component lists, non-proven component status, incomplete project status, addition/deletion of components, project list filters, pmm file management, specific file archiving, graphic resources per user.

• Proof: automatic proof cut-off time, creation of new commands and aliases, more effective proof monitor mechanisms, concatenation of User-Pass theories, trace mode for ApplyRule, facilitating of the reuse of demonstrations, optimised proof obligations generator.

• System: passage from .db files to text mode (format xml), modification of the licence management system, improvement of dependency management, local project library management.