User Manual of the RODIN Platform
Contents
1. 33 6 2 4 OR ee ee tee a 33 62 5 Fuge 2 2s a a ee eee ee ee BOR eee ewe ee M X wd 33 ee ee ATI 33 TIPP 34 TC Tr 35 aaa AAA 37 TTC 37 EE E E 37 6 8 The Automatic Post tactid 37 6 8 1 _ Rewrite SS PO sare reo LA 38 6 8 2 Automatic inference rules 42 6 9 Interactive Tactics ricino RE REE RM SRR AP es ORE EES 44 6 9 1 Interactive Rewriting Rules 44 6 9 2 Interactive Inferencerulesk 49 so 7 1 Syntax for Predicates x eo Roo BEE po RS OR GR x ROE D x m ne Row um e 51 LN BERE NEM AME MA EOM VE ae eee 32 53 8 1 Atomic Symbols 33 ROA EO D RES a Be Le 54 v 54 TT 55 56 5 6 JIBracketib9 SR ox de Bo RTS Ro Re 4 BOR x ba 56 iii The reader of this Manual is supposed to have a basic acquaintance with Eclipse 1 Project 1 1 Project Constituents and Relationships The primary concept in doing formal developments with the Rodin Platform is that of a project A project contains the complete mathematical development of a Discrete Transition System It is made of several components of two kinds machines and contexts Machines contain the variables invariants theorems and events of a project whereas contexts contain the carrier sets constants axioms and theorems of a project Machine Context variables2. S MP AND L eo MPORL H P OAR F S H PVQ R S 43 Negation Quantification H P x 0 XSTL H ix P x Q x not free in H and Q H P x ALL R H Yx P x x not free in H Equality HE P HE L P EQL LR FOLRL H x r E P x HG E x P x In these two rules x 1s a variable which is not free in E 6 9 Interactive Tactics In this section the rewriting rules and inference rules which you can use to perform an interactive proof are presented Each of these rules can be invoked by pressing buttons which corresponds to emphasized red operators in the goal or the hypotheses A menu is proposed when there are several options 6 9 1 Interactive Rewriting Rules Most of the rewriting rules correspond to distributive laws For associative operators in connection with such laws as in PRO Vo VR 44 it has been decided to put the button on the first associative commutative operator here V Pressing that button will generate a menu the first option of this menu will be to distribute all associative commutative operators the second option will be to distribute only the first associative commutative operator In the following presentation to simplify matters we write associative commutative operators with two param eters only but it must always be understood implicitly that we have a seguence of them For instance we shall never write Q V V R but Q
3. pair_expr gt lt relop gt lt pair_expr gt lt predicate gt A G Ire Ee kse ras ae CR d gt Ce 51 7 2 Syntax for Expressions expression lt ident pattern gt lt pair expr gt lt rel set expr gt lt rel set op gt lt set expr gt lt domain mod gt lt rel ezpr gt lt range mod gt lt interval expr gt lt arith_expr gt lt term gt lt factor gt lt image gt MN lt ident pattern gt Je predicate gt expression gt Uf lt ident list gt lt predicate gt lt expression gt Uf lt expression gt lt predicate gt PY lt ident list gt lt predicate gt lt expression gt MN lt expression gt lt predicate gt lt DOIT erpr gt lt ident pattern gt ident pattern gt ident pattern gt H lt ident gt lt rel set ezpr gt gt lt rel set expr gt lt set expr gt lt rel set op gt lt set erpr gt eo Se e Sem 6 6 6 LAT bod e ops Cos oy lt interval expr gt U lt interval_expr gt lt interval expr gt 1 x lt interval emm gt lt interval expr gt lt lt interval erpr gt lt interval expr gt o lt interval expr gt lt interval expr gt lt interval erpr gt domain mod gt lt rel expr gt lt interval emm gt lt lt lt interval erp
4. r BEGIN acil r sc INVARIANTS END invl re P END A D EVENTS Dependencies Pretty Print 22 3 8 Dependencies Refining a Machine A machine can be refined by other ones This can be done directly by selecting the machine to be refined in the Project Explorer window A right click on the mouse yields the following contextual menu Team Compare With Replace With You then press button Refine A wizard will ask you to enter the name of the refined machine The abstract machine is entirely copied in the refined machine this is very convenient as quite often the refined machine has lots of elements in common with its abstraction 3 9 Adding more Dependencies 3 9 1 Abstract Event The absraction of an event is denoted by a Refine Event element Most of the time the concrete and abstract events bear the same name But it is always possible to change the name of a concrete event or the name of its abstraction If you want to specify the abstraction of an event first select the Event tab of the editor and right click on the event name The following contextual menu will pop up 23 bos INITIALISATION b x find remove 1 gt e us Copy x E Paste s grdl e New Event s grd2 New Local Variable y New Guard O y a Mew Action amp SEIT e New Refine Event WES e New Witness Sees Contexts You have then to choose the New Refine Event option The abstract event can then be enter
5. 3 Project Explorer Es g P z brp P EP car v ig celebrity P KS celebrity ctx 0 PO celebrity ctx 1 The error itself is shown by opening the Problems window 21 Proof Control fi Problems 58 Progress Properties 1 error O warnings 0 infos Description v i Errors 1 item 3 Identifier PP has not been declared By double clicking on the error statement you are transferred automatically into the place where the error has been detected so that you can correct it easily as shown below E celebrity ctx 0 x Axioms Label Predicate axml PEN axm3 KePNI Cc P axm KkK c P c axm5 k n 1d P g 5 The Proof Obligation Explorer The Proof Obligation Explorer window has the same main entries as the Project Explorer window namely the projects and its components context and machines When expanding a component in the Proof Obligation Explorer you get a list of its proof obligations as generated automatically by the Proof Obligation Generator 28 2 Obligation Explorer x brp car v celebrity celebrity 1 INITIALISATION inv1 INV INITIALISATION inv2 INV amp find act1 SIM rmv l inv1 INV rmv l inv2 INV rmv 2 inv1 INV rmv 2 inv2 INV As can be seen in this screen shot machine celebrity 1 of project celebrity is expanded We find seven proof obligations Each of them has got a compound name as indicated in the tables below A green logo situated
6. T PV VQV VQV VR PV VQV VR Implication JT ES ee P La se H Pal se pe c E Per Ss J 38 Equivalence Negation Quantification Pel P Ter P Pel P LSP P Pep 1 Es dr alo T epp P EZF E F E F BeEF OUP Sher EGF ARC KR a Lb a gt b a NEE aD A pb hs ep dob E FALSE E TRUE E TRUE E FALSE FALSE E TRUE E TRUE E FALSE E Vr PA AQ Va P A Va Q PV dP V Ee Peis tI Uu VES ss le sse P 39 Equality Set Theory Bose ELE 1 E gt F lt GO gt H E lt GAF lt H TRUE FALSE lt lt L FALSE TRUE L Sil REA SS Y AA Casal sni du MA UA Oh oe IU wur T O ouo SU al E Us DE US AU SU eec Ld sob OE Bee T D 16 25e 2 2 DE ut B e tA Bi Or Th A EU Bes I OBL LS E c x P x P E None Z Ke Ee Dios 9 Pp S dom 4e gt a y gt b x y ran 4z gt a yo gt b a b f Ee FE F EE F E F where Fis 40 a single expression E F E F where E and F are single expressions Lud ej ab e KH Y E dl OS laj ee de PEL E In the three previous rewrite rules Ty denotes a type expression that is either a basic type Z BOOL any carrier set or P type expression or type expression x type expression and denotes an expression of type T y U U S S SU OUT UT UY SLT pese SE ANT O VU e 9 In the four
7. V R instead Rules are sorted according to their purpose Conjunction PA QVR PAQ V PAR Disjunction PV QAR PVQ A PVR PEOVER e POM cV Implication PSO ec PRA OSA PAQSR POAR S PaO eem PQ R SS uS Equivalence Pat P gt Q A Qo P Negation PVG PA Q ANG gt ae P Gel Mee P S05 O ABE Set Theory Most of the rules are concerned with simplifying set membership predicates 45 Bis FP es xt PESA E EERS Beo SCT Vax nes 1061 In the previous rule x denotes several variables when the type of S and T 1s a Cartesian product BEBUL FEES Y BET EESNT beb A Eel EESAT FES A EET Pets Di Env EB E union S ds seSA Bes Bel PERES APIE gt Jue APR EET E inter S Vs seS gt EEs HE res PUNTA SS VES DET E dom r lt lt dy E gt y r F eran r dr r gt F er EH Fer FeEer Be Fuer PES AED er PHASE ET ESC A KE DP EHF e Rar EdS A Eb Fer E gt F er T Ev Fer A FET Fer dr rew A ab Fer ES FE p q Jr Een z gt Feg p q dom 4 lt p U q BweFeid S BES A F E ER FRG ep qg En Ven A EGG ed EG F H ep q EnFep G 5H q 46 rcS T r S oT A dom r 2 S reSeT reS T ran r 2 T r S T reseT don r 2 ran r 2 T fESHT feSSTA Vr y zzz gt yEf A z gt zef gt y z fES T fES T A don f 2S fe SaT esq NT elses fES T fe S T A domf lt S feSoT feS T ran f T feST feS
8. a r 0 ca cr 1 et cs lt cr Such hypotheses can be moved to the Selected Hypotheses window button or removed from the Search Hypotheses window button As for the selected hypotheses other buttons situated next to the previous ones allow you to move or remove all hypotheses By pressing the ct button the negation of the corresponding hypothesis becomes the new goal 6 8 The Automatic Post tactic In this section we present the various re writing or inference rules which are applied automatically as a systematic post tactic after each proof step Note that the post tactic can be disabled by using the P button situated on the right of the proof control window 37 The post tactic is made of two different rules rewrite rules which are applied on any sub formula of the goal or selected hypotheses section 6 8 1 and inference rules which are applied on the current sequent section 6 8 2 6 8 1 Rewrite rules The following rewrite rules are applied automatically in a systematic fashion from left to right either in the goal or in the selected hypotheses They all correspond to predicate logical equivalences or expression equalities and result in simplifications They are sorted according to their main purpose Conjunction PA ATA AQ PA NO PA ALA AQ L PA AOA ASaOA AR L PA NOA NOA AR PRA AQA AR Disjunction PV VTV VO T Pv VLV VQ PV VO Pv VQV ViAQV VR
9. deleted confirmation is asked It is then removed from the Project Explorer window 1 5 Exporting a Project Exporting a project is the operation by which you can construct automatically a zip file containing the entire project Such a file is ready to be sent by mail Once received an exported project can be imported next section it then becomes a project like the other ones which were created locally In order to export a project first select it and then press the File button in the menubar as indicated below File Edit Navigate Search Pro celebrity circ closure Cont A menu will appear You then press Export on this menu The Export wizard will pop up In this window select Archive File and click Next Specify the path and name of the archive file into which you want to export your project and finally click Finish This menu sequence belongs as well as the various options to Eclipse For more information have a look at the Eclipse documentation 1 6 Importing a Project A zip file corresponding to a project which has been exported elsewhere can be imported locally In order to do that click the File button in the menubar as done in the previous section You then click Import in the coming menu In the import wizard select Existing Projects into Workspace and click Next Then enter the file name of the imported project and finally click Finish Like for exporting the m
10. ee Dh AAA BGG 5 2 es aT X wd m PIQUE Un le OA UN E 3 2 1 Variables Creation Wizardj 32 2 Direct Editing of Variables o NS ee eee REI 3 3 1 Invariants Creation Wizard TIT TS 3 1 1 Theorems Creation Wizard SEI SO s ci POVE a GAG ee ee AOE See Ne 0 e 3 5 1 Events Creation Wizad 3 52 Direct Editing of Eventsj eee eee eee eines ena ore ae ee pe oe eee ee ee 5 7 Pec OOM eoe wg os x o3 8 eae owe ee 23 9 eee eee eee ee Dane beh adas ee eee bee ee ae 3 9 Adding more Dependencies 3 91 Abstract Event 4 4 4 sors o a na na RR OR EO RE RO OR S 2 92 putting an Eventi e s uen e a SE ie na ND nes e o Ep a ee T SPE ANTIMESSES INN RE Eee ee ee Eee ee eee a IDA bo en ae E S oe eR ERA eee E SON B ee ea 4 Saving a Context or a Machine 4 1 Automatic Tool Invocations ccs 4 2 Errors The Problems Window 5 The Proof Obligation Explorer 6 The Proving Perspective ol LoadingaProolj e 23x ka d e682 eee idas X 9 Bia 4 P GO 9 Tr 6 2 1 Description of the Proof Tree A ee ee SS ii 16 16 16 16 17 18 18 18 19 19 19 20 20 21 22 22 23 23 23 24 24 25 26 27 27 21 28 6 2 3 Navigation within the Proof Tree
11. evt v EQL evt is the concrete event name kom P v is the preserved variable Next are the proof obligations concerned with the new events variant 30 Well definedness of Variant VWD BEEN Deest Vem EN Natural number for a numeric Variant eut NAT evt is the new event name Decreasing of Variant evt VAR evt is the new event name Finally here are the proof obligations concerned with witnesses evt is the concrete event name Well definedness of Witness evt p WWD pis parameter name or a primed variable name evt is the concrete event name Feasibility of non det Witness evt p WFIS pis parameter name or a primed variable name Remark At the moment the deadlock freeness proof obligation generation is missing If you need it you can generate it yourself as a theorem saying the the disjunction of the abstract guards imply the disjunction of the concrete guards 6 The Proving Perspective The Proving Perspective is made of a number of windows the proof tree the goal the selected hypotheses the proof control the proof information and the searched hypotheses In subsequent sections we study these windows but before that let us see how one can load a proof 6 1 Loading a Proof In order to load a proof enter the Proof Obligation window select the project select and expand the component finally select the proof obligation the corresponding proof will be loaded As a consequence e the proof tree is loaded
12. in the toolbar as indicated below file Edit Navigate Search Project Run Refactor Event B Window 49 Project Explorer Si O Aa After pressing that button the following wizard pops up H New Carrier Sets gore Jl cene You can enter as many carrier sets as you want by pressing the More button When you re finished press the OK button 2 1 2 Direct Editing of Carrier Sets It is also possible to create button Add or remove button Delete carrier sets by using the central editing window see window below For this you have first to select the Carrier Sets tab of the editor Notice that you can change the order of carrier sets first select the carrier set and then press button Up or Down e Carrier Sets Name Add T L Delete mmm Down D Carrier Sets Constants Axioms Theorems As can be seen we have created three carrier sets C E and D 2 2 Enumerated Sets In order to activate the enumerated set creation wizard you have to press the corresponding button in the toolbar as indicated below File Edit Navigate Search Project Run Refactor Event B Window Bala Ji lu se ss 9 Project Explorer 5 D VER suene sale ei New Enumerated Set Wizard After pressing that button the following wizard pops up Hd New Enumerated Set Name COLOR Element red Element a reen Element lorangel More Element Cancel You can enter the
13. in the Proof Tree window As we shall see in section 6 2 each node of the proof tree is associated with a sequent e In case the proof tree has some pending nodes whose sequents are not discharged yet then the sequent corresponding to the first pending node is decomposed its goal is loaded in the Goal win dow section 6 3 whereas parts of its hypotheses the selected ones are loaded in the Selected Hypotheses window section 6 3 e Incase the proof tree has no pending node then the sequent of the root node is loaded as explained previously 31 6 2 The Proof Tree 6 2 1 Description of the Proof Tree The proof tree can be seen in the corresponding window as shown in the following screen shot Project Obligatio Proof Tr auto rewrite zs ON goal frees rQ cQ v 0 goal v ovr in roomke r snd c r8 Yi eh rQ r zan c lt c0 G T goal ML v eh c c0 G hyp PP Each line in the proof tree corresponds to a node which is a sequent A line is right shifted when the corresponding node is a direct descendant of the node of the previous line Here is an illustration of the previous tree auto rewrite forall goal gt goal Ovr eh T goal ML hyp Each node is labelled with a comment explaining how it can be discharged By selecting a node in the proof tree the corresponding sequent is decomposed and loaded in the Goal and Selected Hypotheses windows as explained in
14. obligation 36 e 1 show information corresponding to the current proof obligation in the corresponding window This information correspond to the elements that took directly part in the proof obligation generation events invariant etc e soto the next pending node of the current proof tree e load the next reviewed node of the current proof tree 6 5 The Smiley The smiley can take three different colors 1 red meaning that the proof tree contains one or more non discharged sequents 2 blue meaning that all non discharged sequents of the proof tree have been reviewed 3 green meaning that all sequents of the proof tree are discharged 6 6 The Operator Buttons In the goal and in the selected searched or cache hypotheses some operators are colored in red It means that they are buttons you can press When doing so the meaning sometimes several is shown in a menu where you can select various options The operation performed by these options is described in sections and 6 7 The Search Hypotheses Window A window is provided which contains the hypotheses having a character string in common with the one in the editing area For example if we search for hypotheses involving the character string cr then after pressing the search hypothesis button in the proof control window we obtain the following Search Hypothesis 3 as e ep AO et crsca ct r 0 a a l cr e ca et a 0 ca cr ct r 1 ca cr et a l
15. of these components can be made by two distinct methods either by using wizards or by editing them directly In each section we shall review both methods 3 1 Dependencies The Dependencies window is shown automatically after creating a machine you can also get it by selecting the Dependencies tab This was shown in the previous section so that we do not copy the screen shot again As can be seen on this window two kinds of dependencies can be established machine dependency in the upper part and context dependencies in the lower part In this section we only speak of context dependencies machine dependency will be covered in sec tion 3 8 It corresponds to the sees relationship alluded in section 1 In the lower editing area you can select some contexts seen by the current machine 3 2 Variables 3 2 1 Variables Creation Wizard In order to activate the variables creation wizard you have to press the corresponding button in the toolbar as indicated below 16 File Edit r8 d Qm liar c eje e le 8 Project Explorer 3 CD celgNew Variable Wizard jt After pressing that button the following wizard pops up Navigate Search Project Run Refactor Ewent B Ex n RM New Variable Name Initialisation Invariant Add More Inv Cancel You can then enter the names of the variables its initialization and an invariant which can be used to define its type By pressing button Mor
16. 2 xpbek THEN THEN act11 Q Q x actll R R x END END The parameter x being common to both the abstraction and the refinement does not require a witness whereas one is needed for abstract parameter y In order to define the witness one has first to select the Events tab of the editor for the concrete machine where the concrete event here rmv 1 is selected After a right click a menu appears in the window as indicated rmv 1 o x e New Event s grdi New Local Variable x New Guard grd2 a New Action 4 act New Refine Event gt se rmv 2 e New Witness You press button New Witness and then you enter the parameter name here y and a predicate involving y here y b as indicated below 25 actll R R X Most of the time the predicate is an eguality as in the previous example meaning that the parameter is defined in a deterministic way But it can also be any predicate in which case the parameter is defined in a non deterministic way 3 9 5 Variant New events can be defined in a concrete machine Such events have no abstract counterparts They must refine the implicit empty abstract event which does nothing Some of the new events can be selected to decrease a variant so that they do not take control for ever Such events are said to be CONVERGENT In order to make a new event CONVERGENT select it 1n the Events tab and open the Properties window You can edit the conv area The
17. Hr Q f S V T In the two previous rules the occurrence of f must appear at the top level Moreover A and B denote some type Similar left distribution rules exist M FO WOED nr OEM H FE QKE SIM_R In the previous rule the occurrence of f must appear at the top level A similar left simplification rule exists HOF Via HF QUE ay Hr Q f g x In the previous rule the occurrence of f g must appear at the top level A similar left simplification rule exists 7 Syntax of the Mathematical Language In this section we present the syntax of the mathematical language It comprises two main syntactic constructs namely predicate gt section 7 1 and lt expression gt section 7 2 50 7 1 Syntax for Predicates predicate gt quantifier gt lt ident list gt lt unguanti f ied predicate gt lt simple predicate gt lt literal_predicate gt lt atomic predicate gt lt relop gt lt quantifier gt lt unguanti fied predicate gt VW lt ident list gt Y lt ident list gt lt ident gt lt ident gt lt simple predicate gt lt simple predicate gt lt simple predicate gt lt simple predicate gt lt literal predicate gt lt literal predicate gt lt literal predicate gt 1 V lt literal predicate gt lt atomic predicate gt dE KI finite lt expression gt lt
18. T A dom f 2S feST fe SST ran f T pug lt lt HI UO png ping cary me es sar ries pss Sepp r gt s ge psu eg p sUt ar Sr ULL T 47 FU re ES RER E Et Pellent reset re sUt res N ret rB sat r amp s U r amp t Uq gt s p gt s U q gt s pOg gt s p gt s N g gt s Uq gt s pe s U qe s Nq gt s pe s N q gt s SUT r S U r T pUg S plS UalS dom p Ug dom p U dom q ran p Ug ran p U ran q SCT UNT C UNS In the previous rule the type of S and T is P U E SED acude In the previous rule S and T are sets p gUr p q U p r qUr p g p U r p p a is alpls s lt ip g s lt p 9 sdp q s lt p 4 p g gt s p a gt s p q gt s p a P s UN d AUS UNUS Be H Se UE A Z PINE Es SUT In the three previous rules S and 7 are supposed to be of type P U 48 6 9 2 Interactive Inference rules Disjunction Implication H F Q H Q P F R H P Q F R Equivalence H Q PSQ F GO EUV postponed HP P amp Q GO Set Theory H G E P F Q H P f Ee HIGH F Q H G E C QF H gt G E F Q f G Hr QUE E gt Fj G H P f lt giG F Q OV_L 49 H Ge dom g F Q g G H G e dom g F Q f G OV R HF QL lt g G In the four previous rules the lt operator must appear at the top level Hr QS nT nDIS R DIS_R
19. User Manual of the RODIN Platform July 2007 Version 1 4 User Manual of the RODIN Platform Contents 1 Project 1 1 1 Project Constituents and Relationshipsj l Che EUR RUSSE RE NUR a ee b 1 La Creatino a Profeco cora sedas 3 1 4 Removing a Project ss 3 1 Exportar a Project ee uode s Ro INR ee ede aa AA 4 1 6 Importing a Project 4 1 7 Changing the Name of a Project 5 1 8 Creating a Component 2 1 9 RemovingaComponent 6 2 Anatomy of a Context 6 ZI Cater Sci S x 2 wow EOM E SOR a OE ACE SIR eee don Cas 7 2 1 1 Carrier Sets Creation Wizard d eee E ara ora rad 7 22 _Pn m rated Sets 3 22 xe ee aaa asar A 8 S C TT AA cd ob Coens BR B P NA 9 2 3 1 Constants Creation Wizard 9 cm ON E 10 AAA III 11 2 4 1 Axioms Creation Wizard 11 TP 11 2 3 Beie 23 m eB ROSE yu X PRE Mae d EON o WR RO A a ap eee s doas 12 2 5 1 Theorems Creation Wizard 12 2 5 2 Direct Editing of Theorems 13 2 6 Adding Comments 13 21 Dependencies a ang A er E E RS RIRE SES e eg A 14 2 5 Prey PON e sse saiae A g siaa M ES e E NUS A 15 3 Anatomy of a Machine 3 1 Dependencies s o epa a 3d de
20. and actions The components of an events can be seen by pressing the little triangle situated on the left of the event name celebrity 3 celebrity O D A Events var grd Elements Contents Add Event Add Var o x Add Guard s ard xeQ Add Action a grd ve Up 2 grdll xbyek Down a actll O QMXI a Dependencies Variables Invariants Theorems Events 2 4 As can be seen event rmv_1 is made of two parameters x and y three guards x Q y Q and x gt y k and one action Q Q x These elements can be modified select and edit or removed select right click on the mouse and press Delete Similar elements can be added by pressing the relevant buttons on the right of the window 3 6 Adding Comments It is possible to add comments to variables invariants theorems events guards and actions For doing so select the corresponding modeling element and enter the Properties window as indicated below where it is shown how one can add comments on a certain guard Progress Proof Control E 5 Probleme D Basic Label grdll xPyEk Predicate Comment Multiline comments can be added in the editing area labeled Comments 3 7 Pretty Print The pretty print of a machine looks like an input file It is produced as an output of the editing process G celebrity O E E INITIALISATION Pretty Print MACHINE celebrity 0 BEGIN actl r e P SEES celebrity ctx 0 END VARIABLES find
21. carrier sets invariants constants theorems axioms events theorems We remind the reader of the various relationships existing between machines and contexts This is illustrated in the following figure A machine can be refined by another one and a context can be extended by another one no cycles are allowed in both these relationships Moreover a machine can see one or several contexts A typical example of machine and context relationship is shown below Context Machine refines extends Context Machine refines extends 1 2 The Project Explorer Projects are reachable in the RODIN platform by means of a window called the Project Explorer This window is usually situated on the left hand side of the screen but in Eclipse the place of such windows can be changed very easily Next is a screen shot showing a Project Explorer window Car celebrity circ closure conc As can be seen on this screen shot the Project Explorer window contains the list of current project names Next to each project name is a little triangle By pressing it one can expand a project and see its compo nents as shown below P LE brp P E car celebrity P celebrity ctx 0 P G celebrity ctx 1 P celebrity 0 P celebrity 1 P celebrity 2 P celebrity 3 P i circ P m closure lb E conc We expanded the project named celebrity T
22. component machine context etc that can be opened by a multi page editor Container celebrity Browse Component name NENA Jl Please choose the type of the new component Machine O Context cone Click Finish to eventually create the component The new component will appear in the Project Explorer window 1 9 Removing a Component In order to remove a component press the right mouse button In the coming menu click Delete This component is removed from the Project Explorer window In the next two sections we describe in details first the contexts and then the machines 2 Anatomy of a Context Once a context is created a window such as the following appears in the editing area usually next to the center of the screen a x H Carrier Sets Identifier Add Hel Dependencies Carrier Sets Constants Axioms Theorems 2 It shows that a context is made of various components namely dependencies carrier sets constants axioms or theorems In the next sections we are going to see how to create modify or remove such components The creation of these components except dependencies studied in section 2 7 can be made by two distinct methods either by using wizards or by editing them directly In each section we shall review both methods 2 1 Carrier Sets 2 1 1 Carrier Sets Creation Wizard In order to activate the carrier set creation wizard you have to press the corresponding button
23. e 3 Project Explorer 35 0 celebrity 3 New Event Wizard After pressing that button the following wizard pops up H B New Events Name Variable name s vel Em Guard name s Guard predicate s grdi lgrd2 lgrd3 Action s act lact2 lact3 Add More War More Grd More Act ek Cancel You can then enter the events you want As indicated the following elements can be entered name parameters guards and actions More parameters guards and actions can be entered by pressing the corresponding buttons If more events are needed then press Add Press OK when you re finished Note that an event with no guard is considered to have a true guard Moreover an event with no action is considered to have the skip action 20 3 5 2 Direct Editing of Events It is also possible to perform a direct creation button Add Event of variables by using the central editing window For this you have first to select the Events tab of the editor You can also change the relative place of a variable first select it and then press button Up or Down O celebrity 3 celebrity2 60 HN B Events var grd Elements Contents Add Event K s INITIALISATION Add Var P x find rmv I P3 rmv 2 RER Add Guard Add Action Up Down Dependencies Variables Invariants Theorems Events 2 Once an event is selected you can add parameters guards
24. e Inv you can enter additional invariants For adding more variables press the Add button When you re finished press the OK button 3 2 2 Direct Editing of Variables It is also possible to create button Add or remove button Delete variables by using the central editing window For this you have first to select the Variables tab of the editor You can also change the relative place of a variable first select it and then press button Up or Down s celebrity 4 Fa S 8 Y_ Variables Name Add PI Delete _w 17 3 3 Invariants 3 3 1 Invariants Creation Wizard In order to activate the invariants creation wizard you have to press the corresponding button File E Edit Navigate search Project Run Refactor Event Fis i KN E im yt JE e s 3 Project Explorer e S al New Invariant After pressing that button the following wizard pops up H New Invariants Name and predicate You can then enter the invariants you want If more invariants are needed then press More 3 3 2 Direct Editing of Invariants It is also possible to create button Add or remove button Delete invariants by using the central editing window For this you have first to select the Invariants tab of the editor You can also change the relative place of an invariant first select it and then press button Up or Down IN BEES O celebrity 4 Invariants Name
25. ed by adding the name of the abstract event here rmv 1 P s INITIALISATION P x find v remove 1 rmv 1 o x y grdl xER D grdz xb bek O y y b actll R Rx P rmv 2 3 9 2 Splitting an Event An abstract event can be split into two or more concrete events by just saying that these events refine the former as explained in previous section 3 9 3 Merging Events Two or more abstract events can be merged into a single concrete event by saying that the latter refines all the former This is done by using several times the approach explained in the previous case The constraints is that the abstract events to be merged must have exactly the same actions including the labels of these actions A proof obligation is generated which states that the guard of the concrete event implies the disjunction of the guards of the abstract events 24 3 9 4 Witnesses When an abstract event contains some parameters the refinement proof obligation involves proving an existentially quantified statement In order to simplify the proof the user is required to give witnesses for those abstract parameters which are not present in the refinement those appearing in the refinement are implicitly taken as witnesses for their corresponding abstract counterparts Here is an example of an abstract event left and its refinement right rmv 1 rmv 1 ANY REFINES X rmv 1 y ANY WHERE x grdl xeQ WHERE grd2 yeQ grdl xeR grdll xpyek grd
26. enu sequence and layout are part of Eclipse The importation is refused if the name of the imported project not the name of the file is the same as the name of an existing local project The moral of the story is that when exporting a project to a partner you better modify its name in case your partner has already got a project with that same name maybe a previous version of the exported project Changing the name of a project is explained in the next section 1 7 Changing the Name of a Project The procedure for changing the name of a project is a bit heavy at the present time Here is what you have to do Select the project whose name you want to modify Enter the Eclipse Resource perspective A Navigator window will appear in which the project names are listed and your project still selected Right click with the mouse and in the coming menu click Rename Modify the name and press enter Return then to the original perspective The name of your project has been modified accordingly 1 8 Creating a Component In this section we learn how to create a component context or machine In order to create a component in a project you have to first select the project and then click the corresponding button as shown below celebrity Circ closure canc You may now choose the type of the component machine or context and give it a name as indicated New Event B Component This wizard creates a new Event B
27. his project contains 2 contexts named celebrity_ctx_0 and celebrity_ctx_1 It also contains 4 machines named celebrity_0 to celebrity_3 The icons c or m situated next to the components help recognizing their kind context or machine respectively In the remaining parts of this section we are going to see how to create section 1 3 remove section 1 4 export section 1 5 import section 1 6 change the name section 1 7 of a project create a com ponent section 1 8 and remove a component section 1 9 In the next two sections 2 and 3 we shall see how to manage contexts and machines 1 3 Creating a Project In order to create a new project simply press the button as indicated below in the Project Explorer window celebrity Circ closure conc The following wizard will then appear within which you type the name of the new project here we type alpha Mew Event B Project This wizard creates a new empty Event B Praject in the current Workspace After pressing the Finish button the new project is created and appears in the Project Explorer win dow LA Removing a Project In order to remove a project you first select it on the Project Explorer window and then right click with the mouse The following contextual menu will appear on the screen c Go Into Team d Compare With d Restore from Local History You simply click on Delete and your project will be
28. ich we succinctly describe from left to right p0 the prover PP attempts to prove the goal other cases in the list R review the user forces the current sequent to be discharged it is marked as being reviewed it s logo is blue colored dc proof by cases the goal is proved first under the predicate written in the editing area and then under its negation ah lemma the predicate in the editing area is proved and then added as a new selected hypothesis ae abstract expression the expression in the editing area is given a fresh name the auto prover attempts to discharge the goal The auto prover is the one which is applied automat ically on all proof obligations as generated automatically by the proof obligation generator after a save without any intervention of the user With this button you can call yourself the auto prover within an interactive proof the post tactic is executed see section 6 8 lasso load in the Selected Hypotheses window those unseen hypotheses containing identifiers which are common with identifiers in the goal and selected hypotheses backtrack form the current node 1 e prune its parent scissors prune the proof tree from the node selected in the proof tree show in the Search Hypotheses window hypotheses containing the character string as in the editing area show the Cache Hypotheses window load the previous non discharged proof obligation load the next undischarged proof
29. ight mouse key you ll get the following menu 14 New x Delete E Extend Prove c Go Into Team Compare With Replace With After pressing the Extend button the following wizard pops up ji gt New EXTENDS Clause Please enter the name of the new context cancel You can then enter the name of the new context which will be made automatically an extension of C 2 8 Pretty Print By selecting the Pretty Print tab of the editor you may have a global view of your context as 1f it would have been entered through an input text file e Y p Pretty Print CONTEXT celebrity ctx 1 EXTENDS celebrity ctx 0 CONSTANTS Al AXIOMS axml n gt 0 axm2 P Dn END x Dependencies Carrier Sets Pretty Print 4 15 3 Anatomy of a Machine Once a machine is created a window such as the following appears in the editing area usually next to the center of the screen celebrity O M celebrity A X Dependencies Abstract Machine Select the abstraction of this machine Abstract machine None l k Seen Contexts Select the seen contexts of this machine Es Dependencies Variables Invariants Theorems Events It shows that a machine is made of various components namely dependencies variables invariants the orems variant and events In the next sections we are going to see how to create modify or remove such components Except for the dependencies the creation
30. l E et cr lscb 1 Here is the result 34 S Y lt O O crecb 1 O e ca cr 1 O 9 crecr 1 e k 0 cr l cb 1 et cr lscb 1 Notice that the deselected hypotheses are not lost you can get them back by means of the Searched Hypotheses window section 6 7 The three other buttons next to the red button allow you to do the reverse operation namely keeping some hypotheses The ct button next to the goal allows you to do a proof by contradiction pressing it makes the negation of the goal being a selected hypothesis whereas the goal becomes false The ct button next to a selected hypothesis allows you to do another kind of proof by contradiction pressing it makes the negation of the hypothesis the goal whereas the negated goal becomes an hypothesis 6 4 The Proof Control Window The Proof Control window contains the buttons which you can use to perform an interactive proof Next is a screen shot where you can see successively from top to bottom e some selected hypotheses e the goal e the Proof Control window e a small editing area within which you can enter parameters used by some buttons of the Proof Control window the smiley section 6 5 35 e M o O crecs 1 O r 0 a state Y Goal 3 ct cr lscs 1 Problems Progress amp Proof Control Cache Hypothesis wey pov Ur d ob se Ber PE X fl poo OD A A The Proof Control window offers a number of buttons wh
31. l window section 6 4 This happens in particular when you want to redo a proof from the beginning you prune the proof tree from the root node and then you have to press the post tactic button in order to be in exactly the same situation as the one delivered automatically initially When you want to redo a proof from a certain node it might be advisable to do it after copying the tree so that in case your new proof fails you can still resume the previous situation by pasting the copied version see next section 6 2 6 Copy Paste By selecting a node in the proof tree and then clicking on the right key of the mouse you can copy the part of the proof tree starting at that seguent it can later be pasted in the same way This allows you to reuse part of a proof tree in the same or even another proof 33 6 3 Goal and Selected Hypotheses The Goal and Selected Hypotheses windows display the current sequent you have to prove at a given moment in the proof Here is an example Y v O O cr lt cb 1 O e r 0 O e a 1 O e ca cr 1 O e cr lt cr 1 O e k 0 gt cr 1 cb 1 State M Goal 3 et cr 1 lt cb 1 A selected hypothesis can be deselected by first clicking in the box situated next to 1t you can click on several boxes and then by pressing the red button at the top of the selected hypothesis window o Y 0 O crecb 1 e r g m a 1 O ca cr 1 O 0 cr lt cr 1 O k 0 cr 1 cbh 1 State v Goa
32. name of the new enumerated set as well as the name of its elements By pressing the button More Elements you can enter additional elements When you re finished press the OK button The effect of using this wizard as indicated is to add the new carrier set COLOR section 2 1 and the three constants section 2 3 red green and orange Finally it adds the following axioms section 2 4 COLOR fred green orange red green red orange green orange If you enter several time the same enumerated set element you get an error message 2 3 Constants 2 3 1 Constants Creation Wizard In order to activate the constants creation wizard you have to press the corresponding button in the toolbar as indicated below File Edit Navigate Search Project Rum Refactor Event B d W av Fis El ee Qe Z ar lge let sj rx E Project Explorer 33 D 6 celet After pressing that button the following wizard pops up New Constant Name cst1 Axiom laxm5 eer e You can then enter the names of the constants and an axiom which can be used to define its type Here 1s an example New Constant Name Bit axiom faxm5 bit e 0 1 add moram cancel By pressing the More Axm button you can enter additional axioms For adding more constants press Add button When you re finished press button OK 2 3 2 Direct Editing of Constan
33. on the left of the proof obligation name states that it has been proved an A means it has been proved automatically By clicking on the proof obligation name you are transferred into the Proving Perspective which we are going to describe in subsequent sections Next is a table describing the names of context proof obligations Well definedness of a Theorem thm WD thm is the theorem name thm THM thm 1s the theorem name Next is a table showing the name of machine proof obligations 20 Well definedness of an Invariant inv is the invariant name Well definedness of a Theorem thm WD thm is the theorem name Well definedness of an event Guard evt grd WD ee me sa uae grd is the action name Well definedness of an event Action evt act WD E E the vu Den act 1s the action name Feasibility of a non det event Action evt act FIS m ile SE act 1s the action name Theorem thm THM thm is the theorem name Invariant Establishment INIT nv INV inv is the invariant name evt is the event name Invariant Preservation evt inv INV re E l inv is the invariant name Next are the proof obligations concerned with machine refinements evt 1s the concrete event name Guard Strengthening evt grd GRD grd is the abstract guard name Guard Strengthening merge evt MRG evt 1s the concrete event name Is th Action Simulation evt act SIM Gu b dd even ME act 1s the abstract action name Equality of a preserved Variable
34. previous rules S and T are supposed to be of type P U rid Y Qm AU E PUE E Arithmetic Ere t E a em EE B 0 E 0 E E E E Br xlx ff Bx aF Ex x0x k F 0 E F Ex F if an even number of E xa x F Es F if an odd number of 41 DIE 0 E F E F E gt SE B eg Dc A i lt lt i where iis a literal i i where is a literal 1 3 or L computation where 7 and 7 are literals t lt j or L computation where 2 and 7 are literals sl I or L computation where 2 and 7 are literals 1 gt 3 or L computation where and 7 are literals 1 gt 3 or L computation where and 7 are literals ES PES se Le duc see T os gt c 6 8 2 Automatic inference rules The following inference rules are applied automatically in a systematic fashion at the end of each proof step They have the following possible effects e they discharge the goal e they simplify the goal and add a selected hypothesis e they simplify the goal by decomposing it into several simpler goals e they simplify a selected hypothesis they simplify a selected hypothesis by decomposing it into several simpler selected hypotheses 42 Axioms FALSE HYP Are TRUE GOAL Simplification Conjunction Implication H Q PA AR S E T H Q PA AQA ARSS E T H P Q P R F S HP gt RO gt R
35. r gt Q lt interval emm gt lt interval erpr gt 5 lt interval expr gt lt range mod gt lt interval expr gt MN lt interval expr GH lt interval emm gt lt range mod gt p gt lt interval emp gt lt arith_expr gt lt arith_expr gt pst term sh Sterne lt factor gt 4 x mod lt factor gt lt image gt image gt lt primary gt 4 lt expression gt lt expression gt 32 lt primary gt lt simple erpr gt Poli lt simple erpr gt bool predicate gt lt unary_op gt lt expression gt 1 lt expression gt 4 lt ident list gt lt predicate gt lt expression gt U lt expression gt lt predicate gt H lt expression gt 5 lt expression gt KI U Z NY Ny BOOL TRUE FALSE 9 lt ident gt lt integer literal gt lt unary op gt card P Py union inter dom ran DE DEA vid min max 8 Appendix ASCII Representations of the Mathematical Symbols 8 1 Atomic Symbols 53 8 2 Unary Operators O ah 8 4 Binary Operators Symbol ASCII Symbol ASCII Symbol ASCII 55 8 5 Quantifiers 8 6 Bracketing 56
36. re Predicates dd v invl Delete inv2 wp Variables Invariants Theorems Events 2 18 3 4 Theorems 3 4 Theorems Creation Wizard In order to activate the theorems creation wizard you have to press the corresponding button File Edit Navigate search Project Run Refactor Event B Wind ELLE 4 ler ct vr ad e i e Project Explorer 4 DI G celebrit New Theorems Wizard After pressing that button the following wizard pops up H New Theorems Name and predicate yore ze You can then enter the theorems you want If more theorems are needed then press More When you are finished press the OK button 3 4 2 Direct Editing of Theorems It is also possible to create button Add or remove button Delete theorems by using the central editing window For this you have first to select the Theorems tab of the editor You can also change the relative place of a theorem first select it and then press button Up or Down L celebrity 4 Ed B Theorems Name v c dd Delete D Em H thm3 zl Down Dependencies Variables Invariants iants Theorems Events a 19 3 5 Events 3 5 1 Events Creation Wizard In order to activate the events creation wizard you have to press the corresponding button in the toolbar as indicated below File Edit Navigate Search Project Run Refactor Event B Winc Qi lice v C v6 a s S Se t
37. re are three options ORDINARY the default CONVERGENT or ANTICIPATED The latter corresponds to a new event which is not yet declared to be CONVERGENT but will be in a subsequent refinement In order to define the variant use the variant wizard as shown below File Edit Navigate Search Project Run Refactor E 2 Project Expl M Obligation New Variant Wizard Eh A a S IC D Ar Z ee v ES After pressing that button the following wizard will pop up H New Variant Expression variant aea 26 You can enter the variant and then press OK The variant is either a natural number expression or a finite set expression 4 Saving a Context or a Machine Once a machine or context is possibly partly only edited you can save it by using the following button File Edit Mavigate Search a Pr Save Ex T Obligat 4 1 Automatic Tool Invocations Once a Save is done three tools are called automatically these are e the Static Checker e the Proof Obligation Generator e the Auto Prover This can take a certain time A Progress window can be opened at the bottom right of the screen to see which tools are working most of the time it is the auto prover 4 2 Errors The Problems Window 99 499 When the Static Checker discovers an error in a project a little x is added to this project and to the faulty component in the Project Explorer window as shown in the following screen shot
38. section 6 1 32 6 2 2 Decoration The leaves of the tree are decorated with three kinds of logos e a green logo with a in it means that this leaf is discharged e a red logo with a in it means that this leaf is not discharged e ablue logo with a R in it means that this leaf has been reviewed Internal nodes in the proof tree are decorated in the same but lighter way 6 2 3 Navigation within the Proof Tree On top of the proof tree window one can see three buttons e the G buttons allows you to see the goal of the sequent corresponding to the node e the button allows you to fully expand the proof tree e the allows you to fully collapse the tree only the root stays visible 6 2 4 Hiding The little triangle next to each node in the proof tree allows you to expand or collapse the subtree starting at that node 6 2 5 Pruning The proof tree can be pruned from a node it means that the subtree starting at that node is eliminated The node in question becomes a leaf and is red decorated This allows you to resume the proof from that node After selecting a sequent in the proof tree pruning can be performed in two ways e by right clicking and then selecting Prune e by pressing the Scissors button in the proof control window section 6 4 Note that after pruning the post tactic is not applied to the new current sequent if needed you have to press the post tactic button in the Proof Contro
39. ts It is also possible to create button Add or remove button Delete constants by using the central editing window For this you have first to select the Constants tab of the editor You can also change the relative place of a constant first select it and then press button Up or Down E celebrity ctxl HM Constants Name Add red Delete e rear _w o orange Down o bit Down o bit Carrier Sets Constants Axioms Theorems s As can be seen two more constants b t1 and bit2 have been added Note that this time the axioms concerning these constants have to be added directly see next section 2 4 2 4 Axioms 2 4 1 Axioms Creation Wizard In order to activate the axioms creation wizard you have to press the corresponding button in the toolbar as indicated below File Edit Navigate Search Project Run Refactor Eve New Axioms Wizard After pressing that button the following wizard appears H New Axioms Name and predicate laxm7 You can then enter the axioms you want If more axioms are needed then press More When you are finished press OK 2 4 2 Direct Editing of Axioms It is also possible to create button Add or remove button Delete axioms by using the central editing windo
40. utton Add or remove button Delete theorems by using the central editing window For this you have first to select the Theorems tab of the editor You can also change the relative place of a theorem first select it and then press button Up or Down 5 x Theorems Label Predicate Add Delete ELIE 2 6 Adding Comments It is possible to add comments to carrier sets constants axioms and theorems For doing so select the corresponding modeling element and enter the Properties window as indicated below where it is shown how to add comments on a certain axiom 13 Progress Proof Co Properties amp gt Problems O Basic Label axmz ceP Predicate Comment Multiline comments can be added in the editing area labeled Comments 2 7 Dependencies By selecting the Dependencies tab of the editor you obtain the following window a X H Abstract Contexts Select abstract contexts of this context Danz E EZ Dependencies Carrier Sets Constants Axioms Theorems gt r This allows you to express that the current context is extending other contexts of the current project In order to add the name of the context you want to extend use the combobox which appears at the bottom of the window and then select the corresponding context name There exists another way to directly create a new context extending an existing context C Select the context C in the project window then press the r
41. w For this you have first to select the Axioms tab of the editor You can also change the relative place of an axiom first select it and then press button Up or Down 11 C tcelebrity ctx1 X Axioms Name Predicates Add axml COLOR red gree Delete axm2Z red green axm3 red orange _w axm4 green orange Dependencies Axioms Theorems Synthesis Pretty Print o Note that the Up and Down buttons for changing the order of axioms are important for well definedness For example the following axioms in that order axml y x 3 axm2 x Z U does not allow to prove the well definedness of y x 3 The order must be changed to the following axm2 x Z U axml y x 3 The same remark applies to theorems section 2 5 and 3 4 invariants section and event guards section3 5 2 2 5 Theorems 2 5 1 Theorems Creation Wizard In order to activate the theorems creation wizard you have to press the corresponding button in the toolbar as indicated below File Edit Navigate Search Project Run Refactor Eve se a upi el a e vg S co New Theorems Wizard EME After pressing that button the following wizard pops up 12 H New Theorems Name and predicate wore Jl cene You can then enter the theorems you want If more theorems are needed then press More When you are finished press OK 2 5 2 Direct Editing of Theorems It is also possible to create b
Download Pdf Manuals
Related Search