Date of diffusion: january 2010
New Functionalities / Characteristics:
Atelier B 4.0.2 has been released on January 7, 2011 and may be downloaded by Atelier B 4 maintenance contract holders. This release brings 84 bug corrections and 14 new features. Among these features, we can mention:
- The interactive prover displays pending goals. Remaining proof work may now be evaluated with more precision.
- Generation of coverage and exclusivity proof obligations: these proof obligations allow to demonstrate the liveness (coverage) of a system model, and to check that at most one event is enabled in each state of the system.
- Tool for validating user added mathematical rules: this tool provides an unique interface for managing and validating mathematical rules. Moreover manual demonstrations may be typed in which will be saved as comments in the pmm file. The tool provides a view per project and per component, and is also able to generate a validation report.
- Spell-checking B model comments: incorrectly spelled words are identified in the B model editor. A contextuel menu allows to choose a correction among several proposals. Pre-installed languages are English(GB, US) and French (France, Belgium, Canada).
- Support for hexadecimal numbers.
- Mathematical rules displayed in the view “Theory List” are sorted according to their applicability (holding guards are written in bold).
- B model editor informs the user when the edited file has been modified on the disk.
- Addition of a search function “à la grep” enabling the searching of strings among all models of a project.