Date of diffusion: december 2012
New Functionalities / Characteristics:
Atelier B 4.1.0 (Community Edition and Maintenance Edition) has been released on December 11, 2012.
This realease brings 385 bug corrections (37 for 4.0.1, 79 for 4.0.2, and 269 for 4.1.0) and 56 improvements (5 for 4.0.1, 13 for 4.0.2, and 38 for 4.1.0). Among these features, we can mention:
- Support for « data validation » project
- Improved support of integers : maximum implémentable value (MAXINT) can be 16, 32 or 64 bit-wide, integer litterals are not bounded (BigINT)
- Experimental support of real numbers
- Experimental support of floating point numbers
- Support of hexadecimal litterals.
- New C code generator, C4B, with translation profile and makefile creation.
- Localization of the software in English, French, Japanese, and Portuguese.
- Support of Unicode. Identifiers, strings and comments may contain non-ASCII caracters.
- Addition of a components status graphical view
- Parallel execution of proof tasks: firing a proof action several times leads to parallel execution of these tasks. Additional informations, such as the order of execution of thses actions, are displayed
- Improved Integrated Editor : Ctrl-D to delete a line, better indentation, addition of a list of open files, tunable syntaxic highlighting, model navigation (jump to definition, abstraction, or refinement).
- 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 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 a 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).
- 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, with the help of regular expressions.
- Added rules when using the command “pc” are now displayed.