Contact

Version 4.5.1 of Atelier B for Mac-OS

Version 4.5.1 of Atelier B for Mac-OS

Atelier B 4.5.1  is a Community Edition version, freely downloadable

This installer allows the execution of AtelierB 4.5.1 on macOS 10.15, called “Catalina”

We remind that 4.5.1 version improves the following functionalities :

  • Simplified installation with Linux
  • Proof Obligation Generation
    • For Event-B, specific proof obligations may be generated by the new proof obligation generator: deadlock freeness, non-divergence, feasibility, coverage and exclusivity
  • Automatic proof
    •  Interfacing tool « IAPA » (Linux only) to connect with provers from Why3  platform
  •  Interactive proof
    •  Release of proof drudges, which let user use SMT solvers to define proof rules
    • New feature to add its own groups of proof commands
    • Improvement in typing of proof commands
    • Configurable timeout added to proof commands belonging to pp family
    • A new proof command added to Apply Tactic
    • New functionalities in the proof tool to prove rules
    • Integration of ProB model checker in the interactive prover
  • C4B code generator now supports arrays indexed by enumerated type variables
  • Editor now displays proof obligations
  • Coding rules are now verified in the Atelier B

New functionalities of the versions 4.4.2 and 4.3 are described in their respective version notes (release notes 4.4.2 , release note 4.3 ).

If you require more detailed information please refer to the 4.5 release notes

You will also like:

Copy link
Powered by Social Snap