MDELTA - Atelier B
Contents
1. X_wd po file containing the well definedness lemmas X_wd pmi file containing the interactive proof work to be done e For the PMLE of the interactive proof commands of a B component named X option a or p has been selected X_pmi po X_pmi pmi e For the PMLE of the PatchProver file option a or r has been selected PatchProver lemmas PatchProver unresolved contains expressions that could not be analysed be cause of a too imprecise syntax PatchProver res contains the lemmas of PatchProver lemmas and their status after the application of the predicate prover proved or unproved e For the PMLE of each Pmm file option a or r has been selected X lemmas X unresolved X res e A script file called createDelta sh see Step III when the a option has been selected 4 3 Step II Verifying the application of mdelta You have to verify that Step I went smoothly by examining the displayed messages If some of the messages indicate a problem you have to e Analyse the origin of the problem and correct it e start again step I USING MDELTA 13 4 4 Step III Creating the delta PROJECT B project 4 4 1 Manual creation To use Atelier B on the well definedness lemmas generated during the previous step you have to create a fake B project The proof obligations of this project will then correspond to the well definedness lemmas To obtain this project it i2. can now begin to check informally and or prove formally the well definedness lemmas TA component X is considered to be empty if it is reduced to MACHINE X END 14 MDELTA User Manual for the lemma related to components or interactive proof commands just use Ate lier B as usual after opening the delta PROJECTB project As far as the lemmas related to user provided rules included in the files ending in lemmas are concerned theses lemmas cannot be handled through Atelier B V3 7 The files ending in res contain the output of the application of the predicate prover to these lemmas performed during step I that is to say their proof status Proved or Unproved The unproved lemmas must then be proved manually by the user who will have to provide a formal proof document The rules from the unresolved files must be proved manually too But before the manual proof two operations must be performed First the user must translate these rules into mathematical lemmad likely to be proved Once translated the user must deduce from them the corresponding well definedness lemmas using table 3 1 The formal proof of these lemmas makes up the last step of the unresolved files handling 2Use Bibliography 1 B Book Jean Raymond ABRIAL 1996 2 B Language Reference Manual version 1 8 5 ClearSy 3 Partial logics reconsidered a conservative approach Formal aspect of computing Olaf OWE 199
3. 3 4 Traitement des expressions d pourvues de sens de la th orie des ensembles Applica tion la m thode B These de Doctorat Lilian BURDY 5 Rule writing guide version 1 0 ClearSy 15
4. Atelier B MDELTA User Manual version 2 0 Be bh A CLEARS Y SYSTEM ENGINEERING ATELIER B MDELTA User Manual version 2 0 Document made by CLEARSY This document is the property of CLEARSY and shall not be copied duplicated or distributed partially or totally without prior written consent All products names are trademarks of their respective authors CLEARSY Maintenance ATELIER B Parc de la Duranne 320 avenue Archimede Les Pleiades IIl 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 mail contact atelierb eu Contents 1 Introduction 2 Terminology 2 _Abbreviations 3 4 54 e a wa oy OR mo ORO YOU e e 22 Definition of terms used 3 Problem presentation 34 Example kewego lue ne ee ERR ACHSE ee ES 3 2 Well definedness conditions 3 3 Example of well definedness lemma generation 3 4 MLE location 3 5 The mdelta tool for checking well definedness 4 1 When you should use it gud eub Wd wu LEO Rg le Sa ee AUR TIE TFT 4 2 2 OU put ce Ha REGE ROE ee KS RR ee te E voe ee e E Sith ae nu ee 4 4 Step III Creating the delta PROJECT B project 4 4 1 Manual creation kk a a a A a 4 4 3 Script Output 4 5 Step IV Proving the well defin
5. edness lemmas MDELTA User Manual Chapter 1 Introduction A mathematical predicate can be e true e or false provided that it is well defined The ill definedness of a predicatd or of an expression contained in this predicate calls into question the correctness of a proof involving this predicate Atelier B V3 7 does not have any means of its own to detect these meaningless expressions MLE do not allow to guarantee the full validity of a proof work performed with Atelier B V3 7 This issue is addressed by the production of well definedness lemmas by the mdeltatool and by their automatic or manual proof This document defines what are meaningless or potentially meaningless expressions It lays down how you can use the mdelta tool to generate the well definedness lemmas that you will have to prove in order to ensure the correctness of your B development as far as well definedness is concerned The verification that a predicate or expression is well typed is performed by the type checker This verification is independent of the well definedness verification Well definedness is only checked for well typed predicates or expressions 2MLE in abbreviated form see Terminology 3The B method is described in 1 MDELTA User Manual Chapter 2 Terminology 2 1 Abbreviations PO proof obligation POG proof obligation generator PRB prover rule base PDB project database direc
6. lar occasions in the B project devel opment life e When the project has been informally validated all PO seem correct but no formal proof has been performed e and when the proof work has formally validated the project some PMLE may have been introduced during the interactive proof process through the use of commands like ah ph or se or user provided rules 4 2 Step I Running mdelta To launch the tool use the following command mdelta with lt DELTA_CHOICE gt lt ATB_HOME gt lt ATB_RESSOURCE gt lt PROJECT_NAME gt e DELTA CHOICE processing options r to apply the tool to user provided rules Pmm and PatchProver files p to apply the tool to interactive proof commands pmi and po files b to apply the tool to B components nf files any combination of the three options above a to apply the tool with all the options enabled equivalent to r p b e ATB HOME installation directory of Atelier B e ATB RESSOURCE complete path of the Atelier B global resource file e PROJECT NAME project declared in Atelier B to which we want to apply the tool 11 12 MDELTA User Manual 4 2 1 Example mdelta a home atelierb AB home atelierb AB AtelierB DeltaTest 4 2 2 Output The whole output of this step is written in the PDB directory of the PROJECT_NAME project in the form of the following files e For the PMLE of a B component named X option a or b has been selected
7. literal value cis well defined true since it s a variable cis non zero see tabld3 1 third line e x 8 c is non zero see the tabld3 1 third line The well definedness lemmas of expression x x 8 c are therefore Hr2e 8F0 Hr c 0 where H refers to the current hypothesis context 3 4 MLE location MLE can be found for a B project in e B components e project level user provided rules e component level user provided rules e interactive proof commands 3 5 The mdelta tool for checking well definedness The mdelta tool does not exactly detect MLE When applied to a project it generates the well definedness lemmas for all the project PMLE and attempts to prove them auto matically The result is available in a child B project that is automatically created or updated Files affected by the PMLE search are e B component files in normal form files ending in nf e Patchprover file e Pmm files e Pmi and Po files Po files are necessary to get context information The well definedness lemmas are gathered and their origin is identifiable PMLE can be tracked down 10 MDELTA User Manual Chapter 4 Using mdelta 4 1 When you should use it This tool can be applied on any B project anytime during its development without the proof being finished Nonetheless all the components must have been type checked successfully We strongly advise you to use mdelta on two particu
8. o deduce them If it is not the case predicate 3 1 is potentially ill defined 3 2 Well definedness conditions The well definedness conditiondl are listed in the table below Expression Well definedness condition ab ae NAbEN a mod b beN AaEN a b b Zi H z P E alP F 2 P X z P E xlP eF xlP max S SNNEF N ASZO min S SN Z N EeF Z AS Z0 card S S c F S inter U UF A2 PIE zlPY 40 r neN f x x dom f f dom f ran f perm S S c F S conc s s seq ran s Vz r dom s s x seq ran s x s t s seq ran s t seq ran t size s s E seq ran s rev s s E seq ran s see s E seq ran s e gt s s E seq ran s tail s size s gt 1 s seq ran s first s size s gt 1 A s seq ran s front s size s gt 1 A s seq ran s last s size s gt 1 A s seq ran s stn n 0 size s s seq ran s sin n 0 size s s seq ran s Figure 3 1 Potentially meaningless expressions 3 8 Example of well definedness lemma generation Let us consider the x x 8 c expression This expression is well defined if IThis conditions come from 3 and 4 PROBLEM PRESENTATION 9 e x is well defined true since it s a variable e x 8 c is well defined if x 8 is well defined if x is well defined true since it s a variable x 8 is well defined true since it s a
9. roved to ensure that a predicate is well defined Chapter 3 Problem presentation 3 1 Example Let us consider the predicate Y TF8 C 3 1 This predicate can be true or false provided that it is well defined If this predicate is not well defined it is then impossible to associate it a true or false value This ill definedness means that at least one operator of the predicate has at least one operand that does not belong to its domain Predicate is obviously arithmetical by nature We consider that this predicate has been type checked operation performed by the type checker and that y x and c are integers The operators appearing in predicate are e equality An equality a b is well defined on the condition that a and b are well defined e addition An addition a b is well defined on the condition that a and b are well defined e integer division An integer division a b is well defined on the condition that a and b are well defined and b is non zero We will then have to check that e x and c are well defined and it is the case since we have supposed that y x and c are integers e the denominator of x x 8 c is non zero e the denominator of 8 c is non zero To establish that predicate 3 1 is well defined we then have to prove the following lemmas c 0 3 2 7 8 MDELTA User Manual x 8 c 0 3 3 The predicate context has to contain these lemmas in the form of hypotheses or enable t
10. s sufficient to create a project with its pdb src and lang direc tories add to it the empty machines X_wd mch and X_pmi mch corresponding to the previously generated X_wd pmi X_wd po X_pmi pmi and X_pmi po files type check them and apply the proof obligations generator it will not generate any PO as the ma chines are empty to every one of them Once done you have to replace the pmi and po files generated by the proof obligations generator by those created by mdelta The well definedness lemmas are now available for an interactive proof work 4 4 2 Automatic creation The createDelta sh script generated during step I with the a option allows to create a delta_PROJECT B project so as to e display from Atelier B the well definedness lemmas e perform interactive proof work on this lemmas You just have to type in sh createDelta sh 4 4 3 Script Output e If a delta PROJECT project already exists important data po pmi lemmas res and unresolved files from the delta PROJECT PDB are backed up in the same place files are renamed with the backup date appended the project is deleted e the delta_PROJECT project is created again with the fake but necessary for the proof work of the well definedness lemmas components e Files created during step I are moved to the delta_PROJECT project PDB directory 4 5 Step IV Proving the well definedness lemmas You
11. tory PatchProver File containing user provided rules that can be used for a whole project in addition to the PRB rules Pmm file File ending in pmm and containing user provided rules that can be used for a component in addition to the PRB rules Pmi file File ending in pmi and containing in particular the interactive commands entered by the user for every PO of a component PO file File ending in po and containing the PO of one component Component this term applies equally to an abstract machine a refinement or an im plementation in the B sense MLE Meaningless Expression PMLE Potentially Meaningless Expression 2 2 Definition of terms used Logic Solver language The language used to implement some of Atelier B tools and in particular proof rules Proof obligation Logical predicate generated by Atelier B from a component written in the B languagd that has to be proved in order to guarantee the component correctness The B language is described in 2 6 MDELTA User Manual Meaningless Expression B language expression that cannot be given any mathematical interpretation like a partial function applied to a value outside of its domain or the minimum of an empty set Potentially meaningless expression B language expression requiring extra conditions to be meaningful these conditions are listed in table page 8 Well definedness lemma logical predicate that has to be p
Download Pdf Manuals
Related Search