Contact

Atelier B 4.5

 Atelier B tool

Why use Atelier B?

> Free download
> Distribution Policy
> Maintenance Contract
> Universities teaching B in France

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 baseline:

> Availability of the tool in Linux, 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 well-definedness: automatic, integrated creation of a well-definedness project associated with a main project to validate the well-definedness .

> Addition of improved proof tools for mathematical 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.

More informations about "Atelier B tool"

Copy link
Powered by Social Snap