The new version 4.4.2 of the AtelierB toolset for the B method has been released. This comes with numerous bug fixes and several feature improvement that will be introduced. The most interesting feature is probably the new capability of proof obligations visualisation and management directly within the editor. We have also two new capabilities for the interactive proof and additions to the proof rules management tools.
Proof Obligation Management from the Model Editor
There is a new possibility to explore the relationship between a B model and its proof obligations (PO). We can now visualise the PO and their status along the text source and directly in the editor. This ability comes with the complete traceability information produces the new proof obligation generator.
This feature must be activated in the preferences of the editor, as it can be slow on a large model. Once activated, the editor will come with two columns aside the text which show the PO associated to the visible lines and the PO of the whole model. The proven status of the PO is indicated with colours and one can see a particular PO in detail.
When the model is modified, the PO generation and automatic proof are launched by AtelierB in the background; therefore it is possible to work completely with the editor as long as no interactive proof is required!
The full traceability of formulas is also there and so you can check exactly where, in the PO, some parts of the model are involved by a simple selection of the source text. Moreover, the traceability from the PO formulas to the source code is available as well. Those two capabilities are a powerful tool to help understanding how properties are proven (or dismissed) in a B model.
Proof Mechanism Improvement
Two new features for the interactive proof tooling of AtelierB have been implemented.
It has been always possible to precisely set the timeout of the “PP” prover by adding a parameter in the textual command. Now it is also systematically done with the graphical commands and the timeout is adjustable with a field box next to the PP icon. This is important to limit the proof replay time of your project as the PP prover can be slow to terminate.
The second proof enhancement comes with the capability to write down custom pieces of proof commands in a new special section called “User_Tactic” in the “PatchProver” file. You can then launch this kind of macro proof command with the new command “at” (Apply Tactic) during an interactive proof. The “at” command in itself disappears in favour of the actual commands in order not to introduce proof replay failures if the “User_Tactic” section is modified afterwards.
New features of the proof rules management tool (only in the maintenance edition)
In the maintenance edition of AtelierB, there a tool helping to demonstrate and validate the proof rules (written by the modeller in order to make possible and faster the proof of a B model). This tool allows an efficient management of the numerous proof rules used in industrial projects.
This new version comes with a better detection function of duplicated rules of a project. For some technical reason, rules are often copied over several component files and this new function can identify and manage sets of duplicated rules requiring only one user action per set of rules.
We can also now extract a file report on the rules that still need be worked upon. And the tool can research and delete a set of unused rules (a theory). Finally it has a better capability for the sorting and tagging of invalidated rules during the verification work.
For more information about the new features and how to use them, please refer to the release notes. You can also directly contact the AtelierB team at atelierb@clearsy.com.
If you require more detailed information please refer to the release notes