Atelier B 3.7 offers numerous improvements with major Atelier B functionalities in order to facilitate the developer’s work:
- User interface: size of project names, improvement of the make command, more permissive project archiving, changes in the user interface banner, refreshing of project and component lists, non-proven component status, incomplete project status, addition/deletion of components, project list filters, pmm file management, specific file archiving, graphic resources per user.
- Proof: automatic proof cut-off time, creation of new commands and aliases, more effective proof monitor mechanisms, concatenation of User-Pass theories, trace mode for ApplyRule, facilitating of the reuse of demonstrations, optimised proof obligations generator.
- System: passage from .db files to text mode (format xml), modification of the licence management system, improvement of dependency management, local project library management.
IMPROVEMENTS IN THE USER INTERFACE:
- Size of project names
- Improvement of the make command
- More permissive project archiving
- Changes in the user interface banner
- Refreshing of project and component lists
- Non-proven component status
- Incomplete project status
- Addition/deletion of components
- Project list filters
- Pmm file management
- Specific file archiving
- Graphic resources per user
CHANGES RELATED TO PROOF ACTIONS:
- Automatic proof cut-off time
- Predicate prover cut-off time
- Creation of new commands and aliases
- Improvement of the proof monitor
- Concatenation of User Passes
- Trace Mode for ApplyRule
- Improvement of the proof obligations generator
- Mhyp, Mgoal, Shyp, Sgoal commands
SYSTEM IMPROVEMENT:
- Passage from .db files to text mode
- Simplification of the .db file/improvement of dependency management
- Local project library management and modification of the license management system