B Language Reference Manual
B Language Keywords and Operators
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.
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.