User Manual of the RODIN Platform
Contents
1. After pressing the Finish button the new project is created and appears in the Project Explorer win dow 1 4 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 New x By c gt Go Into Team k Compare With k Restore from Local History You simply click on Delete and your project will be deleted confirmation is asked It is then removed from the Project Explorer window 15 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 cire 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 gt 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 Ecl2. 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 Theorems Label Predicate Add Delete ELE 14 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 Progress Proof Co El Properties amp gt Problems O x Basic Label axm2 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 J ES Abstract Contexts Select abstract contexts of this context El 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 15 There is another way to directly create a new context extending an existing context C Select the context C in the project window then press the right mouse key you will get the f
3. 4 2 Errors The Problems Window When the Static Checker discovers an error in a project a little x x is added to this project and to the faulty component in the Project Explorer window as shown in the following screen shot a Project Explorer za fe D sath eo gt b brp b z car v a celebrity b celebrity ctx 0 b celebrity ctx 1 The error itself is shown by opening the Problems window El Problems 32 Progress Proof Control Properties 11 error O warnings 0 infos Description zs i Errors 1 item 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 Axioms Label Predicate axml PeN ze axm3 kKePNI cb P ze axm k c P c axm5 k n 1d P 29 4 3 Preferences for the Auto prover The auto prover can be configured by means of a preference page which can be obtained as follows press the Window button on the top tooolbar On the coming menu press the Preferences button On the coming menu press the Event B menue then the Sequent Prover and finally the Auto Tactic button This yields the following window i Preferences ype filter text Auto Tactic General Preferences for the Automatic Tactic Event B Enable auto tactic for proving Help Tactics are run as auto t
4. finite s H finite f s fin_fun_img_R Ht fe Sas h H finite S H finite ran f fin_fun_ran_R For applying the previous rule the user has to write the set corresponding to S T in the editing area of the Proof Control Window H fle ST H finite S H finite dom f fin fun dom H For applying the previous rule the user has to write the set corresponding to S T in the editing area of the Proof Control Window H finite S F dn Ve rEeS n lt z H finite S P Jan Yr resS z gt n H finite S E NAVES MAT H finite S E 3n Vz z S gt lt 1 In the four previous rules S must not contain any bound variable 59 H F Jn Vora n lt z H F SCZ Ni H finite S H F dn Vr xeEeS rn HF SCN H finite S Cardinality H a lt b F Q b a 1 H b lt a Q 0 H Q card io bi H a lt b P a b 1 F Q H b lt a P 0 F Q H P card a b H 0 In the two previous rules card a b must appear at top level HL P SCT H P card S lt card T There are similar rules for other cases A The Mathematical Language The syntax type checking and well definedness conditions of the mathematical language are described in a separate document entitled The Event B Mathematical Language B ASCII Representations of the Mathematical Symbols The mathematical symbols used in the Event B mathematical language are Unicode charac
5. Seer 42 Equality Set Theory i AM EZE 1 BHeP GreA E GAF HA TRUE FALSE l FALSE TRUE L Okee lh pha SE 39 UNA go Rist a poi t SAND ew Saas SMI oee a E STE USO E a e UN DAGA Sa E gt eS T Be mam Al B C DA E E Z SS V E EE Do gt Aste N BS SOME PE oon Y Ss gt 5 OS Y H j SI dom ran 5 Y poe seo dom z gt a y gt bj 1 y ran f gt a y gt bj a b 43 PLANE F Ee F E F where F is a single expression S x F 2 F where F is a single expression E F E F where E and F are single expressions loa yeoby f arg br y Ly o k nA gt ale Lety gt 1 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 or type expression gt type expression and t denotes an expression of type Ty Dios 8 E Oy VE Uss GT UY A O AO NI Sipas Ous VU se B In the four previous rules S and T are supposed to be of type P U U thus takes the r le of a universal set for S and T r Y Vir ZU TUE E FUE E E AU UA TT ATA VS Oe Y E E Ada le Te Sr ACS Peas Be S SCA ws E OCA Mm A CB AND DE SS Kej A tas Na S CA EL OCA A vo A PCB ANB Cc S AC BUS Finiteness Cardinality finite 9 T finite a b T finite
6. 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 NOTE The hurried reader can skip these sections and go directly to section 2 8 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 in the toolbar as indicated below File Edit Navigate Search Project Run Refactor Event B Window El ja Project Explorer 0 o O E celebrity Marn After pressing that button the following wizard pops up Mew Carrier Sets 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 0 Carrier Sets Name Add ee Delete D Down ees os h Carrier Sets Constants Axioms Theorems a 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
7. Add Guard Im WEN rmv 2 Add Action Up 22 7 Dependencies variables Invariants Theorems Events be Once an event is selected you can add parameters guards and actions The components of an events can be seen by pressing the little triangle situated on the left of the event name O celebrity 3 celebrity O Events Elements Contents Add Event Add Var o x Add Guard y s grdl Add Action 2 grd 2 grdll x acill 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 N 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 23 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 itis shown how one can add comments on a certain guard Progress Proof Control E gt Problems 3 0O 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 o s MACHINE celebrity 1 REF INES celebr
8. S UT finite S A finite T finite P S finite S finite S xT S 8 V T lt O V finite S A finite T finite r finite r finite a b T card 0 card U EI 1 card P S 2card S card S x T card S x card T card SAT card S card S N T card S UT card S card T card S N T card S 50 S O card S S lt go card S lt 0 AS 2 a0 card 5 E card S gt 0 S lt g bre cardo o Sg card S T Jee S ard S 2775 m 45 Arithmetic ta A ER E 0 E O E E E E E E 0 Ex xlx xff P ss uw F Ex x0x x F H E xa x F Ex a F if an even number of E xa x F Ex x F if an odd number of E 1 0 E 0 E F E F Be E Be 1 eS sj i i where isa literal 1 7 or et On LJ Or be Or iy 2S AE s Ee Se BE OB db Pop tS NJE F e e 2 Where 2 1s a literal 1 computation computation 1 computation computation computation where 2 and 7 are literals where 2 and 7 are literals where 2 and j are literals where 2 and 7 are literals where 2 and 7 are literals 46 E 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
9. e 32 ajo wo seves E 9 od w 3 2 S EE E wl 9 OE 2 w u 8 EE ee E 3 2 1 Variables Creation Wizardj 3 2 2 Direct Editing of Variablesh Oo a os Bebe E 2 eke eeee ee eee sate ee AE S Q bip Soe ees 3 3 1 Invariants Creation Wizard aaa y aaa Aaa s jA Thco ENEE 3 4 1 _ Theorems Creation Wizard DEE EEN a EVE e Z Sos p GAG ee eA AEE See ee eee eee M Q eu eee soda 3 5 1 Events Creation Wizad 3 5 2 Direct Editing of Eventsj eee eee eee eines ena ore ae ee pe oe eee ee ee Of Pec Geer s es a os ee 2 p w S S Q ans ga 2 S eh ee eee eee 2 4 aia be adas sP a 3 9 Adding more Dependencies 3 91 Abstract Event 262d be zobe na e e e e es e es ss eos os Es 3 9 2 putting an Eventi s s Z lt x a Q slk Q WU ela dl sp Ww eb a ee 3 9 3 Merging Events ws su ss 64586560 8 s es s esos is os os s 3 9 4 _ ina e gt a as Ds 305 Variant A 4 Saving a Context or a Machine 4 1 Automatic Tool Invocatlons e 4 2 Errors The Problems Window 2 2 0 00 eee eee ee 4 3 Preferences for the Auto proverh 5 The Proof Obligation Explorer 6 The Proving Perspective Odl Loading a PI OO s racer aaa 62 Whe Proof Vice tasa e NI 7 6 2 1 Description of the Proof Tree 1
10. ever Such events are said to be CONVERGENT In order to make a new event CONVERGENT select it in the Events tab and open the Properties window You can edit the conv area There 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 27 In order to define the variant use the variant wizard as shown below File Edit Navigate Search Project Run Refactor E rz unala Zz er vl v lt e 8 Project Expl 22 Obligation new Variant Wizard a Pi a na After pressing that button the following wizard will pop up R New Variant Expression E riant cone You can enter the variant and then press OKT 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 Navigate Search riz Els ae ls a Pr Save Ex xs gt 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 1t 1s the auto prover 28
11. 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 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 31 Next is a table describing the names of context proof obligations Well definedness of an Axiom axm is the axiom name Well definedness of a Theorem thm WD thm is the theorem name Theorem thm THM thm is the theorem name Next is a table showing the name of machine proof obligations Well definedness of an Invariant nv 1s the invariant name Well definedness of a Theorem thm WD thm is the theorem name Well definedness of an event Guard evt grd WD evt is the event name grd is the guard name Well definedness of an event Action evt act WD l the Sven ners act is the action name Feasibility of a non det event Action evt act FIS En me Ao act 1s the action name Theorem thm THM thm is the theorem name Invariant Establishment INIT inv INV nv 1s the invariant name evt is the event name Invariant Preservation evt inv INV e nv is the invariant name 32 Next ar
12. m Invariant im var1 E 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 More Inv you can enter additional invariants For adding more varlables 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 1t and then press button Up or Down 18 o 20 celebrity 4 ta Variables Name zad Cc Delete Dependencies Variables Invariants Theorems Events i 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 Edit Navigate Search Project Run Refactor Event rz m e ole 3 Project Saniora e O New Ee Wizard After pressing that button the following wizard pops up DI New Invariants Name and predicate yore ze You can then enter the invariants you want If more invariants are needed then press More 19 3 3 2 Direct Editing of Invariants It is also possible to create button Add or remove button Delete invariants by using the central editin
13. 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 B pel s i Br ae lt Create new component r Celebrity gt Cire closure gt conc 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 component machine context etc that can be opened by a multi page editor Container celebrity Browse Component name MEMO Please choose the type ofthe new component Gei Machine O Context can 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 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 s 7 CONTEXT ctx gt EXTENDS D SETS gt CONSTANTS gt AXIOMS gt THEOREMS END Pretty Print Edit Synthesis Dependencies Carrier Sets Constants Axioms Theorems You are in the Edit area allowing you to edit pieces of the con
14. 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 e they simplify a selected hypothesis by decomposing it into several simpler selected hypotheses 47 Axioms FALSE_HYP Gin ae TRUE_GOAL Simplification Conjunction Implication H Q PA AR S E T H Q PA AQA AR S E T H P Q P R F S HP gt RO gt R S IMPANDL MPORL H P OAR S H PVQ R F S 48 Negation Quantification H P x F Q XST L H 3x P F Q x not free in H and Q H P x ALL R H ve Div x not free in H Equality H P E H P E EQL LR eo EEN eh H x c F P x HG E x F P x In the last two rules z is a variable which is not free in E 49 6 8 3 Preferences for the Post tactic The post tactic can be configured by means of a preference page which can be obtained as follows press the Window button on the top tooolbar On the coming menu press the Preferences button On the coming menu press the Event B menue then the Sequent Prover and finally the Post Tactic button This yields the following window iN Preferences a ix Post Tactic ov ep b General Preferences for the Post Tactic apply after every tactic application b Event B Enable post tactic for proving b Help Tactics are run as post tactics b Install Update True Goal Discharge B4free
15. 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 the goal the Proof Control window a small editing area within which you can enter parameters used by some buttons of the Proof Control window the smiley section 6 5 38 Se Y o O crecs 1 O e r 0 O0 e a state Y Goal z et crtlscsri Problems Progress Proof Control Cache Hypothesis wey pov hr de sp se k P Ct lyr G p S rr gt The Proof Control window offers a number of buttons which we succinctly describe from left to right nPP the prover newPP attempts to prove the goal other cases in the list pO 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 editin
16. 1 17 17 18 18 18 19 19 20 20 20 21 21 21 22 24 24 25 25 25 26 26 26 7 28 28 29 30 31 6 2 2 Decoration 0 0 ee ee ee ee et tk kk tk 35 pea ee ee eee SE 35 02 Midi EEN 36 O25 o ooh s x he bo eG oe Q m eee eee eee ee 36 DROP EEDA E SHEE EERE Oe eee eee eee oe ee MA 36 EENEG 37 ee ee III 38 Deo a aa EE 40 Ps P s 40 a ara EEEE eee we eS 40 6 8 The Automatic Post tactich 41 651 EREECHEN 41 6 8 2 Automaticinferencerules 47 A ee ee EE 50 6 9 Interactive Tactics www 82d Ge eee de dee awe Rede Oa REDRESS 50 6 9 1 Interactive Rewrite Rules 30 6 9 2 Interactive Inferencerulesk 36 60 60 pee REM EE V CBee eee ee ee eee ee ee 61 T ESSE CREA AG ERED EVA RES EOE A Be bla 61 phe Gabe tee NEVEM SS D ea ee eee et ee 61 TENA 62 TETERA 63 BO BrackelidolL s syra ce sins rn rad 63 111 Foreword The reader of this Manual is supposed to have a basic acquaintance with Eclipse Basic help about using the Eclipse platform is available on line from the RODIN platform To view it select Help gt Help Contents from the menubar Then select Workbench User Guide in the Web browser window that pops up 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
17. Events Creation Wizard In order to activate the events creation wizard you have to press the corresponding button in the toolbar as indicated below D Ce File Edit Navigate Search Project Run Refactor Event RB Winc e BE Mm oa ix ICH 3 Project Explorer 33 O celebrity 3 New Event Wizard S gt 21 After pressing that button the following wizard pops up Mew Events Parameter identifier s EH Ee AA Guard predicate s Action substitution s ki Guard label s k Action label s 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 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 1t and then press button Up or Down 22 O celebrity 3 celebriy2 6 h Events var grd Elements Contents Add Event Pos INITIALISATION Add Var b s find
18. ML Discharge b Run Debug False Hypothesis Discharge PP restricted Discharge v Seguent Prover Goal in Hypotheses Discharge PP after lasoo Discharge Auto Tactic Goal Disjunct in Hypotheses Discharge PP unrestricted Discharge Functional Goal Discharge b Team Type Rewriter Simplify Simplification Rewriter Simplify Exists Hypotheses Simplify Find Contradictory Hypotheses Simplify Use Equals Hypotheses Simplify Shrink Implicative Hypotheses Simplify Shrink Enumerated Set Simplify Clarify Goal Mixed Implicative Goal Simplify For all Goal Simplify Implicative Hypotheses with Conjunctive RHS Simplify HEAD Implicative Hypotheses with Disjunctive LHS Simplify Conjunctive Goal Split Restore Defaults Apply In the left part you can see the ordered sequence of individual tactics composing the post tactic whereas the right part contains further tactics you can incorporate in the left part By selecting a tactic you can move it from on part to the other or change the order in the left part 6 9 Interactive Tactics In this section the rewrite 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 Rewrite Rules Most of the rewrite rules c
19. User Manual of the RODIN Platform October 2007 Version 2 3 User Manual of the RODIN Platform Contents 1 Project 1 1 1 Project Constituents and Relationshipsj l P ara ee eee eee Pa 2 ho Crans a Profeco cora sedas 3 1 4 Removing a Project e 4 15 ExXportime a Project e e e uz e w k w ese 2 ke k ke ROBA A GSE 4 1 6 Importing a Project s e ee ss ee 5 1 7 Changing the Name of a Project 5 1 8 Creating a Component 5 1 9 Removinga Compare 6 2 Anatomy of a Context 6 ASA AREA ae CE S Q S eee N 2 w S eee E 8 2 1 1 Carrer Sets Creation Wizard 8 eee E ara ora rad 8 22 Pnuimerated OCIS s o s E a E j k Qoa Qe A amp SUQ AA 9 PR COUSIGNIS asar rasa ha Coens HERG 2 Ge Eee 10 2 3 1 Constants Creation Wizard 10 a E ao a Aa EE 11 AAA III 12 24 1 Axioms Creation Wizard 12 arras AA 12 23 Beie da rara ase 13 2 5 1 Theorems Creation Wizard 13 2 5 2 Direct Editing of Theoremsh 14 2 6 Adding Comments 15 2 Dependencies ejidos Q qe wg S s an Se ae g W S S ew bee dee e ee 2 15 2 0 Prey Pon e sse saiae de bbe ed Be E a w w GGG be be W dees amp 16 3 Anatomy of a Machine 3 1 DependenciesS y o ie a ow SRR ee Coed eRe DEES 0 lt
20. actics Install Update True Goal Discharge B4free P1 Discharge Run Debug Goal in Hypotheses Discharge B4free PP Discharge Seguent Prover Functional Goal Discharge Find Contradictory Hypotheses Simplify B4free ML Discharge PP restricted Discharge Post Tactic B4free PO Discharge PP after lasoo Discharge b Team Use Equals Hypotheses Simplify PP unrestricted Discharge Shrink Implicative Hypotheses Simplify Type Rewriter Simplify Simplification Rewriter Simplify False Hypothesis Discharge Clarify Goal Mixed Restore Defaults Apply cnc On the left part you can see the ordered sequence of individual tactics composing the auto prover whereas the right part contains further tactics you can incorporate in the left part By selecting a tactic you can move it from on part to the other or change the order in the left part 30 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 Obligation Explorer x amp gt E brp 2 b amp car v amp celebrity v O celebrity 1 INITIALISATION inv1 INV INITIALISATION inv2 INV find act1 SIM O rmv 1 inv1 INV O rmv 1
21. angle By pressing it one can expand a project and see its compo nents as shown below Project Ex e brp b i car v 23 celebrity celebrity ctx 0 celebrity ctx 1 celebrity 0 celebrity 1 celebrity 2 celebrity 3 bu circ b EE closure b conc We expanded the project named celebrity This 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 Project Explorer CH b 5 celebrity gt u circ lb E2 closure b E conc The following wizard will then appear within which you type the name of the new project here we type alpha New Event B Project This wizard creates a new empty Event B Project in the current Workspace Project name Jalphal
22. 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 the orems and events of a project whereas contexts contain the carrier sets constants axioms and theorems of a project Machine Context variables 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 either of 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 cire closure Cont As can be seen in this screen shot the Project Explorer window contains the list of current project names Next to each project name is a little tri
23. e 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 12 celebrity ctxl X Axioms Name Predicates Add axml COLOR red gree Delete axm2Z red x green axm3 red x orange oe axm4 green orange Dependencies Axioms Theorems Synthesis Pretty Print o E 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 z Z 0 does not allow to prove the well definedness of y x 3 The order must be changed to the following axm2 z Z 0 axml y x 3 The same remark applies to theorems section 2 5 and 3 4 invariants section and event guards sectior 3 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 Navigate Search Project Run Refactor Eve bel a oe s s New Theorems Wizard 13 After pressing that button the following wizard pops up W New Theorems Name and predicate tra f gt wore JL zen 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 button Add or remove button Delete
24. e the proof obligations concerned with machine refinements l evt is 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 I t is the concrete event name Action Simulation evt act SIM eh Me act is the abstract action name Equality of a preserved Variable evt v EQL aa ME na upe P v is the preserved variable Next are the proof obligations concerned with the new events variant Well definedness of Variant Finiteness for a set Variant Natural number for a numeric Variant evt NAT evt is the new event name Decreasing of Variant evt VAR evt 1s 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 IWWD p is parameter name or a primed variable name evt is the concrete event name Feasibility of non det Witness evt p WFIS p is 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 33 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 subs
25. eS gt EEs BE upa n e 5 APIT Ve ES APS DET E dom r lt lt dy E gt y r F eran r dr a gt F er EH Fer FobEecr EHF Sadar BES A En Fer BSF Erer EBnuFer A FeT EHF Sar EdS A Eb Fer EHF er T Es Fer A FET Ferlw dr rew A x gt Fer ES FeE p a Jr Een az gt Feg p lt a dom g lt p U q ErPFeid S BES A F E Eco Fo G e p q EM Fep A EX Geg E G F Hjeplja ErFep A GrHeg re SeT reseT A dom r S FEST pe Bee TA zany aL re Se T reseoT A dom r S A ran r T pe Se TEST NADA ieee Fam Y s fES T fES T A dom f S PES BT FESTA ETS 53 fes gt oT fES T A dom f S T fes T fe S T A ran f fESS gt T fes T A dom f S P fes gt T fe S T A ran f a O E E v V V oo V gt gt in a Sei c C D Co O Y Y di ji 7 Y E E E D C A A E e a V V V V LATINA Sy a Ss Y Y C O j Hom ow C C 1 _ A E ze E E 7 T T ij CE i Y Ss V LC wD WwW z Z E se di D MV VW e e o S SE SO JE SB P DD E amp Pm mm ou A Ne eae D se ZEN ag ag ag Sees sst s geng ZN NON eme r b t Se E r bD t Kg O ret Nah a r P t Na U NVO ASR ETON OES Noe Na RE RA ZN NON TD Nae Ne Nees Ne eS NS v R O q Ds q D s q P s NR Ne rN SE EGE ETS Na D sst RS SN pOg gt s p Ug es riS lU
26. ement right rmv_ 1 rmv_ 1 ANY REFINES x rmv_1 y ANY WHERE x grdl xeQ WHERE grd2 yeQ grdl xeR grdll xbyek grd2 xpbek THEN THEN actll Q Q x act11 R R x END END 26 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 He Pm 1 Paste o x e New Event ene New Local Variable a gt New Guard a grd New Action a act11 New Refine Event e New Witness b rmv 2 Ss 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 rmv 1 S rmv 1 o x 2 gradil xER D grd xb bek 4 acill R z R x Most of the time the predicate is an equality 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
27. equent 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 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 In case the proof tree has no pending node then the sequent of the root node is loaded as explained previously 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 Ir x Search auto rewrite v H goal frees r0 c0 v V gt goal v V ovr in roomke r bp snd c r0 v V eh rO r vw ah c c0 G T goal ML Yen c lt c0 hyp PP 34 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
28. g 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 39 load the next non discharged proof obligation 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 goto the next pending node of the current proof tree 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 al
29. g 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 R M a ME AA D celebrity 4 Invariants Name Predicates Add Q c P invl Delete inv2 _ Up Dependencies Variables Invariants Theorems Events 3 4 Theorems 3 4 1 Theorems Creation Wizard In order to activate the theorems creation wizard you have to press the corresponding button File Edit Navigate Search Project i Ge ai Geb ve e Ye w e Project Explorer 2 o H G celebrit New Theorems Wizard After pressing that button the following wizard pops up Run Refactor Event B Wind R New Theorems Name and predicate 20 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 CH 52 celebrity 4 Si D Theorems El Mame Predicates Add Delete H thm H thm3 Down z Dependencies Variables Invariants Theorems Events 3 5 Events 3 5 1
30. indicated below File Edit Navigate Search Project Run Refactor Event B Window Fre z p SU ia th e e el s oi tS Gr Project Explorer za Me i 2 After pressing that button the following wizard pops up New Enumerated Set Element Element Element You can enter the 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 T COLOR red green and orange in this wizard is to add the new carrier set COLOR section 2 1 and the three constants section 2 3 3 red green and orange Finally it adds the following axioms ction dy COLOR red green orange red green red orange green Z 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 Ge Run Refactor Event B AA AA Ele sl gt es After pressing that button the following wizard pops up Mew Eonstant EE wei 10 You can then enter the names of the constants and an axiom which can be used to define its type Here is an example Mew Constant By pressing the More Axm button you can enter additional axioms For adding more c
31. ipse 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 gt Then enter the file name of the imported project and finally click Finish Like for exporting the menu 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
32. ity 0 SEES celebrity ctx 0 VARIABLES r Q INVARIANTS invl Qc inv C EVENTS In P Q m Pretty Print Edit Synthesis Dependencies 24 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 New x Delete Rename Z Refine Prove fi S SH lt gt Go Into 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 guite 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 ks INITIALISATION b s And remove 1 ie Copy udi E Paste a grdl e New Event s grd2 New Local Variable 4 New Guard O y a New Action gctll e New Refine Event b rmv 2 e New Witness
33. key of the mouse you can copy the part of the proof tree starting at that sequent 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 36 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 We O O 4 cr lt cb 1 O e r 0 O a 1 O e ca cr 1 O erecr 1 O amp k 0 gt cr 1l cb 1 State Y 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 Y s DJ O crecb 1 St r 0 A a 1 O ca cr 1 O 0 crecr 1 O 4 k 0 cr 1 cb 1 State Y Goal E et cr lscb 1 37 Here is the result e Mm lt O crscb 1 O e ca cr 1 O crecr 1 Ob k 0 gt cr l cb 1 State 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
34. l 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 1s 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 El O e eo 0 et crsca et r 0 A a Cr lt ca et a 0 ca cr et r 1 ca cr et a l a r 0 ca cr l 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 40 6 8 The Automatic Post tactic In this section we present the various rewrite or inference rules which are applied automatica
35. lly 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 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 AO JL PNA NOA ASaOA AR L PA AQA AQA AR PA AQA AR Disjunction PV VTV VQ T Pv VLV VQ PV VO Pv VQV ViQV VR T PV VQV VQV VR PV VQV VR Implication Team gt E Lae T Pat I E e L ue PSP o 41 Equivalence Negation Quantification Pel P TSP P Pel P LSP P Per 1 Es Th alo T Sl P EAF E F E F BeEF OUP Sher EGF ARC KR a Lb a gt b a NEE aD A w b Q gt b E FALSE E TRUE E TRUE E FALSE FALSE E TRUE E TRUE E FALSE E Vz PAG Va P A Va Q PV ys PO Ee Peis 5 VIBE ieee
36. o Sees Contexts gt 25 You have then to choose the New Refine Event option The abstract event can then be entered by adding the name of the abstract event here rmv_1 b INITIALISATION b s find v remove 1 rmv_1 x u grdl xeR u grd xbbek D y y b 4 actll R RN x bz rmv Z 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 93 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 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 refin
37. ollowing menu New x Delete E Extend Prove a c gt Go Into Team k Compare With Replace With k After pressing the Extend button the following wizard pops up ji gt New EXTENDS Clause Please enter the name of the new context cance 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 you may have a global view of your context as if it would have been entered through an input text file ctx celebrity ctx 1 x 3 CONTEST celebrity ctx 1 EX TENDS celebrity ctx B CONSTANTS A AXIOMS axml r gt axm2 gt P Dn Pretty Print Edit Synthesis Dependencies 16 3 Anatomy of a Machine Once a machine is created a window such as the following appears in the editing area D 2 MACHINE mch v gt REFINES gt SEES gt VARIABLES gt INVARIANTS gt THEOREMS gt VARIANT gt EVENTS END Pretty Print Edit Synthesis You are in the Edit page allowing you to edit elements of the machine namely dependencies key words REFINES and SEES variables keyword VARIABLES invariants keyword INVARI ANTS theorems keyword THEOREMS variants keyword VARIANTS or events Keywords EVENTS These modelling elements can be edited in a way that is similar to what has been explained for contexts in section 2 1t 1s not repeated here It is also po
38. onstants press Add button When you re finished press button OK 2 3 2 Direct Editing of Constants 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 JE celebrity ctxl E S Constants Name Add red Delete o green h P o orange o bit o bit z Carrier Sets Constants Axioms Theorems o As can be seen two more constants bit1 and bit2 have been added Note that this time the axioms concerning these constants have to be added directly see next section 2 4 Down HAUG 11 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 window For this you have first to select th
39. orrespond to distributive laws For associative operators in connection with such laws as in PA QV VR 50 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 sequence of them For instance we shall never write Q V V R but Q V R instead Rules are sorted according to their purpose 51 Conjunction PA QVR PAQ V PAR Disjunction PV QAR PVQ A PVR BRO aa Vi se APSO Vet R Implication Res AQSA Pe O PRO S R PSO NAJ PSO PS PVO R PSR KO RD Equivalence PSQ P3Q A Q gt P Negation ave Po lena en SILA Verne 5 0 sr m S S Set Theory Most of the rules are concerned with simplifying set membership predicates BeFeSxT BESA FET E eP S ECS SET sevi PES ET In the previous rule x denotes several variables when the type of S and 7 is a Cartesian product 32 BCS OT En Ve BET EESNT EESALEET EESAT EESAT E CET PB gt DEAN AE E union S ds seSA Bes EEJ 2628 S APIT dr rEeSAPA Eet E inter S Vs s
40. previous line Here is an illustration of the previous tree auto rewrite forall goal gt goal Ovr 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 section 6 1 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 ared logo with a in it means that this leaf is not discharged e a blue 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 Note that a reviewed leaf is one that is not discharged yet by the prover Instead it has been seen by the user who decided to have it discharged later Marking nodes as reviewed is very convenient in order to perform an interactive proof in a gradual fashion In order to discharge a reviewed node select it and prune the tree at that node section 6 2 5 the node will become red again undischarged and you can now try to discharge it 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 35 e the button allows you to fully expand the
41. 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 section 6 8 is not applied to the new current sequent if needed you have to press the post tactic button in the Proof Control 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 1t 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
42. r T r S UT 54 dom pUq lt lt dom p U dom q ran p Ug lt lt ran p U ran g SCT UNT C UN S In the previous rule the type of S and T is P U In the previous rule S and T are sets SCANS SCA NS UBEO PUUT dp a Ups gUr p g p U r p p a is alpls sdp q s lt p 4 sdp q s lt p 4 p g gt s p a gt s p q gt s p q Ps OS ATI OS UO T CUSUT AUSSAU v 1 UNSA DO se UN STUT In the three previous rules S and T are supposed to be of type P U Cardinality card S lt card T SCT card S gt card T TCS card S lt card T SCT card S gt eard T TES card S card T S T In the five previous rules S and 7 must be of the same type 55 6 9 2 Interactive Inference rules Disjunction Implication H F 7 Q H Q P F R H P Q F R Equivalence H Q PSQ F GO EQV postponed H P P amp Q F G P Set Theory H G E P F Q H P f 4 E F G F Q H G E F QF H G E F Q G H E QU lt 1 gt F y G H P f lt g G F Q OV_L 56 H Ge dom g F Q g G H G e dom g F Q f G OV R H F O lt 9 G In the four previous rules the lt operator must appear at the top level Hr QS T DIS R DIS_R Hr Q f S ATI In the two previous rules the occurrence of f t must appear at the top level Moreover A and B denote some type Similar left distribution rules e
43. ssible to do so in a different way as explained in sections 3 1 to 3 6 The creation of these elements except dependencies can be made by two distinct methods either by using wizards or by editing them directly In each section we shall review both methods NOTE The hurried reader can skip these sections and go directly to section 3 7 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 in 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 17 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 File Edit Navigate Search Project aalay r v 2 ale e rier Deiere 3 UE O celd New Variable Wizard After pressing that button the following wizard pops up Run Refactor Event B New Variable Identifier EE Initialisation 5 45 Ivar
44. ters beyond the ASCII subset These characters are not always easy to input with a regular keyboard To help users enter these characters a list of standard input strings have been defined When any of these strings is entered it is automatically converted by the user interface to the corresponding Unicode character 1 e mathematical symbol 60 B 1 Atomic Symbols T TRUE TRUE o fe B 2 Unary Operators union union inter B 3 Assignment Operators ESES 61 B 4 Binary Operators Symbol ASCII Symbol ASCII Symbol ASCII 62 B 5 Quantifiers B 6 Bracketing 63
45. text namely dependencies keyword EXTENDS carrier sets keyword SETS constants keyword CONSTANTS axioms keyword AXIOMS or theorems keyword THEOREMS By pressing the triangle next to each keyword you can add remove or move corresponding modelling elements As an example here is what you obtain after pressing the triangle next to the keyword AXIOMS 3 e CONTEXT ctx gt EXTENDS D SETS gt CONSTANTS z AXIOMS Go gt THEOREMS END Pretty Print Edit Synthesis Dependencies Carrier Sets Constants Axioms Theorems D By pressing the button you obtain the following z AXIOMS O axm UNDEFINED H 0 52 You can now enter a new axiom and a comment in the corresponding boxes as indicated below z AXIOMS laxml b0 e BOOKING bg is a constant bboking G 2 You can add another axiom in a similar fashion z AXIOMS t axml bO e BOOKING b0O is a constant booking O laxm2 bl e BOOKING wl another constant booking erg For removing an axiom press the button You can also move an axiom up or down by selecting it press mouse left key when situated on the axiom logo and then pressing one of the two arrows 7 or Other modelling elements are created in a similar fashion It is also possible to do so in a different way as explained in sections 2 1 to 2 7 The creation of these elements except dependencies studied in section
46. xist HE WOK H QED Hr O FHEH SIM R In the previous rule the occurrence of f must appear at the top level A similar left simplification rule exists HE WD O 9 f HF Qo Hr 0 f 9 4 SIM_R In the previous rule the occurrence of f g must appear at the top level A similar left simplification rule exists Finiteness H Sel H finite OI ea SIC H finite S For applying the previous rule the user has to write the set corresponding to 7 in the editing area of the Proof Control Window 57 H finite S V V finite 7 H F finite S n n T fina R H finite S IMA H finite S T H finite S H finite OI H finite r Dm rel H For applying the previous rule the user has to write the set corresponding to S gt T in the editing area of the Proof Control Window H finite r Tim rel mg H H finite r s H finite r fin_rel_ran_R H finite ran r H finite r fin rel dom P H finite dom r H F fe SST H finite 5 H finite f Dm fun1_R For applying the previous rule the user has to write the set corresponding to S T in the editing area of the Proof Control Window H fr e SHT H finite 5 fin_fun2_R H finite f 58 For applying the previous rule the user has to write the set corresponding to S T in the editing area of the Proof Control Window H F fe S T H
Download Pdf Manuals
Related Search