MADE IN FRANCE

Online Documentation

ATELIER B

Installation Guide

This guide provides instructions for installing Atelier B 4.7.1 Community Edition. It covers Windows, Linux and MacOS platforms.

 

B, EVENT-B

B Language Reference Manual

The B Language Reference Manual describes the B language supported by the Atelier B version 4.7.1 tool. It is primarily intended for users who carry out developments using the B method, but also for anyone wishing to discover the possibilities of the B language.

B Language Keywords and Operators

This table contains the operators and keywords of the B language, their ASCII and mathematical representation, and their priority level.

Type Checker: Error Message Manual

This manual presents the various error and warning messages of the Type Controller. Its purpose is to specify the origin of the errors for each message in order to help the user: once the cause has been correctly identified, it is easier to correct the specification.
For complete and detailed information, please refer to the B Language Reference Manual.

PROOF

Atelier B Open Resources

This GitHuB contains:

  • A very large number of proof obligations stored in POG files
  • A SMTLib-2.6 translation of these proof obligations, stored in SMTLib-2.6 files. The translation was carried out using ppTransSmt.

CODE GENERATION

EXTENSIONS

Atelier B is an extensible tool. It is possible to connect third-party tools that interface with the files used and/or generated by Atelier B, via extension points. These extension points can be used to add menus to the Atelier B user interface. Finally, the file formats used to store models and proof obligations, and to interact with third-party proofers, are all public and XML-based.

BXML Schema Documentation

This document describes the BXML format, which is an XML representation of a B or Event-B component.

PO XML Schema Documentation

This document describes and illustrates the POG format: an XML representation of the proof obligations of a B or Event-B component.

Proof Mechanism XML Schema Documentation

This diagram defines the format of the proof mechanisms. In Atelier B, proof mechanisms are descriptions of how automatic proof programs (provers) should be applied to proof obligations.