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