Home

Atelier B 4

1. 5 2 2 Workspace Modifications It could be interesting for the user to modify the workspaces properties This is possible by triggering the Workspace gt Properties menu or via a right click on the desired workspace AtelierB View Project Refresh Close Remove Restore project You will then get access to the following configuration dialog ClearSy 60 Atelier B 4 User manual ClearSy 5 2 Managing workspaces Properties for workspace atb bbatch servers krt commands resource file Workspace name atb Workspace database directory Mhome pmauduit AB Connect automatically at startup Configuration Details Cra Here we find back the properties already seen while creating a workspace excepted the remote or local aspect The Configuration Details button will give you information on the version of the different tools installed e The Servers tab allows you to specify remote servers which can execute in parallel different tasks on B Projects e The krt contains some controls about the Atelier B kernel the krt binary e The Commands tab allows you to configure some tools the Typechecker xref the PO Generator the prover the predicate prover the lemmas prover and the Delta Component e The Resource file tab lets you the ability to tweak your resource file and is meant to be used by advanced users Please consult t
2. e The reference value for each metric e The list of metrics to display in the project report the project report is a table that contains metrics for all the project implementations e The list of metrics to display in the implementation report the implementation report is a table that contains metrics for a specified implementation ClearSy 93 Atelier B 4 User manual ClearSy 6 7 Extracting Metrics e The list of metrics to display in the operation report the operation report is a table that contains metrics for an operation in a specified implementation The user can use the configuration files provided by Atelier B or create his own configuration files The configuration files supplied with Atelier B are located in the AB press lib LC directory The files have a cvl extension Example of a project report A RL htc Fri Hoi Name 1 1 2 3 4 5 6 A A A ene ae Pi Poio Homo PGS Se tant E Reference Values 500 100 10 3 2 100 Hocipolpispisngcldsias teninden Pacer esisns eecebeSe Feceeesses Distributor_imp 14 12 1 2 1 5 Poesicbsoemsatetecsos Husrac nos toeseeksce tscesdsuss dodosaesat Screen_imp 13 6 1 141 1 A cls Htc dolia ocetecs ce Harahan Honilaisn Ficinia 1 NB_INST_OPER 2 NB_INST_SEQ 3 NB_CTRL_SEQ 4 NB_CTRL_IMB 5 NB_WHILE_IM
3. 18 Lob ach blow ee eed ee ek eae ak Skee eee Ee 20 21 Sul terraces acct Sak Me al oe eo he Oe hh ok ete Beek at de dl ee ao ee he al 21 ClearSy Atelier B 4 User manual ClearSy CONTENTS 32 MamGUll 3 3 BAMTOT soes ke ce ee ee 3 4 Command Mode User Interface 4 Quickstart guide 4 1 Projects management 4 1 4 Opening and Closing a B Project 4 2 Projects Advanced usage 4 2 1 Users management 4 2 2 libraries management 4 2 3 Definition files directories Management 4 2 4 Archiving a project 4 2 6 Reading Properties of a Project 4 3 Components Management 4 3 1 Adding a Component 4 3 5 Editing a Component 4 3 6 Restoring a Component 5 Applying the B method se eee ee ed 5 2 Managing workspaces ClearSy Atelier B 4 User manual ClearSy CONTENTS 5 2 1 creating a Workspacel ee 98 5 2 2 Workspace Modifications 2 60 5 2 3 Deleting a Workspacel ee 62 5 2 4 Opening and Closing a Workspace oaoa aaa o 62 5 3 Syntax analysis and Typecheck oaa a 63 5 4 Automatic refinement 0 0 00000 a 66 5 5 Generating Proof Obligations 2 0 0 ee 66 5 6 Displaying Proof Obligations 2 2 2 0 000 a 69 SAREE a a BOG he GE ee wes eae eR By 71 E A e oe ese ae Bs 73 poset a a ey SoG SA Ge de ee wee pee we ae By 73 5 10 Checking the Translatable Language BO 74 5 11 Project Checking ce e A nae ee Ge 77
4. This function accepts five optional parameters own If this parameter equals 1 only the components that you are manager of are displayed mch If this parameter equals 0 the machines are not displayed ref If this parameter equals 0 the refinements are not displayed imp If this parameter equals 0 the implementations are not displayed name This parameter allows to filter the list by component names Use the character For example to display all components with a name starting with a S letter specify the S value Examples To obtain the list of the components that you manage bbatch 2 gt sml 1 Printing Own machines list B_Site_central Card Card Card_imp Keyboard_code Keyboard_code_ref End of machines list ClearSy 92 Atelier B 4 User manual ClearSy 4 3 Components Management To list machines only bbatch 2 gt sml 0100 Printing machines list B_Site_central Card Card Keyboard_code End of machines list To list only machines with a name starting with K and ending with code bbatch 2 gt sml O 1 0 O K code Printing Own machines list Keyboard_code End of machines list 4 3 4 Reading Information on the Components Description This function displays the following properties of components e The entire access path of the B source file e The type of the component machine refinement or implementation Graphical user interface In order to obtain information on a component y
5. A eos a ie Hs eet we ae he amp GO eG ee ee nae E a We 78 5 13 Applying a Tool to all the Components of a Project 0 79 5 14 Updating a Project 4 ge 4 ed ee eee Ee eee ae Ye ee es 80 Seo teh veo pee Bae Hea ae a en ote A ge Bee 81 5 16 Dependencies Management 81 83 A 83 el ar Ass eE a ad e 84 RE Sf Bhs As e as aa de 85 6 4 Dependency Graphs ee 87 6 5 Operation call graph 2 ee 90 6 6 Cross References s a ieat da a ba Re ae Bee e e ae ra oe 91 6 7 Extracting Metrics e 93 ClearSy Atelier B 4 User manual ClearSy CONTENTS 98 A E A A A A A 98 E A a A pa Ae E 98 101 Ca end A Go cd a cdo o de a de A 101 AN a A a a A 101 SN A A o Se A ee tee 102 A adh ei os A 103 ates A a a oe ee NA 104 Ae ey Bek oy tne oe ees 2 105 iy Bayo Bet ee hae ee ae 106 8 8 Configuring the Printing Script 2 aa 0000002 ee ee ee 106 Appendix 108 Limitations of Project Documentation Tools 0 0 0 000000 ee ee 108 Files created by the Atelier B 2 0 a 109 ClearSy Atelier B 4 User manual ClearSy Introduction 1 Introduction 1 1 About this document This documents aims to introduce the different features provided by the Atelier B tool Atelier B is a set of tools allowing developping applications using the B method Atelier B helps the designer in the formalisation of its application e By automatically executing actions relevant to the B method
6. e automatic demonstration of POs e interactive demonstration of POs that are not automatically demonstrated translatable language checking translating implementation into one of the following programming language C C ADA or HIA The presentation of these commands assumes that the reader is familiar with the B method This manual therefore only covers the implementation conditions for the functions listed previously and not their aims in relation to the method In the basic version of Atelier B translation to standard computer languages ADA or HIA is not included The ADA or HIA translators must be installed separately ClearSy 57 Atelier B 4 User manual ClearSy 5 2 Managing workspaces 5 2 Managing workspaces This section is useful only if you intend to use the GUI since workspaces do not exist into the command line interface While using the Command line interface you need to parameter a specific configuration This is why the notion of workspace appear in the current version of the GUI a workspace is a kind of configuration for the Command line interface which will be used by the GUI After having installed the Atelier B a default workspace is automatically created and allows you to directly begin to develop By the way it is possible to tweak your configuration by creating a new custom workspace 5 2 1 creating a Workspace The workspace creation can be done into the GUI via the following menu Vie
7. the interpreter stores the last project name entered In the same way the interpreter stores the last component name entered To use this default parameter simply type lt return gt Example bbatch 3 gt typecheck MM_1 bbatch 4 gt pogenerate pogenerate MM_1 yes return Using Interactive Help The help command displays the list of commands available This list is displayed in the following format General commands cd change directory v version print Project level commands add add definitions directory apl add project lib spl show projects lists Machine level commands available after open_project aa ada all a adatrans af add file ani animator s status sg status global t typecheck u unprove The commands are presented in the following order 1 General commands ClearSy 26 Atelier B 4 User manual ClearSy 3 4 Command Mode User Interface 2 Project management commands 3 Commands that apply to components A project must be opened to be able to use these commands Command abbreviations are indicated within parenthesis before the command name You can also obtain help on a specific command by typing the command help command_name or h command_name For example bbatch 9 gt help help help command get help on commands ClearSy 27 Atelier B 4 User manual ClearSy Quickstart guide 4 Quickstart guide The next chapters of this do
8. 1 5 Conventions 1 5 Conventions Each feature provided by Atelier B is presented in the following way e A Description section describes the main characteristics of the command e A Graphical user interface section that shows how the command can be used through the graphical user interface e A Command line interface section that describes the command through the Atelier B batch mode e An optional parameters section documents the ressources that can be used to modify the behaviour of the command The parameters are described as follows Example Comment ATB POG Generate_ Obvious _ PO name of the ressource Configured during Atelier B installation default value Generate obvious proof obligations or not Ressource description Within the graphical user interface description all the labels of buttons are written in italic For instance the Help button ClearSy 9 Atelier B 4 User manual ClearSy Installation 2 Installation This document describes the procedures to follow to e Install Atelier B e Configure and parameter Atelier B We recommend that you read the entire document before starting the Atelier B installation procedure Some specific kind of installation must be performed by the system administrator as some operations must be performed by the super user creating login accounts etc The first part contains all the information necessary for selecting the machine and th
9. Atelier B 4 User manual ClearSy 2 1 Preparing the installation 2 1 9 Users of Previous Version If you already have a previous version of Atelier B installed you must install the new version in a different directory or in a different sub directory of the previous directory Please refer to chapter 2 3 of this document Note that if you tried a beta version you may will have to uninstall it before trying to install the current release 2 1 10 Installation on a Read only Partition If for greater security you choose a disk partition that is mounted on other machines in read only mode you must follow a specific procedure when installing Atelier B By default Atelier B uses a directory where the users must be able to write files These files contain information on the projects created by the users This directory named bdb represents the Atelier B data base By default this directory is located in the Atelier B installation directory If the installation partition is read only you will have to use an Atelier B data base on another disk partition ClearSy 14 Atelier B 4 User manual ClearSy 2 2 Installing Files 2 2 Installing Files This section describes the Atelier B installation procedure and its options for a workstation or a server 2 2 1 Windows For this operating system installation is fully automatic Zax Welcome to the Atelier B Setup Wizard This will install Atelier B 4 0 Beta on your comput
10. B method We will describe in details in the following this graphical user interface ClearSy 21 Atelier B 4 User manual ClearSy 3 2 Main GUI 3 2 Main GUI The main GUI looks like the following screenshot The main objective of this interface ClearSy Atelier B eaha AtelierB View Workspace Project Component Help YO voo UN ooo o oog Workspaces e e y atb Welcome to Atelier B Please select from the following sections where you would like to start O CLETATTO New Projects Atelier B 4 0 in a nutshell Create a Project Software Developement leb Sites Create a Project System Modelisation Atelier B eu Recent Projects BMethod com Tools clearsy com e uevol320 library e lib2 e lib e library zc Ate er B svn Copyright c 2008 ClearSy System Engineering Errors amp Tasks amp Servers amp Errors 0 ViA Warnings 0 Hide Finished tasks J ES E fam iocamos Message Location Component Project Component Action Status la B T No errors is to facilitate and optimize project management tasks 22 Atelier B 4 User manual ClearSy 3 3 Editor 3 3 Editor Atelier B furnish a specific editor specially customized for B component edition It proposes fonc tionnalities like completion error underlining etc It looks like this Ploc occupancy me Atelier E File Edit View Search 400009090 block_occupancy_1_it_i block occup
11. E gt a block_occupancy 1 OK OK 7 7 0 Q block_occupancy_1_i OK OK 33 21 12 block_occupancy_1_it OK OK 6 6 o Q Dlock_occupancy_1_it_i OK OK 19 9 10 block_occupancy_2 OK OK 5 5 0 Q Dlock_occupancy 2 i OK OK 31 18 13 Dlock_occupancy_3_i OK OK 12 5 T block_occupancy_4 OK OK 4 4 0 l block_occupancy 4i OK OK 2 0 2 E ClearSy 84 Atelier B 4 User manual ClearSy 6 3 Component Status We can notice that the columns may vary depending on the use of the interfaces and the user prefer ences Command line interface The user interface is started up you already have opened a project To obtain the project status type the following command status_global or 58 6 3 Component Status Description A component with the B method applied on pass through several states Modified after modification of the component source Parsed after a syntax analysis of the component TypeChecked after type checking of the component POGenerated after generating of component proof obligations AutoProved after an automatic or interactive demonstration of all the proof obligations of the component These states are exclusive A component loses its Modified state as soon as it is successfully type checked This function displays the component state as shown below Printing the status of QUERY QUERY TypeChecked home project spec QUERY mch End of Printing the status If the component is the POGenerated status t
12. FALSE Perform or not expression syntax checks ATB COMP Disable_ Formal_ Params_ Type_ Check FALSE Perform or not type checks of formal parameters ATB COMP Disable_ Variables Initialisation_ Checker FALSE Perform or not variables initialisation checks ATB COMP Disable_ Locale_ Variables_ Type_ Check FALSE Perform or not variables type checks ATB COMP Disable_ Operation_ Input_ Parameters_ Type_ Check FALSE Perform or not operation input parameters type checks ATB COMP Disable_ Operation_ Output_ Parameters_ Type_ Check FALSE Perform or not operation output parameters type checks ATB COMP Disable_ Parameters_ Instanciation_ Check FALSE Perform or not machine parameters instanciation checks ClearSy 76 Atelier B 4 User manual ClearSy 5 11 Project Checking ATB COMP Disable_ Predicate_ Syntax_ Check FALSE Perform or not predicate syntax checks ATB COMP Disable_ Valuation_ Check FALSE Perform or not VALUES clause checks ATB COMP Enable_ Typing_ Identifiers FALSE Variables of array record or interval type must be typed with an identifier if this resource is TRUE special case for HIA translations 5 11 Project Checking Description This function only available via the command line interface performs checks on all
13. Once a source file has been attached to a project the user analyses which components are contained in the file and permit the management of these components Atelier B only accepts as B source files those whose name ends in one of the four following suffixes mch ref imp mod The contents of each type of file is as follows e A file named Ident mch must contain one and only one component an abstract machine named Ident e A file named Ident ref must contain one and only one component a refinement named Ident e A file named Ident imp must contain one and only one component an implemen tation named Ident e A file named Ident mod must contain a component named Ident It can also contain the refinements of this component as well as modules an abstract machine and all its refinements imported by the implantation of the component Finally for each module present in the file the modules imported by this module can also be present A suffix file mod permits the storage in a single file of a B module or a sub part of the project made up of a module and the modules imported by this module If the contents of the files do not respect these rules the file will still be attached to the project An error message is then displayed in the start up window No other operation will be possible on the component before its correction Graphical user interface The GUI is launched and a project is opened In order to add componen
14. be positioned ATB BCOMP Enable Typing Identifiers TRUE It is easier to save this resource in the project resource file of the projects wich will be translated into the HIA language Graphical user interface The user interface has already been started up a project is opened To check the translatable language on the components perform the following operations 1 Select the components from the list of components 2 Use the Component gt BO check or directly the keyboard shortcut Ctrl B The result of all checks is displayed component by component in the start up win dow If there is an error on one of the components an error message is displayed in the er ror view A double click on the error will then open the internal editor if configured as the default editor at the error location Command line interface The user interface is started up you already have opened a project To BO check component comp_name type the following command bOcheck comp_name or bOc comp_name ClearSy 75 Atelier B 4 User manual ClearSy 5 10 Checking the Translatable Language B0 Usable Parameters ATB COMP Disable_ Array_ Compatibility _ Check FALSE Perform or not compatibility checks of array indexes ATB COMP Disable_ Concrete_ Constants_ Type_ Check FALSE Perform or not type checks of concrete constants ATB COMP Disable_ Expression_ Syntax_ Check
15. files present in the project data base directory files present in the translation directory When all the project is archived all data is stored As a result when the project is restored refer to sub section 44 2 5 the user will retrieve it in the same state and will not have for instance to type check again what was already type checked Graphical user interface In order to archive a project with the GUI it is necessaryn after having opened the workspace containing the project to archive to click on the given project and to select into the menu Project gt Archive A wizard is displayed then Archive project Archive destination file tmp archive tar gz Parameter Source files e Whole project gt Sources and Proof files lt Back Next gt Cancel Select a destination file and the different parameters needed then click on the Nezt button ClearSy 42 Atelier B 4 User manual ClearSy 4 2 Projects Advanced usage Command line interface The user interface is already started up To archive a project use the archive or arc command This command has three parameters e The project name e The path to the archive file e The type of archival O B source files archive 1 entire project archive 2 B source and proof files archive Example To archive the entire project proj_name type the following command archive proj_name home project tarPROJ arc 1 The
16. have at least 512 Mo of RAM The necessary memory space is strongly dependent of the other applications running on your work station and of the size of the developments made with Atelier B 2 1 4 Disk Space Requirements To install Atelier B you need about 100 Mo of disk space The disk space occupied by a project developed with Atelier B depends on the size of the B source files The disk space occupied by the files generated automatically by Atelier B equals about 25 times the disk space of all the B source files 2 1 5 External tools Atelier B produces files that can be worked on with the following tools Tool Version Type Vendor TEX 2E Word processor Free software PDFLaTeX 3 Word processor Free software Word 7 or greater Word processor Microsoft Moreover for certain fonctionnalities it couls be usefull to install some free external tools e Dot furnished with GraphViz e A SSH client OpenSSH or Putty for Windows userd be Visit See ClearSy http www graphviz org http www chiark greenend org uk sgtatham putty download html for more informations 11 Atelier B 4 User manual ClearSy 2 1 Preparing the installation E lo Disk Server Machine Server Disk server AB bbin linux solaris Machine with Machine with Linux Solaris Figure 1 Example of a network system You can use Atelier B with
17. links are displayed Library components filtering The user may choose between several options for the components linked to the project and that are in a library The options available are Show All In this case the components present in libraries are handled in the same way as the other components If these components depend on other components they will also be included in the graph Show In this case only components directly linked to project components will be displayed If these components depend on other components they will not be displayed Group In this case all the components in the same library are combined in the same node of the graph Hide In this case the components present in libraries will not be displayed For all components present in libraries the library name is given in brackets Components not linked filtering The user can choose to not see the isolated components in other words the components that are not linked to other components Instanciation graph The user can choose to visualise only the instanciation graph in other words only the IMPORTS links between the different modules Dependency graphs can be included in the documentation automatically generated by Atelier B refer to section A Graphical user interface The GUI is already launched a project is opened To obtain a dependency graph the user have to perform the following operations ClearSy 88 Atelier B 4 User manual C
18. on specifications and refinements e By providing helper services not directly required by the B method but necessary for industrial developments such as management analysis and documentation of a project 1 2 Objets handled by Atelier B In this section we are introducing the main objects handled by Atelier B Component File that contains a source written in the B language It is the basis of a B develop ment component is a generic term that can correspond to a B specification abstract machine a refinement of this specification its implementation last refinement level Writing B component is performed by using the text editor of the workstation Project Set of files components external C C HIA or ADA sources makefiles that are used or created during the development of an application using B completed with additional information used by Atelier B see BDP User It is necessary to define a list of users that are allowed to access and modify the project Note that all users have the same access rights and that at least one user should be provided Project Database BDP All the internal information required for the correct execution of Atelier B tools are stored in a directory called BDP This directory also contains files created by the Atelier B documentation tools ClearSy 6 Atelier B 4 User manual ClearSy 1 3 Atelier B user interfaces 1 3 Atelier B user interfaces In this
19. performed NB_SEE_MACH NB_IMPORT_MACH NB_MACH_EXTEND NB_ENUM_SET NB_ABSTR_SET NB_ENUM_ITEM NB_MACH_PAR TOT_NB_ENUM NB_CONC_VAR NB_OPER NB_CONST NB_LOC_VAR NB_INPUT_PAR NB_OUTPUT_PAR NB_INST_OPER NB_NEST_CTRL NB_SEQ_CTRL NB_NEST_WHILE NB_SEQ_INST NB_VAR_IN LG_PREFIX LG_PAR_MACH LG_IMP LG_INPUT_PAR LG_OUTPUT_PAR LG_SET LG_ITEM_SET LG_CST LG_CONC_VAR LG_LITERAL LG_LOC_VAR LG_OPER LG_OPER_MACH LG_CONDITION SZ_ARRAY NB_OP_PROMUE SZ_CONC_VAR SZ_CST number of seen machines number of imported machines number of extended machines number of enumerated sets number of abstract sets maximum number of elements in a enumerated set number of machine formal parameters total number of enumerated elements number of concrete variables number of operations number of concrete constants maximum number of local variables per operation number of input parameters per operation number of output parameters per operation total number of instructions in an operation maximum number of control statements nested in an operation maximum number of control statements in sequence in an oper ation number of nested whiles number of instructions in sequence in an operation number of VAR IN in an operation maximum size of rename prefixes maximum size of a machine parameter implementation name size maximum size of an operation input parameter maximum size of an operation output parameter maximum size of a set id
20. performed uselessly the interface detects it and asks then the user for a confirmation In example the following question could be asked to you after a Typecheck Typ echecker p Select components are all already typechecked N Do you want to force typechecking inactive dependance mode CEES Command line interface The user interface has already been started up To stop the management of dependencies and therefore be able to force an action you must type the following command disable_dependence_mode or ddm You can then type your command For example typecheck AA To bring the management of dependencies back into function you must type the following command enable_dependence_mode or edm ClearSy 82 Atelier B 4 User manual ClearSy Analysing B developments 6 Analysing B developments 6 1 Presentation Analysing a B development is a set of commands used to obtain information on the components of a project The analysis commands are used to e determine the status of a project syntax checked proven etc e determine the proof status of a component number of proof obligations per operation etc e create a dependency graph between the components ClearSy 83 Atelier B 4 User manual ClearSy 6 2 Project status 6 2 Project status Description This function is used to create a summary table that provides information on all the components of a project It is used
21. presentation ClearSy 98 Atelier B 4 User manual ClearSy 7 2 Displaying a B Source e use the presentation supplied by Atelier B Normal comments are deleted from the B source file only the comments enclosed between and character sequences are retained Graphical user interface The GUI is already launched and a B project is opened 1 Select the desired component into the components list 2 Trigger the Component gt Save as menu The following dialog is then displayed Save component as jea Save as pdf rtf latex Show with default application 10 Cancel Select the export options then finally click on the Ok button Command line interface The user interface is started up you already have opened a project To display convert a B source into a word processor format use one of the following commands e show_doc_latex or sdl This function converts the B source into IAT X format e print_doc_latex or pdl This function converts the B source into TEX format then sends the produced file automatically sent to the selected printer To change the selected printer use the set_print_paramscommand e create_doc_rtf or cdr This function converts the B source into Word format The name of the file produced is displayed in the start up window You should then edit the file using Word or any RTF compliant editor The first parameter for these functions is t
22. project To obtain cross references type the following command get_project_xref or gpx This command includes one or two parameters ClearSy 92 Atelier B 4 User manual ClearSy 6 7 Extracting Metrics 1 The filter on identifiers e 0 for all identifiers of the component specified as second parameter e 1 for on identifier of the current project specified as second parameter e 2 for all identifiers of the project 2 The component for filter O or identifier for filter 1 Examples To obtain cross references for all of the identifiers defined in the component comp type the following command get_project_xref 0 comp To obtain cross references on an identifier ident type the following command get_project_xref 1 ident To obtain cross references for all the identifiers defined in the project type the following command get_project_xref 2 6 7 Extracting Metrics Description This function extracts metrics from an implementation or from all the implementations of the project These metrics are used to measure the complexity of an implementation or of the analysed project check that the implementation or the analysed project complies with programming rules measure the minimum memory size required for implementing the data layouts used in the B sources The metrics extracted are exctracted according to the data present in a configuration file This configuration file contains the following information
23. the Atelier B gt Preferences and to configure your own editor If you select an external editor you will have to give a path to the path as shown below Preferences Component View Use different actions depending on the clicked column Text editing Main window Projects New components Internal Editor Installation v Get status information for each component slower on large projects Text encoding UTF 8 Use the internal editor Use an external editor External editor command xemacs Q Cancel o Command line interface The user interface is started up you already have opened a project To edit the comp_name component a project should be opened then type the following command edit comp_name or e comp_name Usable parameters ATB OPT_TOOLS_ lt SYSTEM gt Editor_ Path Positioned at the Atelier B set up Access path to the text editor 4 3 6 Restoring a Component Description ClearSy 55 Atelier B 4 User manual ClearSy 4 3 Components Management This function is used to restore B source files or definitions files from an archive created using the function described in sub section Restore is performed in the current project If the restored component is not in the current project the function add it automatically If the component is already present in the project it is replaced by the restored component Gra
24. the project com ponents The rules checked by this function are e a machine can only be imported once in a project e aseen machine must be imported by a project component e the SEES clause must be transversal to a component e the dependency graph must not contain cycles e the names of project components must be differents an upper lower case difference is not enough These checks are described in the B language Reference Manual These checks are required to translate the project They are run automatically by Atelier B before project translation Some of these checks are performed automatically before the syntax analysis and the type check of components in order to warn the user as soon as possible The user can also perform these checks on demand by following the procedures described below Command line user interface ClearSy 77 Atelier B 4 User manual ClearSy 5 12 Translating The user interface is started up you already have opened a project To perform the checks on this project type the following command project_check comp_name or pchk comp_name The parameter of this command is the name of the implementation that is the project entry point 5 12 Translating Description In the basic version of Atelier B only the C translator is shipped named ComenC This function translates project implementations into different languages For further information refer to the translators user s manual G
25. with the full path of the new script file The Atelier B is shipped with a printing tool named bprint This script is unavailable from the GUI but could be used via the Command line interface By default the printing script used by the Atelier B is the the script atelierb_ directory AB bbin bprint In order to use another script follow these instructions 1 Create a new script 2 Modify the value of the resource ATB ATB Print _Command in the resource file AB AtelierB by giving the full path of the new script ClearSy 107 Atelier B 4 User manual ClearSy 8 8 Configuring the Printing Script Appendix Limitations of Project Documentation Tools The outputs in Word rtf formats are limited This is due to the abilities of the programs and their formats This functionality should be used with care For the Word output format the limitations are the following 1 The logo is not included in the generated document 2 The table of contents is not generated 3 Be careful when including Postscript files e no check is performed to ensure that the file is present on generation e the file must be present on the disk e Word must recognize Postscript files e The printer must be able to interpret the Postscript 4 The files are intended for PCs and may not be used directly on Macintosh computers ClearSy 108 Atelier B 4 User manual ClearSy 8 8 Configuring the Printing Script Files created by the Atelier B Th
26. ATB ATB TypeChecker_Command TC kin ATB ATB Xref_Command xref ATB ATB Proof_Obligations_Generator_Command PO kin ATB ATB Prover_Command MU kin ATB ATB KParser_Commandpk a m20000 ATB ATB POViewer_Command POV kin ATB ATB Predicate_Prover_Command PP kin ATB ATB BED_Command bed ATB ATB Animator_Command ANLkin ATB ATB Limit_Checker Command checker Dona ela To edit the project resource file open the given project trigger the Project gt Properties menu then click on the resource file tab A similar window as seen previously is then displayed 8 4 Display resource values and AtelierB version Description The version display command shows e the global version of Atelier B e the version of all Atelier B tools e the current values of resources Graphical user interface To display resource values and Atelier B version just go on the workspace s properties and on the first tab bbatch there is a Configuration details button After having clicked on it a window similar to the following screenshot ClearSy 103 Atelier B 4 User manual ClearSy 8 5 Modifying the external tools configuration atb Configuration Details ATELIER B version AtelierB ATELIER B BATCH USER INTERFACE version V3 7 23 Compiled for Linux Compiled with gcc version 4 2 4 Ubuntu 4 2 4 1ubuntu3 The following libraries are used SESSION MANAGER library version V3 7 17 Compiled for
27. Atelier B 4 User manual ClearSy Document written by ClearSy This documentation is distributed under the CREATIVE COMMONS CC BY CERTAINS DROITS RESERVES Every names of products quoted in this document are trademarks of their respective authors ClearSy System Engineering Parc de la Duranne 320 av Archim de Les Pl ades III Bat A 13857 AIX EN PROVENCE CEDEX 3 FRANCE Tel 33 0 4 42 37 12 70 Fax 33 0 4 42 37 12 71 email contact clearsy com ClearSy Atelier B 4 User manual ClearSy CONTENTS Contents 6 1 1 About this document 6 a go Oe A An Ben oe o a A 6 13 Atelier B user Imterfaces e 7 1 4 Organisation of this document 8 1 5 Conventions imita a a a e a a A 9 10 ea A a e a hae a 10 2 1 1 Introduction i 426542644 ple reido rc a e e babes 10 Ceras a a a aa A 11 pala Plog a aaa a aE a ata A 11 A E 11 2 1 5 External tools 26522 sb maf o 2 22 hs esos ea e 11 2 1 6 Using Atelier B on a multi platform network 12 2 1 7 Creating the Atelier B manager account 2 2000 13 2 1 8 Choosing the Installation Directory 0 0 200000 13 Sah plete eidbeeekbagal bie eed Eh 14 ik i ae bok Eee ee a RS 14 obi p ee ee ek Pda ke bbb he ek bee ak bas te bE GS 15 2 2 1 Windows 244 4 644244 pie ee bbbaeebeagael bie ee bbb es 15 Phe eb bee ak bbe ee bE be eee ek be a eo 17 bb hob bow ee eR baw eh doe a Pe eee ee bE aS
28. B 6 LG_CONDITION The first line shows the names of the metrics that are repeated after the table The second line remains the reference value for each metric The next lines show the values of the metrics for each project implementation If a metric value exceeds the reference it is enclosed between lt value gt example 4 Example of an implementation report METRICS FOR IMPLEMENTATION Ecran_imp E A ee Title Value Ref gt ref CR Popes eset ah aha NB_INST_OPER 13 500 OK Proa naar ips Fra EEE 4 NB_INST_SEQ 6 100 e OK hse A A 4 4 NB_CTRL_SEQ 1 10 n OK Aa So eee cee 4 NB_CTRL_IMB 4 3 25 KO Poel ei Se eR SS Jaade NB_WHILE_IMB 1 2 OK ClearSy O E Atelier B 4 User manual ClearSy 6 7 Extracting Metrics EA A A AN A a ed cl AO A ln DRA metas ad LG_CONDITION 1 100 o OK AA A aad aha ae ae DA PR ted ts eda ee ala ne aa A teh ae The first column shows the names of the metrics The second column shows the maximum value of each metric for all implementation operations The third column shows the reference value
29. Linux Compiled with gcc version 4 2 4 Ubuntu 4 2 4 1ubuntu3 B Compiler version V1 144 29 04 2008 The following flags have been used Compiled with gcc version 4 2 4 Ubuntu 4 2 4 1ubuntu3 Compiled for Linux target Pentium version B DECOMPILER version V2 23 jeu mar 15 18 54 06 CET 2007 The following flags have been used Compiled for Linux Compiled with gcc version 4 2 4 Ubuntu 4 2 4 1ubuntu3 LOGIC SOLVER version K56 mardi 20 mai 2008 17 02 03 CEST Compiled for Linux Compiled with gcc version 4 2 4 Ubuntu 4 2 4 1ubuntu3 inkaen innt Viton Men 8 5 Modifying the external tools configuration Presentation By default Atelier B uses the external tools configured during installation To modify one of these tools for all Atelier B users you have to modify the value of its resource Tool Resource Text editor ATB OPT_TOOLS_ lt SYSTEM gt Editor_ path TEX ATB OPT_TOOLS_ lt SYSTEM gt Latex_ Binary _ Directory Graphical user interface It is possible to configure some external tools directly from the GUI independently of the resources explained previously To do so trigger the Atelier B gt Preferences menu then click on the Instal lation tab The following window is displayed ClearSy 104 Atelier B 4 User manual ClearSy 8 6 Modifying Memory Allocation of the Logic Solver From this interface you can reconfigure the SSH and DOT paths Pr
30. O it receives by preference order e the demonstration of the ancient PO with the same number if this PO would end e the first one of the ancient PO demonstrations proved of the same clause e the first one of the ancient PO demonstrations proved of a different clause e the demonstrations of the ancient PO with the same number wich was not ending If a new PO can t deduct itself from an ancient one but if its number and pertenancy clause do exist it receives the demonstration of the ancient PO with the same number and clause In this way the user retrieves his demonstation even if he renamed some identificators ClearSy 67 Atelier B 4 User manual ClearSy 5 5 Generating Proof Obligations Thanks to this mecanism the user can keep the interactives demonstrations and automatics if the PO are the same The messages of PO generator are displayed in the start up window as following Generating proof obligations of Machine B_Keyboard_code Initialisation proof obligations 3 obvious proof obligations 3 b_input_code proof obligations obvious proof obligations 2 3 proof obligations generated 11 obvious proof obligations generated Generation complete Normalising b_check_code unchanged Merging Done For each clause present in the component Atelier B displays the number of proof obligations to be proved proof obligations and the number of obvious proof obligations deleted obvious proof o
31. agement Somepaces blocks Components Hierarchical view e ato Component wv TypeChecked POs Generated Proof Obligations Proved PGCD block_occupancy y block_occupancy_1 OK OK 7 7 E Components Q block_occupancy_1_i OK OK 33 21 E Definitions Q block_occupancy_1_it OK OK 6 6 Y Libraries i block_occupancy_1_it_i OK oK 19 9 source WD lemmas 9 block_occupancy 2 OK OK 5 5 H library di block occupancy 2 1 OK oK 31 18 a test 9 block_occupancy_3 OK OK 4 4 block_occupancy 3 OK OK 12 5 y block_occupancy_4 OK OK 4 4 block_occupancy_4 OK OK 2 0 9 block_occupancy_5 oK oK 4 4 Q block_occupancy_5_ OK OK 35 24 block_occupancy_i block_occupancy_iti OK OK 19 9 configuration OK OK 0 0 W inputs OK OK 4 4 Unproved BO Checked 0 12 OK OK OK OK OK OK OK OK OK OK OK OK OK This view is customizable and it is possible to sort this list according to a given column by clicking on its header This version allows you to open several projects simultaneously Reciprocally the closing of a project is triggered by using the Project gt Close menu of the interface This leads to empty the components listing Command line interface The user interface is already started up To open project proj_name type the following command open_project proj_name or op proj_name The user interface is already started up To close a project type th
32. already proved This percentage does not take in account POs eliminated by the proof obligation generator The last line in the table TOTAL sums up each information for all operation of the component This information can be included in the documents automatically generated by Atelier B refer to sub section A Graphical user interface The GUI is aleardy launched a project has been opened To obtain information on a component you have to click on the given component and trigger the Component gt Status menu or either use the Ctrl s keyboard shortcut A dialog is displayed as on the following screenshot ClearSy 86 Atelier B 4 User manual ClearSy 6 4 Dependency Graphs Block occupancy 3 Component status Component Status for block_occupancy_3 AutoProved home pmauduit AB blocks block_occupancy_3 mch ni nPRI nPRa nun Pr oooooooo0oo0o000 Command line interface The user interface is started up you already have opened a project To obtain the status of the comp_name component type the following command status comp_name or S comp_name 6 4 Dependency Graphs Description This command is only available if the workstation has the Graph Viz free package tool installed visit http www graphviz org for more information A dependencies graph is provided for the selected component or for the whole project The search for dependencies is recursive Therefore if component X depen
33. ame The following message is displayed in the start up window Unproving successful 5 10 Checking the Translatable Language BO Description Before using the translators for exporting to standard computer programming languages check that the language used in the implementations can be translated The constructions authorized in the implementations are described in the B Language Reference Manual The error messages from the BO checker are displayed in an error window and in the start up window as following lt file gt lt line number gt lt column number gt BO check lt error description gt ClearSy 74 Atelier B 4 User manual ClearSy 5 10 Checking the Translatable Language B0 Exemple BO Checking Machine B_Keyboard_code_1 B_Keyboard_code_1 imp 5 11 BO Check binary expression is not a simple term B_Keyboard_code_1 imp 5 19 BO Check binary expression is not a simple term BO Check error in B_Keyboard_code_1 Column and line numbers allow an exact location of the place where the error was detected When the component is correct the following message is displayed in the start up window BO Checking B_Keyboard_code_1 BO Checking B_Keyboard_code_1 successful remark To use the HIA translator it is necessary to type the array with concrete constants By default the BO checker indicates that the concrete constant is not implementable In that case to pass over the BO checker the following resource has to
34. ancy 1 it i This file has been generated by BART B Automatic Refinement Tool Generated the I0N10 2008 DO NOT EDIT 7 IMPLEMENTATION block occupancy 1 it i REFINES block_occupancy 1 it SEES configuration inputs CONCRETE_VARIABLES rg_t_block courant INVARIANT rg_t _block_courant NATURAL 4 rg_t_block_courant 0 size bijection_t_block t_block_a _traiter bijection_t block 1 rg t block _courant INITIALISATION rg_t_block_ courant 0 OPERATIONS pragma INLINE initier_iteration_t_ block poursuivre iteration_t_block continue lt initier_iteration_t_block BEGIN rg_t_block courant lt lire card_t block continue bool 1 lt rg t block_courant END B Symbols 3 Outline ax Description Ascii Functions and relations Partial function gt gt Total function gt Partial surjection gt Surjection gt gt Lambda function a Override lt Relation lt gt Domain substraction lt lt X Its main functionalities are Component editing PMM file associated to B component editing e RMF file associated to B component editing e PatchProver and PatchRaffiner editing Syntaxic coloration Printing Auto completion and automatic indentation ClearSy 23 Line 15 Column 10 Atelier B 4 User manual ClearSy 3 3 Editor e Some syntax checking e Navigation between open files It also includes a presentation of language B symbol
35. archive created is named home project tarPROJ arc 4 2 5 Restoration Description This function is used to restore a project managed by Atelier B from the data stored in an archive created using the function described in the previous sub section Three restore options are available e restore B source files e restore B source files and proof files e restore the entire project A restoring always creates a new project When a project is restored the following data from the archived project are lost e the list of project libraries e the name of the project manager the user who is restoring the project automatically becomes the manager of the created project ClearSy 43 Atelier B 4 User manual ClearSy 4 2 Projects Advanced usage e the list of users authorized to access the project Remark You can restore the B source files and the proof files of a project archived with a previous version of Atelier B You cannot restore a project using the sources and proof files option if your archive has been generated with the only B sources option If so the Atelier B will indicate you an error Graphical user interface A wizard has been implemented to lead you in the restoration task Restore Project Workspace Archive path Select file new project name Destination directory home pmauduit AB Browse Restoration parameter D Source files Whole pro
36. bligations 699 Atelier B displays a character each time a new PO is generated The PO clauses that have been copied are listed at the end of generation Graphical user interface The GUI is already launched a project is opened To generate the Proof Obligations on components you have to perform these following steps 1 Select the components into the components list 2 Click on the PO Generate If the POs have been generated for a given component the Atelier B will ask the user if it is necessary to execute a command in full mode In case of errors on a component a message is added into the errors view ClearSy 68 Atelier B 4 User manual ClearSy 5 6 Displaying Proof Obligations Command line interface The user interface is started up you already have opened a project To generate the proof obligations for component comp_name with the Differential option type the following command pogenerate comp_name 1 or po comp_name 1 To generate the PO for component comp_name with the full option type the following command pogenerate comp_name 0 or po comp_name 0 The option by default proposed by Atelier B is the Differential mode Usable parameters ATB POG Generate_ Obvious_ PO Positioned at Atelier B installation Determine wether the Atelier B will generate or not the obvious PO 5 6 Displaying Proof Obligations Description Atelier B provides two method
37. comp gt This file has been generated by BART B Automatic Refinement Tool Generated the I0N10 2008 DO NOT EDIT Command line interface The interface is launched a project is opened To use the automatic refinement function on the component nom_ comp you have to type in the following command bart lt nom_comp gt 5 5 Generating Proof Obligations Description This function produces the proof obligations of a component The component must be type checked refer to the section 45 3 The proof obligations are defined by the B method They depend on the level of the software devel opment e In machines the selected mathematical model must be consistent e In the following steps you must prove that refinements keep the properties of the previous step model ClearSy 66 Atelier B 4 User manual ClearSy 5 5 Generating Proof Obligations The document Proof Obligations _ Reference Manual describes the PO in a theoric way In theory there is a proof obligation for initialization and a proof obligation for each of the operations In practice these obligations can be large and complex formulas The Proof Obligations Generator function split the theoretical PO into many simpler PO Some PO are so easy to prove that the PO Generator can prove them by itself In return the initially foreseen number of formula increases Some PO defined as obvious are automatically eliminated by the tool Before generat
38. ct Status table in SGML format stg Project data base Component Status table in SGML format tex Project data base Files generated by the documentation tools for translation into LaTeX rtf Project data base Files generated by the documentation tools for translation into Word dvi Project data base Files generated by LaTeX for display or print out ps Project data base LaTeX files converted into PostScript format for printing out bod str Translation directory Object files generated by the ADA translator blf sub directory ada ads adb Translation directory Files generated by the ADA translator after link sub directory ada edition continued on next page ClearSy 109 Atelier B 4 User manual ClearSy 8 8 Configuring the Printing Script continued from previous page File Location Contents makefile Translation directory Directives for ADA compiler sub directory ada bod str Translation directory Object files generated by the HIA translator blf sub directory hia hia h Translation directory Files generated by the HIA translator after link sub directory hia edition makefile Translation directory Directives for HIA compiler sub directory hia bdy spe Translation directory Object files generated by the C translator blf sub directory cpp cpp h Translation directory Files generated b
39. ction is used to update all the components of a project It takes into account the dependencies between the project components and the status of each com ponent This function redoes for each component all the actions that have already been performed at least once This function offers two options forced mode Operations that have already been performed at least once will be repeated regardless of the status of the components For example if a component is already in the Type Checked state and the user requests a Forced remake on the project then the type check will be redone on this component normal mode The operations that have been performed at least once in the past will be repeated only if necessary Command line interface The user interface is started up you already have opened a project To update all the project components type the following command remake force or r force ClearSy 80 Atelier B 4 User manual ClearSy 5 15 Tools interruption The force parameter must equal 0 in normal mode and 1 in forced mode 5 15 Tools interruption Description This function permits the interruption of some actions According to the executed action this interruption is either automatic or manual e The manual interrupt works with the following actions Syntax analysis and type checking Generation of proof obligations Automatic demonstration It offers different possibilities according
40. cument describe every functionalities supplied by the Atelier B This chapter describes more particularly the steps to follow in order to use the functions of the Atelier B In summary to start a development with the Atelier B you will have to 1 Create a project see sections 44 1 2 2 Open this projet see section 44 1 4 3 Add components to this project see section 44 3 1 Or simpler if you have a project archive you could restore it see section 4 2 5 and begin to work with the newly restored project Once those steps accomplished you can begin to apply B Method on your components the Atelier B allows you to 1 Perform the syntax analysis and the Type Check see section 5 3 2 Generate the Proof Obligations see section 415 5 3 Automatically demonstrate some of these Proof Obligations see section A5 7 4 Print the Proof Obligations see section A5 6 5 Use the interactive prover to demonstrate remaining proof obligations see section 453 After having created the implementations of your project you will be abled to 1 Control the language of these implementations see section 45 10 2 Translate the project into machine language by using a translator see section 345 12 During those development steps you can use the analysis functionalities of the Atelier B in order to 1 Print the progress state of the project or a component in particular see sections and 446 3 2 Show dep
41. d by type The user can request this information ClearSy 91 Atelier B 4 User manual ClearSy 6 6 Cross References e for a specific identifier e for all of the identifiers defined in a component e for all of the identifiers defined in the project the user will obtain a dictionary of the terms used in the project To distinguish the specifications and implemantaions of local operations the names of the implemantations of local operations are preceded by refinement_of_ VARIABLES end_delay concrete variable Definition of end_delay in B_Delais mch CONCRETE_VARIABLES Use of end_delay in B_Delay mch INVARIANT Use of end_delay in B_Delay mch INVARIANT Modification of end_delay in B_Delay mch INITIALISATION Modification of end_delay in B_Delay mch b_init_delay Modification of end_delay in B_Delay mch b_stopper_delay Modification of end_delay in B_Delay mch b_delay_elapsed OPERATIONS b_delay_elapsed operation name Definition of b_delay_elapsed in B_Delay mch OPERATION PARAMETERS end_del operation output parameter Definition of end_del in B_Delay mch b_delay_elapsed Modification of end_del in B_Delay mch b_delay_elapsed This information can be included in the project documentation automatically generated by Atelier B Warning Calling this function generates a semantic analysis of the concerned components Command line interface The user interface is started up you already have opened a
42. document we call B Tools the tools that are related to the application of the B method the analysis the adjustement and the documentation of software written with B The B environment described in this manual allows two main interfaces for using the B tools e an interactive mode that uses a graphical interface based on windows and buttons In the next sections this mode will be called the Graphical User Interface e a batch interface that uses a dedicated language called Command Language In the next sections this mode will be called batch mode ClearSy 7 Atelier B 4 User manual ClearSy 1 4 Organisation of this document 1 4 Organisation of this document This document is separated in three parts that allows to gradually initiate the reader to the use of Atelier B and its different interfaces It has been written with the aim of both allowing new users to learn Atelier B and both allow user of previous versions to be efficient with this new version of Atelier B e The first section describes the installation of Atelier B and its prerequisites depending on the different supported operating systems It also provides an introduction to the two interfaces e The second sections aims to provide a quick start guide that describes the different features available through the Atelier B interfaces e The third section explores the practical use of Atelier B within a B development ClearSy 8 Atelier B 4 User manual ClearSy
43. ds on component Y for example via an IMPORTS link and component Y depends on component Z for example via a SEES link then components X Y and Z will be present in the graph The components are grouped by module A module contains a machine its refinements and its implementation Given the complexity of the projects a number of options are available for filtering the links and the modules displayed The user can choose between several options in order to filter the links and the modules being printed Here are the different options Components filtering The user can choose between several options for the components The available options are All All the project components are present Selected only Only the selected component is displayed ClearSy 87 Atelier B 4 User manual ClearSy 6 4 Dependency Graphs Selected and transitively linked Only the selected component and all its refinements and ab stractions are displayed Link filtering The user can choose the types of links SEES IMPORTS displayed Graph direction The user may choose to do a graph ascending In this case the components that are dependent on the selected component are displayed This shows the impact of a modification to this component on the other project components All the component incoming links are displayed descending In this case the component linked to the selected component are displayed All the components outgoing
44. e filesystem where Atelier B will be installed It also contains explanation on how to use Atelier B on a network The second part provides a detailed description of the procedure to follow in order to read the Atelier B files supplied After performing the operations described above Atelier B and its user accounts can be potentially configured These operations are described in paragraph The section 8 contains all the information necessary for customizing Atelier B The last part of this section explains the procedure to follow so as to ease the port of B projects developed with a previous version of Atelier B 2 1 Preparing the installation 2 1 1 Introduction This section explains how to e Select the machine to install e Use Atelier B on a network e Create the Atelier B manager account e Select the filesystem where the Atelier B files will be installed Note that those steps are not required on all operation systems For instance under Windows OS it is not useful to create a manager account ClearSy 10 Atelier B 4 User manual ClearSy 2 1 Preparing the installation 2 1 2 Resources required before installation To install and use Atelier B you must have one of the following operating systems available e Linux with glibc version 2 or greater e Solaris 2 6 SunOS 5 6 or compatible e Microsoft Windows 2000 or greater e MacOS versions 10 4 or greater 2 1 3 Memory Requirements It is recommended to
45. e following command close_project or clp ClearSy 37 Atelier B 4 User manual ClearSy 4 2 Projects Advanced usage 4 2 Projects Advanced usage This section is about the advanced management of projects The main functionalities described below are available using the Project gt Properties which gives access to the following interface Properties for project blocks project software development l krt l resource file project database home pmauduit AB blocks bdp project translate directory home pmauduit AB blocks lang Configuration Details Users Remove Libraries Definitions directories The command line equivalents will be given afterwards 4 2 1 Users management Description In order to grant access to the objects managed by Atelier B it is possible to add and or delete users in addition every users declared on a project have the same read write rights on it It is however essential to let at least one user in the list Graphical user interface ClearSy 38 Atelier B 4 User manual ClearSy 4 2 Projects Advanced usage Simply click on the users you wish to suppress then click on the remove button Click on the Add button to display a dialog box allowing you to type in a user name If you want to give an access to every users you can specify a wildcard using the character 4 2 2 libraries management Description When developping on sig
46. e reason why two manuals are dedicated to this subject e Interactive Prover User s Manual e Interactive Prover Reference Manual The Atelier B automatic prover has different levels of force These forces are described in sub section 3 1 1 of the Interactive Prover User s Manual The messages of the automatic prover are displayed in the start up window as shown below Proving B_Delays Proof pass 0 still 3 unproved PO clause b_init_delas End of Proof Initialisation Proved O Unproved 0 b_init_delay Proved 1 Unproved 0 b_stop_delay Proved 0 Unproved 0 b_delay_is_up Proved 3 Unproved 0 TOTAL for B_Delays Proved 4 Unproved 0 ClearSy 71 Atelier B 4 User manual ClearSy 5 7 Automatic Demonstration For each clause of the component Atelier B displays a each time a proof obligation is proved and a each time the prover fails Graphical user interface The GUI is already launched and a project is opened To launch the automatic prover on some components you have to perform the following instructions 1 Select the componets into the list 2 Click on the Component gt Proof menu and on the desired force You can in addition launch a customized proof by triggering the Component gt Proof gt Customize Proof menu The following window will then show up A Proof A m Proof Automatic Force 0 Settimeout sec 180 EY Proof Automatic Force 3 A y Set
47. e table below describes all the files created by Atelier B File project_name desc Location Atelier data base Contents Project descriptor directories manager users libraries project_name db Project data base Project components name localization owner usedby_ Project data base Marker indicating that the project is opened by a user project Project data base transla Marker indicating that the directory is occupied tion directory by a project lib Project data base Directory of library project PDBs lock Project data base Markers used to ensure mutual exclusion be tween users of the same project deB versB Project data base FIFOs for communication between the user in terface and the Logic Solver src Project data base B source files with expanded definitions There is one file per component even if expand_src Project data base B source files one per component nf Project data base normalized form of component tse Project data base Extended table of symbols generated by BOChecker po Project data base Component proof obligations Opo Project data base component obvious proof obligations pmi Project data base Saved component interactive proof pmm Project data base Rules defined by the user for each component project_name gdl Project data base Dependency graph project_name stg Project data base Proje
48. e user atelierb has privileged rights on all the projects created via Atelier B All intermediate files generated by Atelier B during a development will belong to the atelierb group The two Atelier B user interfaces are executable files with the set group id bit Regardless of the user who executes them Atelier B will have the rights of the atelierb group On the other hand the user source files B sources proof rules files will have the rights assigned by the users They can therefore be protected with the standard UNIX access rights We recommend that you follow the procedures defined by the constructors for creating this account and this group e use admintool for SUN systems e use sam for HP UX systems e use adduser or linuxconf for Linux systems We recommend using the directory selected in the sub section below as the home directory of this account 2 1 8 Choosing the Installation Directory If you install Atelier B for several users you must choose a directory where the users will have read and execute access This directory must also be visible to all machines that are likely to run Atelier B To install the Atelier B files you must have the write access to this directory We recommend that you install the Atelier B files in a directory named atelierb in the disk partition where you normally install applications To install Atelier B you will need around 100 Mbytes depending on your operating system ClearSy 13
49. ecomes_ Such_ That FALSE Allow or not the becomes as substitution in implementation ATB BCOMP Allow_ CHOICE FALSE Allow or not the CHOICE substitution in implementation ATB BCOMP Allow_ LET FALSE Allow or not the LET substitution in implementation ATB BCOMP Allow_ Parallel FALSE Allow or not the Parallel substitution in implementation ATB BCOMP Allow_ Pre FALSE Allow or not the PRE substitution in implementation ATB BCOMP Allow_ Read_ In_ Values FALSE Allow or not using previously valued constants in the VALUES clause ATB BCOMP Allow_ SELECT FALSE Allow or not the SELECT substitution in implementation ATB BCOMP Tab_ Width 8 Number of character needed to obtain a tabulation ClearSy 65 Atelier B 4 User manual ClearSy 5 4 Automatic refinement 5 4 Automatic refinement Description A functionality of the Atelier B permits to generate refinements automatically based on the use of the Bart Graphical user interface The GUI is already launched and a project is opened In order to use this functionality click on the desired component then trigger the menu Component gt Automatic Refinement The newly created components are automatically attached to the project and a comment is added to their sources lt nom_
50. eferences Main window Projects New components Internal Editor Installation Local Atelier B Installation Ressource file nome pmauduit sre AtelierB MAKE_ATB AB AtelierB x Browse Maximum running tasks 1 Remote server connection ssh putty GraphViz Dot interpreter path to dot command usr bin dot Browse Browse CETE 8 6 Modifying Memory Allocation of the Logic Solver Modifications of the Logic Solver parameters are required in the following cases ClearSy e Your machine does not have enough memory to execute Atelier B Message type Cannot launch the Logic Solver check if there is enough memory e The complexity of your B project forces you to increase the memory size Message types Compiler Memory Full SEQUENCE ID NUMBERS OVERFLOW SEQUENCE MEMORY OVERFLOW SEQUENCE _chn ID NUMBERS OVERFLOW SEQUENCE _chn MEMORY OVERFLOW stopping forward because OBJECTS OVERFLOW MAXIMUM NUMBER OF THEORIES xx REACHED 105 Atelier B 4 User manual ClearSy 8 7 Modifying Memory allocation of the K parser GOAL STACKS OVERFLOW SYMBOLS OVERFLOW at lt symb gt To set Logic Solver parameters for all Atelier B users it is necessary to modify the value of the resource named ATB ATB Logic_Solver_Command in file AB AtelierB Refer to section 48 2 Depending on the size you need you have to replace the line ATB ATB Logic_Solver_Command krt with one of the f
51. endence graphs between components see section 246 4 ClearSy 28 Atelier B 4 User manual ClearSy Quickstart guide You could similarly use functionalities in order to produce automatically documentations in various formats Plain Text ATEX PDF or RTF see section A7 2 for more information about these features When your B Projects are reaching a significant size you can 1 Archive them in order to do backups see section 44 2 4 2 Split your large projects into several little projects by using the concept of libraries see section 4 2 2 ClearSy 29 Atelier B 4 User manual ClearSy 4 1 Projects management 4 1 Projects management A project managed by the Atelier B is characterized by e Its name e A Project Data Base where all the files created by Atelier B are stored PDB e A directory where the translations of components to machine languages are stored e A set of B source files these files can be located in different directories The creation of these directories and B source files is entirely up to the user if using Command line tool The graphical user interface creates the directories if necessary The projects managed by Atelier B are multi user projects Many users can work on the same project simultaneously Atelier B uses in its ideal installation the rights of the UNIX group atelierb in order to solve UNIX files access permitions between these users see paragraph 42 1 7 It i
52. ent and trigger the Component gt Proof gt Interactive Proof menu The following window will be then dispayed Atelier Be prover blocia occupancy Die locke lc Proof Edit View Help 40000 VOOR 0 amp amp ma en Pr FF 0 mis EH e mp e es Freh an Theory list a8 Proot oes Only applyable rules Mome pmaudultsrc AtellerB MAKE_ATE 2 1 Simplityx RecEqualityx E FindLabX E Errors 0N Message Location Component a JH Enumerated sets GEJ Situation GE Show only unproved POs initialisation Pot Logical analysis CE Po2 initier_iteration_t_block Depth o 2 Eg G POI Po2 poursulvre_iteration_t_block Por Po2 Search rule result CE 4 M Search hypothesis result ClearSy 70 Atelier B 4 User manual ClearSy 5 7 Automatic Demonstration The Proof Obligations are visible into the Situation view Usable Parameters ATB OPT_ TOOLS _ lt SYSTEM gt Latex_ Binary Directory Positioned at Atelier B installation Directory where it is possible to find the Latex binaries ATB OPT_ TOOLS_ lt SYSTEM gt Latex_ Viewer Positioned at Atelier B installation Name of the Latex viewer 5 7 Automatic Demonstration Description This function automates in the limit of its ability the demonstration of the proof obligations for each B component The proof activity is essential to the B method This is th
53. entifier maximum size of a set element identifier maximum size of a visible constant identifier maximum size of a visible variable identifier maximum size of a literal character string in an operation maximum size of a local variable identifier maximum size of an operation identifier maximum size of an operation identifier machine identifier maximum size of a condition expression for an operation num ber of operators memory space taken by the arrays number of operations promoted and extended memory space taken by the visible variables other than arrays memory space taken by visible constants other than arrays Graphical user interface This function is not available from the GUI Command line interface The user interface is started up you already have opened a project To calculate the metrics on all the implementations of a project type the following command ClearSy 96 Atelier B 4 User manual ClearSy 6 7 Extracting Metrics lchecker_project config_path output or lcp path_config output The first parameter is the complete path of the configuration file to use for example lt rep_Atelierb gt AB press lib LC CONFIG_clause cvl The second parameter is the output format the values 0 1 4 6 and 8 correspond respectively to a LATEX Interleaf ASCII FrameMaker or Word displaying The values 2 3 5 and 7 correspond respectively to a ATRX Interleaf ASCII FrameMaker or Word print out To calculate
54. er It is recommended that you close all other applications before continuing Click Next to continue or Cancel to exit Setup Just follow the assistant to simply install Atelier B It will ask you for some preferences for instance the installation directory see the figure below al Select Destination Location N Where should Atelier B be installed E Setup will install Atelier B into the following folder To continue click Next If you would like to select a different folder click Browse C Program Files Atelier B Browse At least 104 4 MB of free disk space is required Finaly if the installation is correct it will display the following window ClearSy 15 Atelier B 4 User manual ClearSy 2 2 Installing Files E setup Atelier B aloj xj Completing the Atelier B Setup Wizard Setup has finished installing Atelier B on your computer The application may be launched by selecting the installed icons Click Finish to exit Setup ClearSy 16 Atelier B 4 User manual ClearSy 2 2 Installing Files 2 2 2 Mac OS X Under this operating system Atelier B contains also an instaler with dmg extension Just follow the assistant to simply install Atelier B ClearSy 17 Atelier B 4 User manual ClearSy 2 2 Installing Files 2 2 3 GNU Linux and Solaris An atelierb user could be necessary to install Atelir B under GNU Linux or Solaris This is not
55. er interface The GUI is launched and a project is opened To do a syntax analysis and a typecheck on components you have to 1 Select the desired components into the components list 2 Click on the Typecheck button each component is processed successively If there is a syntax error an error window will be displayed This window contains the description of the detected errors If there is a semantic error on one of the components a warning window will be displayed In this case check the type of error according to the messages displayed in the start up window If a syntax error occurs the error is reported with a description into the errors view Remark You can interrupt the treatment by using the function described in chapter on page Command line interface The user interface is started up you already have opened a project To perform a syntax analysis and a type check on component comp_name type the following command typecheck comp_name or t comp_name The information and error messages from the type checker are displayed in the start up window Usable parameters ATB BCOMP Allow_ ANY FALSE Allow or not the ANY substitution in implementation ClearSy 64 Atelier B 4 User manual ClearSy 5 3 Syntax analysis and Typecheck ATB BCOMP Allow_ Becomes_ Member_ Of FALSE Allow or not the becomes member of substitution in implementation ATB BCOMP Allow_ B
56. ete a definition file directory click on the one you want to suppress then click on the Remove button Command line interface The user interface has already been started up To add the dir directory to the proj project you must type the following command add_definitions_directory proj dir or add proj dir Beware you must indicate the absolute path of the directory On the contrary To delete the dir directory from the project name proj_name you must type the following command remove_definitions_directory proj_name dir or rdd proj_name dir 4 2 4 Archiving a project Description This function allows you to archive every files of a given project The created archive is a zlib compressed file equivalent to a classical tar file This function can be used to e back up a project e make a copy of a project e g to transfer it to another machine There are three options for archiving e Save all the B source files mch ref and imp and definition files ClearSy 41 Atelier B 4 User manual ClearSy 4 2 Projects Advanced usage e Save all the B source files and the proof files With this option Atelier B also saves the files in the project data base used by the proof tools po files proof obligations pmi files demonstrations pmm files user rules PatchProver file user tactics AtelierB file project resource file e Save the entire project B source files
57. for each metric The fourth column shows the excess percentage according to the reference value The last column shows OK if the value is below the reference value KO if not Example of an operation report METRICS FOR OPERATION message_controler_code 4 4 4 Title Value Ref gt ref CR 4 4 NB_INST_OPER 6 500 OK a ar a NB_INST_SEQ 4 100 s OK Pr 4 4 NB_CTRL_IMB 4 3 25 KO tsa oes AA 4 4 NB_CTRL_SEQ 1 10 a OK PRA AAA assess 4 4 NB_WHILE_IMB ol 2 OK s s a a a a a e S LG_CONDITION 1 100 ol OK Posen eso a eap apia aae p eS 4 4 The second column shows the value of each metric for the analised operation The meaning of the other table columns is the same as in the implementation report The following table shows the list of the available metrics ClearSy 95 Atelier B 4 User manual ClearSy 6 7 Extracting Metrics Metric Code Calculation
58. he component name The second parameter is the type of required presentation To retain the original presentation specify the value PLAIN Use the NORM value for a standardised presentation ClearSy 99 Atelier B 4 User manual ClearSy 7 2 Displaying a B Source Usable parameters ATB OPT_ TOOLS _ lt SYSTEM gt Latex_ Binary Directory Positioned at Atelier B installation Directory where to find the Latex binaries ClearSy 100 Atelier B 4 User manual ClearSy Atelier B Parameters Customization 8 Atelier B Parameters Customization 8 1 Introduction This section describe how the user can tweak the Atelier B in order to modify e external tools used by Atelier B editor HTML browser etc e memory amount used by Atelier B e parameters of Atelier B tools e printing script used for documents generated by Atelier B 8 2 Presentation of the customization system There are three ways for the user to customize Atelier B e create a resource file HOME AtelierB which customizes all Atelier B for the current user please not that we do not recommend to use this file because it may lead to conflicts with the other configuration files create an AtelierB file in the PDB directory of a project This file customizes Atelier B when the user opens this project create any file that the user has to specify explicitly when its use is requested When the same resource is specified in several of t
59. he function displays a table showing more precise information on the component proof obligations Example ClearSy 85 Atelier B 4 User manual ClearSy 6 3 Component Status Printing the status of FILE_BUFFER_1 FILE_BUFFER_1 POGenerated home projet spec FILE_BUFFER_1 mch farsa NbObv NbPO NbPRi NbPRa Pr Hanoi Initialisation 3 0 load_buffer 122 3 O 3 100 create_record 4 1 0 0 o not_in_buffer 7 il o mod_buffer 8 o val_buffer 8 o size_file 5 oO 4 FILE_BUFFER_1 47 4 0 3 75 4 End of Printing the status The columns in this table show for each operation on the component NbObv This column contains the number obvious proof obligations of the operation These proof obligations are eliminated automatically by the generator of proof obligations NbPO This column contains the number of not obvious proof obligations of the operation NbPRi This column contains the number of proof obligations proved by the interactive prover NbPRa This column contains the number of proof obligations proved by the automatic prover Pr This column contains the percentage of proof obligations on the operation
60. he paragraph 8 for more information ClearSy 61 Atelier B 4 User manual ClearSy 5 2 Managing workspaces 5 2 3 Deleting a Workspace The deletion of a workspace is simply done by triggering the Workspace gt Remove menu This will not suppress any file related to your projects from your hard drive 5 2 4 Opening and Closing a Workspace A double click on a workspace or a click on the Workspace gt open menu will open the desired workspace the icon is then changing and the available project is displayed Workspaces oes PGCD blocks library In order to close a workspace use the Workspace gt close menu The link between the GUI and the Command line interface is then closed and the Workspace icon is being changed Workspaces ClearSy 62 Atelier B 4 User manual ClearSy 5 3 Syntax analysis and Typecheck 5 3 Syntax analysis and Typecheck Description This function combines the syntax analysis and the type checking of B components The syntax checking ensures that the sources for the selected machines comply with the B language syntax On this subject the reader can refer to the B language Reference Manuel Type checking controls e identifier conflicts e typing rules missing declarations e language restrictions visibility rules e etc This type check is necessary for the PO generation The type check of a component is automat
61. hose files the priority order is the following from highest to lowest e the explicit file e the file associated to the project e the file associated to the user When two files are given explicitly the second one takes precedence When a resource is described in none of those files a default value is taken which is present in the Atelier B general resource file Atelier B parameters are by default defined in file AB AtelierB This file contains parameters shared by all atelierb users It is also possible to define specific parameters for a user or a project refer to Atelier B User Manual ClearSy 101 Atelier B 4 User manual ClearSy 8 3 Creating a resource file This file has the following format Lines beginning with an exclamation mark or a hash sign are comments other lines contain the name of a resource followed by its value The file contains the following parts e Graphical resources benv lt resource_name gt e Localisation of internal tools ATB ATB lt resource_name gt e Localisation of optional tools ATB OPT_TOOLS_ lt system gt lt resource_name gt where lt system gt is LINUX for a Linux machine HP10 for HP UX 10 20 SUN5_6 for Solaris 6 or greater e Parameters for internal tools ATB lt internal_tool gt lt resource_name gt Examples ATB POG Generate_Obvious_PO FALSE When the value of this resource is FALSE Atelier B does not save obvious proof obligations To
62. ically applied to all the components required by the current component through the following links SEES USES INCLDES IMPORT EXTENDS REFINES This type check on the required components is only applied when necessary i e if a component change was made since the last type check Modifications of form comments spaces are not taken in account Syntax errors are displayed in an error window and in the start up window They are displayed as following lt file gt lt line number gt lt column number gt lt error description gt Example AA mch 6 17 Sequential substitution is not allowed in a specification Line and column numbers show exactly the location in the source file where the error occurs Semantic errors are displayed in the Atelier B start up window They are displayed as following Type checking machine AA Loading referenced_machines Checking name_conflicts ClearSy 63 Atelier B 4 User manual ClearSy 5 3 Syntax analysis and Typecheck Checking constraints clause Checking INVARIANT clause Error 1 2 in aa 1 2 should be a set Error Variable aa has not been typed Checking operation b_ask_code Checking operation b_code_typed No information saved for AA End of Type checking The type checker displays an information message for each processed clause The Type checker Error messages manual describes in detail all the error messages generated during this phase Graphical us
63. ing the proof obligations for a component Atelier B ensures that the component is type checked Otherwise the type check is automatically performed Generating proof obligations creates four files in the PDB e the comp_name po file contains the PO of the comp_name component e the comp_name opo file contains the obvious PO of the comp_name component e the comp_name pmi file contains the status of the proof obligations proved not proved as well as the interactive demonstrations e the comp_name stc file contains a description of the component If the Differential option is used and if the PO of the component have already been generated at least once Atelier B compares the component with the description saved in the comp_name stc file For each operation and for the initialization it generates the PO only if one of the information occuring in their construction has been modified Otherwise it copies the PO from the ancient files If the full option is used the Atelier B generates all the PO again even if they haven t been modified After the new PO generation and if they have already been modified before they are automatically compared to the ancient ones in order to keep the associated demonstrations The comparison rule is the following one A P O B deducts itself from a P O A if they have the same goal and if the assumption of B contains the assumption of A If a PO can deduct itself from one or several ancient P
64. isible into the main window of Atelier B as seen on this screenshot Workspaces Pp PGCD blocks library After some modifications it may be useful to update the list this could be done by clicking onto the Workspace gt refresh menu ma lt Workspaces a Close Remove A Restore project BP blod Properties PB library Command line interface The user interface has already been started up To view the list of projects type the following command show_projects_list or spl ClearSy 31 Atelier B 4 User manual ClearSy 4 1 Projects management The list is displayed as shown below Printing Projects list projecti project2 End of Projects list 4 1 2 Creating a project in Atelier B Description The Attach project function allows all users to declare a new project in Atelier B The information required to declare the project is e the name of the new project and its owner e the Project Database directory PDB used by Atelier B to store internal files e the translation directory used by Atelier B to store translated files e The project type non required SOFTWARE for B Software projects SYSTEM for Event B projects By default the newly created project is considered as software To reference a given project only the PDB and translation directories are required by Atelier B refer to the directions below The creation of these tw
65. ject Source and Proof files First choose a workspace in which you are willing to restore your project then choose a path to the archive file give then a name to your newly restored project and a path in which to restore the files Finally select the restoration parameter and click on the Next button If the restoration process has successfully finished the new project must appear in the workspace The components and the definition directories are automatically attached to the project Command line interface The user interface is already started up To restore a project use the restore or res command This command requires four parameters e the archive file access path ClearSy 44 Atelier B 4 User manual ClearSy 4 2 Projects Advanced usage e the type of restore O restore B source files 1 restore the entire project 2 restore B source files and proof files e the name of the restored project you must give the name of a new project e the project base path if you do not wish the directories to be created in the current directory Example To restore and create the COPY project type the following command restore home project tarPROJ arc 1 COPY home COPY A new project called COPY is created in the home COPY directory 4 2 6 Reading Properties of a Project Description This function displays the following properties of a project e the access path to the project database e the access
66. learSy 6 4 Dependency Graphs 1 If you want a dependency graph about a specific component select it from the com ponents list 2 Trigger the Component gt Dependence Graph menu 3 Select the desired options on the dialog then click on the Ok button Below is a screenshot of the dialog which allows you to select the different options Dependence Graph Components All Selected only Selected and transitively linked Links y Imports v Sees The window presenting the graph will finally appear a Dependence graph for project blocks x Zoom In Zoom Out block_occupancy block_occupancy_i block_occupancy_1 block_occupancy_1_i block_occupancy_1_it block_occupancy_1_it_i block_occupancy_it block_occupancy_it_i block_occupancy_2 block_occupancy_2_i block_occupancy_3 block_occupancy_3_i block_occupancy_4 block_occupancy_4_i block_occupancy_5 block_occupancy_5_i Copy to clipboard Save as Print Close window ClearSy 89 Atelier B 4 User manual ClearSy 6 5 Operation call graph Command line interface The user interface is started up you already have opened a project To obtain a dependency graph use the following command project_status or ps This command uses seven parameters 1 The name of the component or the value to obtain a graph for the entire project 2 The option on c
67. mandatory as seen previously but in multi user mode it solves many problems concerning file access rights Please see the previous section for more informations on atelierb specific user The installation under those operating system is done by a shell script After downloading Atelier B archive you just need to uncompress it and to run the install_atelierb script user host su atelierb Password atelierb host home user atelierb host tar xvzf atelierb 4 0 linux tgz atelierb host cd atelierb 4 0 atelierb host atelierb 4 0 install_atelierb Follow the instructions below the different steps proposed by the installation script ATELIERB Installation Procedure Machine host Operating System Linux 2 6 24 23 generic Most of the questions that you will be asked have a default answer enclosed in brackets for instance Do you understand yes To use the default answer just type return ClearSy 18 Atelier B 4 User manual ClearSy 2 2 Installing Files Would you like to continue yes Installation procedure steps 1 Extract installation files 2 Configure and parameter Atelier B products q Quit installation procedure Go to step number 1 Do you want to generate obvious proof obligations as a default no Enter the complete path to your text editor usr local bin xemacs Is Latex installed on your system yes Enter the directory containing Latex binaries usr bi
68. metrics on a project implementation type the following command lchecker_mach name_imp config_path output or lcm imp_name config_path output The first parameter is the implementation name The two other one have the same meaning that for lcp ClearSy 97 Atelier B 4 User manual ClearSy B projects Documentation 7 B projects Documentation 7 1 Description Theses functions are available only if some external tools are installed on the workstation like ATEX a PDF viewer and Microsft Word OpenOffice The Atelier B provides some commands allowing to create automatically complete documents including the following information e B source files e user rule files pmm e status tables for the project and each component e different graphs e cross references In these documents e the B language symbols are displayed using math fonts e the B language key words are displayed in bold face characters The two commands offered by Atelier B are e Displaying a B source only e Create a complete document that may contain all the above information in the order chosen by the user 7 2 Displaying a B Source Description This function applies itself on any component of a B project The B source file specification or refinement is converted in an understable format of the selected word processor When converting the B source file the user can choose two types of presentations he can e keep his original
69. mmand cd or change_directory 2 Display the list of B sources present in this directory using the command 1sb or list_sources_b This command displays the list of files with mch ref imp or mod extensions present in the current directory 3 Add a component using command af file_name or add_file file_name ClearSy 49 Atelier B 4 User manual ClearSy 4 3 Components Management Example af AA mch 4 3 2 Suppressing Components Description This function permits to suppress one or several components from the current project B source files themselves are not deleted they are just removed from the list of components of the project When a component is suppressed all the information related to this component are deleted from the PDB except the following ones e B source files e user rule files pmm e automatically generated project documentation e translations Graphical user interface The GUI is launched and a project is opened Select the components you wish to exclude from the project and select the Component gt remove menu Or you can also click on the blue icon into the toolbar Command line interface The user interface is started up you already have opened a project To suppress a component from a project type the following command remove_component comp_name or rc comp_name If comp_name corresponds to a component part of a mod file then all the components incl
70. modify a resource for all Atelier B users the procedure is 1 Log in as atelierb under UNIX compatible systems only 2 Go to the Atelier B installation directory 3 Edit the resource file AtelierB 4 Change the line corresponding to the resource with the new value 5 Save your changes 8 3 Creating a resource file Description This function allows to edit the resource file If the file does not exist it is created and initialized from a model The model contains the list of all resources Displaying a resource can be made by uncommenting the line and updating the resource value Graphical user interface ClearSy 102 Atelier B 4 User manual ClearSy 8 4 Display resource values and AtelierB version In order to edit a resource file from a workspace click on the target workspace then use the Workspace gt Properties menu and click on the Resource file tab An overview of the dialog is given below Properties for Workspace atb _bbatch servers krt commands resource file F Ji i i i Jl i i i i i i Ji i i i i li i i Ji i i i i Ji i i ll Ji Ji i i i i Ji i i i i Ji i li i i li i l i Ji i i i ll i i i i i i Ji i i Jl i i i Ji gt Tools resources ATB ATB Logic_Solver_Commandkrt a c70000d3000e100910000h10000m1000000n1300000110400560000t1100x5000y5500
71. n Enter the name of the Latex viewer xdvi Enter the name of the Latex to PostScript generator dvips Is there a HTML viewer installed on your system yes Enter the complete path to your HTML viewer usr bin firefox Installation of Atelier B succeeded 0K ClearSy 19 Atelier B 4 User manual ClearSy 2 3 Previous versions of Atelier B 2 3 Previous versions of Atelier B This section describes the procedure to follow so as to retrieve the projects developed with the previous version of Atelier B The procedure to follow is 1 Archiving projects With the previous version of Atelier B you must archive the projects you wish to retrieve To do this use the Archive project function described in the User Manual You need only archive B source files and proof files 2 Installing the new version of Atelier B Follow the instructions of this manual to fully install the new version of Atelier B 3 Restoring projects With the new version of Atelier B restore the projects which were archived previously using the Restore Project function as described in section 4 2 5 ClearSy 20 Atelier B 4 User manual ClearSy Overview 3 Overview 3 1 Interfaces Atelier B user interface is split in two main parts one dedicated to project management the other allows editing B components using a specific developped editor Both have been developped in order to assist user during its development using the
72. nents of a project ClearSy 90 Atelier B 4 User manual ClearSy 6 6 Cross References The operation call graph can be included in the documentation automatically produced by Atelier B refer to section A command line interface The user interface is started up you already have opened a project To obtain an operation call graph type the following command op_call_graph or ocg This command include three parameters 1 the name of a component or the value to have a graph on all the project 2 the name of an operation the INITIALISATION key word or the value to have the graphs of all the operations 3 1if you wish to extend the graph to the refinements and to the operation abstractions otherwise 0 Example To display the operation call graph of operation op_name of component comp_name and all its refinements and abstraction type the following command op_call_graph comp_name op_name 1 or ocg comp_name op_name 1 6 6 Cross References Description This function performs searches on the identifiers defined in the project components For each identifiers the function displays e its type variable set e the place where it is typed e the names of the components and the clauses where it is defined e the names of the components and the clauses where it is used e the names of the components and the clauses where it is modified for variables only Identifiers are sorte
73. nificant sized projects it is fundamental to be able to e Use libraries of predefined components e Structure a prominent project in several sub projects If they wish the users can bind their projects to other projects managed by the Atelier B For this they can use the Add library function Every project available can become a library to the current project When a library is bound to a project the user of the project can write links SEES IMPORTS to components provided by this library The Add library function checks that the library to add is not already declared within the project If a component is defined into several libraries then the component which would be evaluated would be the one which is defined into the first imported library In case of doubts on the handled components it could be useful to request a printing of the project s dependence graph Graphical user interface As displayed on the previous screenshot the potential libraries list is displayed into the frame Libraries into the box on the right Use the mouse to select the project to be added as a library then click on the left pointed arrow button in order to add it to the current project Libraries es KI lib P Reciprocally select the library you want to exclude from the project then click on the right pointed arrow button in order to exclude a library from the project Command line interface ClearSy 39 Atelie
74. o directories is up to the user The project components can be scattered through the file system their access path and names are stored in a file located in the PDB and called project_name db Graphical user interface In order to create a project from the GUI you have to click on the AtelierB gt New Project menu or use either the shortcut Ctrl P either a right click on the given workspace then the New gt Project menu The project creation wizard will then appear ClearSy 32 Atelier B 4 User manual ClearSy 4 1 Projects management New project Name and config Workspace ato Project type Software development gt System modelisation Project Name You will have to choose between B Software and Event B After having typed a project name the interface will choose directories suitable for the project location but it will be customizable on the second page of the wizard New project Bdp Project Database home pmauduitABestbdp Browse Translations directory home pmauduitAB testlang Browse PatchProver Browse link You can use the Browse buttons to facilitate the choice of these directories Once the configuration is done and the wizard closed the newly created project should appear into the workspace view and be automatically opened as shown in the screenshot below ClearSy 33 Atelier B 4 User manual ClearSy 4 1 Pr
75. ojects management Workspaces ms atb PGCD PR blocks P library Components Es Definitions Y Libraries source WD lemmas Command line interface To create a project e Choose and create a directory for the PDB e Choose and create a directory for the translations e Launch the command line interface e Create the B project by typing the following command create_project nom_projet chemin_bdp chemin_lang SOFTWARE or crp nom_projet chemin_bdp chemin_lang SOFTWARE e Check that the project has been correctly created by typing show_projects_list or spl Remarks You are not forced to type in the full path you can give a relative path according to the current directory from where you launched the Atelier B The previous command allows to create a B Software project If you want to create an Event B project just replace SOFTWARE by SYSTEM 4 1 3 Deleting a Project In Atelier B Description The Detach project function deletes an existing project The intermediate files produced by Atelier B in the project data base will then be deleted These informations are not deleted ClearSy 34 Atelier B 4 User manual ClearSy 4 1 Projects management e B source files e user rules files pmm the project documentation that is automatically generated e the translations e the project data base directory e the translations directory To completely clear the project you
76. ollowing ones e for a small Logic Solver ATB ATB Logic_Solver_Command krt a m700000e40 e for a medium Logic Solver ATB ATB Logic_Solver_Command krt a m1000000e40 e for a large Logic Solver ATB ATB Logic_Solver_Command krt a m4000000e40 e for an extra large Logic Solver ATB ATB Logic_Solver_Command krt a m6000000e40 If a user wants a Logic Solver with another size different from the size used by all Atelier B users he must write its value for the resource ATB ATB Logic_Solver_Command in a file named AtelierB in his home directory 8 7 Modifying Memory allocation of the K parser Modification of the K parser parameters must be performed if your B source files are very large or if these files contain a large number identifiers Messages like SEQUENCE ID NUMBERS OVERFLOW SEQUENCE MEMORY OVERFLOW SEQUENCE _chn ID NUMBERS OVERFLOW SEQUENCE _chn MEMORY OVERFLOW SYMBOLS OVERFLOW at lt symb gt To modify the K parser parameter settings please follow the same procedures as above using the resource named ATB ATB KParser_Command 8 8 Configuring the Printing Script Description ClearSy 106 Atelier B 4 User manual ClearSy 8 8 Configuring the Printing Script By default the printing script used by Atelier B is the script named atelierb_directory AB bbin bprint To use another printing script 1 create a new script file 2 modify the value of the resource ATB ATB Print_Command in the file AB AtelierB
77. omatic Proof Force 1 y Hierarchical view Filter Component v TypeChecked POs Generated Proof Obligations Proved Unproved BO Checked Q block_occupancy ij block occupancy _i Q block_occupancy_1 di block_occupancy_1_i block_occupancy_1_it block_occupancy_1_it_i pancy 9 block_occupancy_2 block_occupancy_2_i pancy block_occupancy_3 pancy block_occupancy_3_1 Y block_occupancy_4 GJ block_occupancy_4_i block_occupancy_5 Q Dlock_occupancy_5_i 9 block_occupancy_it block_occupancy_it_i l pancy_it configuration OK inputs OK ClearSy 51 Atelier B 4 User manual ClearSy 4 3 Components Management On the next screenshot is displayed a usage of the Filter by name functionality B blocks Components Hierarchical view Filter block_ Component w TypeChecked POs Generated ProofObligations Proved Unproved BO Checked block_occupancy block_occupancy_1 Q block_occupancy_1_i l block_occupancy_it_i block_occupancy_ it Q block_occupancy_i l block_occupancy_5_i block_occupancy_5 Q block_occupancy_4_i block_occupancy_4 Ml block_occupancy_3_i block_occupancy_3 block_occupancy_2_i block_occupancy_2 Q block_occupancy_1_it_i block_occupancy_1_it command line interface The user interface is started up you already have opened a project To display the list of project components use the following command show_machine_list or sml
78. omponents A for All S for Selected only G for Selected and transitively linked 3 The library option A for Show All S for Show G for Group N for Hide 4 The direction of the graph U for up D for down 5 The types of links to display The links are in the following order EXTENDS IMPORTS INCLUDES SEES USES The value O deletes the displaying of the link Example To display only IMPORTS and SEES 01010 6 The option on the components not linked 1 to hide the isolated components 0 to show them 7 1 to see only the instanciation graph otherwise 0 Example To display the project graph with all the links type the command project_status A D 11111 00 6 5 Operation call graph Description This command is available only if the workstation has the DaVinci tool installed and only by using the Command line interface The operation call graph permits to visualise the cascades of operation calls in the OPERATIONS LOCAL OPERATIONS and INITIALISATION clauses of a B component This type of graph is useful during the proof phase as it allows to better understand where the elements of an operation PO come from To distinguish the specifications and implementations of local operations the name of the implemen tation of a local operation is preceded by refinement_of_ in this graph The operation call graph is provided for some selected components for these components and all those they depend on or for all the compo
79. on the proof status is indicated into the Situation view See the interactive proof manual for more information accessible via the Help gt Help contents menu Command line interface The user interface is started up you already have opened a project To run the interactive prover on component comp_name type the following command browse comp_name or b comp_name After typing this command the interactive prover prompt is displayed PRI gt You can then type the various interactive prover commands Type qu to quit 5 9 Cancelling Demonstrations Description ClearSy 73 Atelier B 4 User manual ClearSy 5 10 Checking the Translatable Language B0 This function is used to cancel the demonstrations performed on a component in order to repeat interactive proofs The interactive demonstrations are not lost Only the status of the proof obligations is changed Graphical user interface The GUI is launched a project is opened To cancel the component demonstrations perform the following operations 1 Select the components from the list of components 2 Use the Components gt Unprove menu The return messages into the tasks view must then indicate the following label Unproving successful Command line interface The user interface is started up you already have opened a project To cancel demonstrations of the component comp_name type the following command unprove comp_name or u comp_n
80. ou have to select it and click on the Component gt Properties menu A dialog like presented on the screenshot below appears then ClearSy 53 Atelier B 4 User manual ClearSy 4 3 Components Management Properties for component block occupancy 21 rx component Q9 block_occupancy_2_i Location home pmauduit AB blocks block_occupancy_2_i imp CESFTA The distinction on the type of the component is done by the blue icon shown ib the interface Command line interface To get information on a component called comp_name a project should be opened then type the following command infos_component comp_name or ic comp_name The properties are displayed as follows MACHINE gt Main LOCATION gt home project spec OWNER gt userl 4 3 5 Editing a Component Description This function allows you to edit the source file corresponding to a component By default the editor is the Atelier B internal editor but this can be customized by the editor of your choice Graphical user interface In order to edit a component in the GUI by using the internal editor you have to double click on the ClearSy 54 Atelier B 4 User manual ClearSy 4 3 Components Management component The editor is then launched You can also use the Component gt Edit menu or the keyboard shortcut Ctrl E You can custom the editor configuration in the main Atelier B configuration To do so click on
81. out those tools but some functionalities will remain disabled 2 1 6 Using Atelier B on a multi platform network You can install Atelier B on a network of machines that use a common file server All the users of systems supported by Atelier B can share an installation directory This manual contains instructions for installing Atelier B on a multi platform network Figure I on page 12 shows an example of a network installation In this example Atelier B is installed on a server machine Several machines with various operating systems use Atelier B The routing according to the type of system used is performed automatically by the Atelier B start up scripts ClearSy 12 Atelier B 4 User manual ClearSy 2 1 Preparing the installation 2 1 7 Creating the Atelier B manager account This section concerns only UNIX like operation systems in the case of a multiple user configuration The users can share projects and work on the same project at the same time The sharing of projects by several users means that the UNIX files must be shared between these users and therefore causes the usual problems of access rights between the users To avoid compromising system security Atelier B uses a specific Unix user and group named atelierb Before installing Atelier B you must therefore create an atelierb account and a group with the same name This user and this group must be defined on all the machines where Atelier B is likely to run Th
82. path to the translations directory e the name of the project manager e the list of project libraries Graphical user interface The GUI is already launched and a workspace is opened To obtain information on a project you have to display the Project Properties page ClearSy 45 Atelier B 4 User manual ClearSy 4 2 Projects Advanced usage Properties for project blocks x project software development krt resource file project database home pmauduit AB blocks odp project translate directory nome pmauduit AB blocks lang Configuration Details Users pmauduit Add Libraries PGCD 4 library test Definitions directories Cree Remove orcs Command line interface The user interface is already started up To view the properties of project proj_name type the following command project_infos proj_name or ip proj_name The properties are displayed as follows Name LIFT Database path home projects pdb Translations path home projects transl Manager user Libraries LIBRARY ClearSy 46 Atelier B 4 User manual ClearSy 4 3 Components Management 4 3 Components Management 4 3 1 Adding a Component Description A B project is made up of a list of B components located in text files These components are either directly linked to the project or accessible through libraries The B source files are text files containing one or several components
83. phical user interface This command is not available in the GUI However you can restore the component s sources by hand by following these instructions 1 Uncompress the archive file 2 Open in the GUI the given project 3 Click on the Project gt Add components menu and select the components source files that you want to add to your project Command line interface The user interface is started up you already have opened a project To restore a component use the get_list_from_archive command followed by the restore_source command The get_list_from_archive command displays the list of files in a project archive bbatch 2 gt get_list_from_archive home project tarPROJ arc x tmp atelierb tar 486 bytes 1 tape blocks Printing Components in archive file tarPROJ Acq_1 mch Arithmetic_1 mch Arithmetic_2 imp End of List The restore_source command performs the restore For example to restore the Acq_1 mch compo nent in the MyProj project you must type bbatch 3 gt restore_source home projet tarPROJ arc Acq_1 mch x tmp atelierb tar 486 bytes 1 tape blocks x spec Acq_1 mch 342 bytes 1 tape blocks ClearSy 56 Atelier B 4 User manual ClearSy Applying the B method 5 Applying the B method 5 1 Presentation To develop programs using the B method Atelier B proposes a set of commands allowing e syntax and type checking of components e automatic generation of proof obligations PO
84. ponent is already in TypeChecked state and the user requests Forced Make on the project then the type check will be repeated on this component normal mode The requested operations are only performed if necessary Warning When a Forced Make is requested on the project only the requested operation will be systematically repeated on all the project components For example If you request a Forced Make for the POgenerate operation then the generation of proof obligations will be repeated on all the project components The type check will not be repeated Command line interface The user interface is started up you already have opened a project To perform an operation on all the project components type the following command ClearSy 79 Atelier B 4 User manual ClearSy 5 14 Updating a Project make_all operation force or m Operation force The operation parameter can take one of the following values typecheck pogenerate bOcheck prove The force parameter must equal 0 in normal mode and 1 in forced mode If the requested operation is prove you must give a third parameter which is the prover force level to apply 3 2 1 0 1 2 or 3 Refer to sub section 45 7 5 14 Updating a Project Description When several users are simultaneously working on a large scale project modifying a component can have effects on several other project components on all the components linked to this component The Remake project fun
85. r B 4 User manual ClearSy 4 2 Projects Advanced usage With the user interface running To add the 1ib_name library to the proj project type the following command add_project_lib proj lib_name or apl proj lib_name To display the list of libraries of project proj_name type the following command show_project_libs_list proj_name or spll proj_name The list is displayed as shown below Printing Project proj_name libs list 1lib1 1ib2 End of Project proj_name libraries list To remove the lib_name library from the proj_name project type the following command remove_project_lib proj_name lib_name or rpl proj_name lib_name 4 2 3 Definition files directories Management Description Definition files are a means to share common definitions for several components Their description are given in chapter 2 3 The DEFINITIONS clause of the document Reference Manual for B language This section describes the procedures to follow so as to add a new directory to a B project which can contain definition files used by the components of this project Graphical user interface Still onto the project properties page see the previous screenshot into the Definition directories frame click on the Add button to display a dialog box which allow you to select a directory ClearSy 40 Atelier B 4 User manual ClearSy 4 2 Projects Advanced usage Definitions directories Add On the contrary to del
86. raphical user interface In order to translate a component using the ComenC translator perform the following instructions 1 Select the desired component into the list of components 2 Trigger the Component gt Generate Code menu The following dialog will then appear Translator options x Language ComenC 4 gt Components Al e Selected Only Project e Native Heterogenous Cae oo ClearSy 78 Atelier B 4 User manual ClearSy 5 13 Applying a Tool to all the Components of a Project After having selected the desired options click on the Ok button to confirm and launch the trans lation process Command line interface To translate an implementation imp_name into C language you have to type in the following command ComenCtrans imp_name or b2c imp_name 5 13 Applying a Tool to all the Components of a Project Description The Make project function only available with the command line interface is used to perform on all the components of a project the following operations e syntax analysis and types check e generating proof obligations e proof e checking the translatable language BO This function takes into account the links between project components its operation is similar to the UNIX make function This function proposes two options forced mode The requested operations will be performed regardless of the state of the components For example if a com
87. s for displaying proof obligations e Using the PO Viewer e Using the interactive prover Using the interactive prover is recommended in the following cases e complex assumptions in this case the search functions of the interactive prover are required to analyse these proof obligations e the number of proof obligations is high The PO would rather be displayed one by one which is impossible using the POViewer The Interactive Prover User s Manual sub section 5 4 describes the different methods available for viewing proof obligations This sub section describes the use of the PO Viewer ClearSy 69 Atelier B 4 User manual ClearSy 5 6 Displaying Proof Obligations This tool enables e displaying the proof obligations of a component clause by clause e displaying obvious proof obligations i e those that were eliminated by the proof obligations generator e displaying and printing proof obligations using mathematical fonts via a word pro cessing program I4TfXor Word The proof obligations include comments that specify e the origin of the assumptions for example Component invariant e the theoretical justification of the proof obligation In this case the comment refers to a sub section in thex Proof obligations Reference manual Graphical user interface The GUI is supposed to be launched a project is opened To open the GUI of the interactive prover it is necessary to click on the given compon
88. s however possible to use Atelier B in mono user mode you would although lose in end use flexibility A B project managed by Atelier B can also use other projects regarded as libraries Libraries may be used to split industrial size projects into some smaller projects Atelier B also offers functions to archive projects These functions are used to back up or copy projects For project archiving and portability reasons we encourage Atelier B users to adopt a project layout that obeys the following rules All users of the same project should be in the same UNIX group the atelierb group The project directories should ideally have a common root If project_dir is this di rectory the PDB and the translation directory must be sub directories of project_dir For example project_dir pdb and project_dir lang e The B source files must be located in sub directories of project_dir You can for example define a sub directory for each software element especially if the users who are responsible for them are different e The directories containing definition files see section 4 2 3 must also be sub directories of project_dir ClearSy 30 Atelier B 4 User manual ClearSy 4 1 Projects management 4 1 1 Display the list of projects Description This function is used to display the list of projects accessible to the Atelier B user Graphical user interface Once the workspace is opened the projects list is directly v
89. s with facility to insert them in a component ClearSy 24 Atelier B 4 User manual ClearSy 3 4 Command Mode User Interface 3 4 Command Mode User Interface This user interface allows Atelier B to be used on a terminal as well as in semi automatic mode with a command file This interface is a command interpreter like a shell with the mostly same features as the Atelier B graphical user interface To start up the command mode user interface open a shell window and type the command startBB Under Windows a link exists in the Start menu AtelierB Batch interface To quit the command mode user interface type quit or q You can use this interface in two different ways 1 interactively or 2 with a command file Using a Command File A command file can contain e Comments lines starting with e Atelier B commands long name or abbreviation Example of a command file list of projects show_projects_list users of the LIBRARY project spul LIBRARY contents of the current directory Ms 1 end of the command file To execute a command file only under UNIX like OS type one of the following commands startBB i file_name ClearSy 25 Atelier B 4 User manual ClearSy 3 4 Command Mode User Interface or startBB lt file_name or startBB lt lt END list of commands END Using the Interpreter Some commands have default parameters For project management commands
90. should delete manually those files and directories after deleting the project using Atelier B Graphical user interface This action is available from the Project gt remove menu or from a right click on the workspace view Component Help Open we Close Archive Add Components ypeChec Refresh Components F5 4 Status Edit PatchProver Edit PatchRefiner Properties The files created by Atelier B are destroyed although some information are kept Command line interface The user interface has already been started up To delete a project named proj type the following command remove_project proj or rp proj ClearSy 35 Atelier B 4 User manual ClearSy 4 1 Projects management 4 1 4 Opening and Closing a B Project Description The function Open project grants access to the components of a project Reciprocally the function Close Project closes the previously opened project Graphical user interface To open a project into the interface you have to click on the Project gt Open menu or to right click on the given workspace on the wanted project then click on Open Component Help Close Remove Archive Add Components Refresh Components Status Edit PatchProver Edit PatchRefiner Properties Once the project is opened the components list appears ClearSy 36 Atelier B 4 User manual ClearSy 4 1 Projects man
91. timeout sec 180 E Y Proof Replay A Set timeout sec 180 E w e CEES you can then add a programmed sequence of different forces to your components selection and fully customize your proof You could interrupt the process by defining a timeout Command line interface The user interface is started up you already have opened a project To run the automatic prover on component comp_name type the following command prove comp_name lt force gt or pr comp_name lt force gt The lt force gt value could be 0 1 2 3 for the different prover force levels 1 for Fast prover level ClearSy 72 Atelier B 4 User manual ClearSy 5 8 Interactive Demonstration 2 for the Replay option 3 for the User Pass option 5 8 Interactive Demonstration Description The primary goal of this function is to allow the user to prove manually the proof obligations that were not proved automatically Graphical user interface The GUI is launched and a project is opened In order to launch the interactive prover you have to follow these steps 1 Click on the chosen component from the components list 2 Click on the Component gt Proof gt Interactive Proof menu or use the keyboard shortcut Ctri i From the prover GUI see paragraph 5 6 you can perform a manual proof The progress is indicated via a progressbar situated in the bottom right of the interface In additi
92. to determine project progress This function takes into account the dependencies between project components If some components are not yet present in the project a warning message is displayed The results table is displayed in the Atelier B start up window This table can also be used by the Atelier B documentation tools refer to sub section A The columns in the generated table indicate TC or Typechecked An OK value means that the syntax analysis and type check of the component and all the components it depends on were successfully performed POG or PO Generated An OK value means that the proof obligations were generated for the component nPO or Proof obligations This column contains the number of non obvious proof obliga tions of the component nUn or Unproved This column contains the number of proof obligations for the compo nent that have not yet been proved Pr This column contains the percentage of proof obligations already proven This per centage does not take into account the obvious POs BOc or BO checked An OK value means that the BO check was performed successfully on this component Graphical user interface Once a project is opened the status is directly available on the components view An example is given on the following screenshot blocks Components Hierarchical view Filter Component w TypeChecked POs Generated Proof Obligations Proved Unproved BO Checked E 9 block_occupancy
93. to the action that is executing e The automatic interrupt is used with the automatic demonstration A timeout can be defined for the automatic demonstartion in order to try some prove tactics which can loop or take too much time Graphical user interface The GUI is already launched a project is opened After having selected one or more components click on the button corresponding to the action of your choice Typecheck PO Generate Proof When the action begins it appears into the tasks view It then possible to interrupt it by clicking on the following icon Tasks 08 Hide Finished tasks 2 g Project Component Action Status Messages Server blocks block occupa 4 Finished Typecheck finished localhost Ly Tasks Errors 5 16 Dependencies Management Description For each of the actions described in this chapter Atelier B checks that this action has not already been performed on this component The action is only carried out if the component or the components it depends on have been modified ClearSy 81 Atelier B 4 User manual ClearSy 5 16 Dependencies Management If this is not the case the following messages are displayed Component lt comp_ name gt is already Type Checked or Proof obligations already generated for lt comp_ name gt The functions described below permit you to force the accomplishment of the action Graphical user interface When some actions seem to be
94. ts from existing files you can use the Project gt Add Components menu This will lead you to a file selection dialog Note that the file selection can be multiple if you have to add more than one file Once the desired files are selected confirm by clicking on the Open button An other solution will be to create a new component if it does not exist To do so select in the contextual menu New gt Components or click in the blue icon onto the toolbar It will then ClearSy 47 Atelier B 4 User manual ClearSy 4 3 Components Management display the following wizard Create new component New component Type Machine O Refinement Implementation Refines H block_occupancy Z gt Directory home pmauduiVAB blocks Once the name of the new component the component type the potential rafined component and the destination path are entered click on the Nezt button The wizard will then show you a overview ClearSy 48 Atelier B 4 User manual ClearSy 4 3 Components Management Create new component X Preview aaaa Author pmauduit Creation date jeu janv 29 2009 MACHINE aaaa Command line interface The user interface is started up you already have opened a project To add a component to the current project perform the following operations 1 Go to the directory where the B source file is located using the co
95. uded in the mod file will be deleted 4 3 3 Displaying the List of Components Description This function displays the list of components of a project grouped by B source files names The components are displayed in alphabetical order according to the names of B source files ClearSy 50 Atelier B 4 User manual ClearSy 4 3 Components Management If the components BB BB_1 and AA are present in the same B source file file mod then the components will be displayed in the following way BB AA BB BB_1 On large scale projects the number of components is often very important This function offers several filters permitting to reduce the number of components and to search components by their names The available filters are e Filter according to the component manager user e Filter by type of component machine refinement implementation e Filter by component name Graphical user interface The GUI is already launched and a project is opened The list of components is printed permanently The filters available inside the interface are different comparing to the one of the Command line interface it is possible to e Filter on a component name by giving a search filter into the textbox located on top of the component view e Activate the hierarchical view which will sort the components following a refinement arborescence e Filter on a specific column See below an example of hierarchical display Gaat
96. w Workspace Project Component Hel EF Component Ctrl N Preferences 83 Project Ctrl P out Ciro IS This menu will trigger the display of a workspace creation wizard asking you in a first time to enter a name and a working directory ClearSy 58 Atelier B 4 User manual ClearSy 5 2 Managing workspaces New Workspace New Workspace v Accessible from local host Workspace database directory c AtellerB MAKE_ATB AB press bdb Browse Connect automatically at startup lt Back Next gt Finish Cancel Do not forget to check the options Accessible from local host if the workspace is intended to be local i e if the path is available locally on the workstation and if you want to open automatically this workspace at launch Connect automatically at startup option If you work on UNIX compatible systems the Atelier B integrates parallelization capabilities on remote computers via the use of SSH Then you are able to specify remote machines on a second page of the wizard This step is not necessary if you specified a local configuration but is mandatory if the newly created workspace is intended to be a remote one ClearSy 59 Atelier B 4 User manual ClearSy 5 2 Managing workspaces New Workspace x Servers Remote servers Tasks Os Host Login Passwd Install Ressources Remove Once the wizard ended you are now ready to manage B projects
97. y the C translator after sub directory cpp link edition makefile Translation directory Directives for C compiler sub directory cpp bdy spe Translation directory Object files generated by the C translator blf sub directory c cpp h Translation directory Files generated by the C translator after link sub directory c edition makefile Translation directory Directives for C compiler sub directory c ClearSy 110 Atelier B 4 User manual

Atelier B 4

Contents

Download Pdf Manuals

Related Search

Related Contents