Version – 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.