Why use Atelier B 4 ?


> Free download
> New Distribution Policy
> New Maintenance Contract
> Universities teaching B in France
> Nouvelles fonctionnalités

New functionalities

Atelier B 3.7 went through numerous improvements and changes to finally become Atelier B 4. Here is an overview of the main changes in this new version:

> 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 tree, simplified access to proof commands, the addition of user rules and the syntactic analysis of formulas.
An editor with browsing and automatic completion that supports the B Language and Event-B. (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 syntactic controls and the generation of specific proof obligations

> Addition of a simple, effective means of interfacing with external tools.