Home

RODIN Deliverable D30

1. 5 1 7 Changing the Name of a Project e o 5 1 8 Creating a Component 5 1 9 Removing a Component 6 2 Anatomy of a Context 6 PREIS S SR a ae R eA Ge EN 8 2 1 1 Carrier Sets Creation Wizard 8 eee eee ara ora rad 8 7 2 EnutWebated OCIS 5 3 koe eG A OR ER 9X SE E 9X P EEE S9 amp s 539 9 po CORSA ooo a ba dede ER B P S SE 10 2 3 1 Constants Creation Wizard 10 a E ao a Aa EE 11 24 AMOS canoa aras aa AAA AAA ES 12 2 4 1 Axioms Creation Wizard 12 arras AA 12 2 3 CO AS 2o pra Ae 13 2 5 1 Theorems Creation Wizard 13 T 14 2 6 Adding Comments 15 2 Dependencies ejidos rear ara 9 ow X bee dee woo A 15 2 0 Prey Pon e sse saiae de bbe ed Rows wo Row XE 9 4 be dk 9 dees A 16 3 Anatomy of a Machine 3 1 JD pendeneles s o ie a ow SRR ee Coed eRe DEES CR Ewe BGG 32 ValiaDles uus wo USE E m od oe me m E EE E m PG ee EE ee E 3 2 4 Variables Creation Wizard 32 2 Direct Editing of Variables 3 3 a uos wo 9 4 892 9 29 ww EUR e BRE ee BGs Sx Hebe Soe 9 3 3 1 Invariants Creation Wizard TIT ST NEUTER EEEEIILITIT 2 ook e ee eee HERE E EEE EERE EA DEES 3 4 1 Th
2. variant x lt variant gt end context lt context identifier gt extends x lt context identifier gt sets x lt set identifier gt constants x lt constant identifier gt axioms x lt label gt lt predicate gt theorems x lt label gt lt predicate gt end In these descriptions section names that is axioms extends etc followed by a star are optional Notice that all machine and context identifiers must be distinct in the same model A model can only contain contexts or only machines or both In the first case the model represents a pure mathematical structure In the third case the machines of the model are parameterized by the contexts Finally the second case represents a machine which is not parameterized Notice that invariants axioms and theorems denote predicates which are labelled such labels must be distinct within a given section Predicates are defined by means of the Event B mathematical language section 6 The variant section is explained in section 3 The previous representation of machines or contexts as well as the usage of keywords do not form a syntax as there is no such syntax in the Event B notation The only part of the Event B notation which depends on a well defined syntax is the Event B mathematical notation section 6 2 Events A machine event represents a transition It is essentially made of guards and actions section 4 The guards together
3. Start RODIN You should be directed automatically to the Event B perspective If this does not happen you will have to change to this perspective manually Eclipse help describes how this is done Create a new Project as described in section 1 3 of the Manual Name the project BirthdayBook Create a new Context Component named BirthdayBook CO in the Project you created This can be done similarly to creating the new project See also Section 1 8 of the Manual In this model we are not interested in the specific structure of the date All we want this context to contain are two carrier sets one for dates and one for people We will call them DATE and PERSON You can add them to the context as described in section 2 1 of the manual Now either press Ctrl S or click on the save Icon to save the context Now we need to create a Machine Component Proceed as you did to create the Context Component just choose Machine this time Give the Machine Component the name BirthdayBook 0 Once the component is created a window with the machine s dependencies appears Add BirthdayBook_CO to the seen contexts so that you can access the carrier sets We need a variable that reflects the contents of the book We call it birthday The following information on the variable can be entered into the New Variable Wizard Manual Section 3 2 1 which can be accessed by an icon on the tool bar Since every person has at most one entr
4. predicate C predicate predicate lt predicate predicate predicate predicate predicate predicate V predicate predicate 1 7 ident list predicate 2 ident list predicate finite C expression expression expression expression expression expression lt expression ident list ident list ident ident The ellipsis which appears at the end of the predicate production rule means that there are still more alternatives combining two expressions into a predicate All those alternatives are not really relevant at this point of the doc ument but will be fully listed in the final syntax see section on page 10 3 2 2 Associativity of operators In this document we use the term associativity with somewhat two different meanings In a mathematical context when we write that an operator say o is associative we mean that it has a special mathematical property namely that xoy oz has the same value as xo yoz In a syntactical context we say that an operator is left associative when formula x o y o z without any parenthesis is parsed as if it would have been written x o y o z To avoid any ambiguity we will always write associative in the algebraic sense when we refer to the first meaning the bare word associative always having
5. 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 triangle By pressing it one can expand a project and see its compo nents as shown below amp Project Ex e brp P EP car v 23 celebrity 9 celebrity ctx 0 celebrity ctx 1 celebrity
6. 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 entere 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 oy COLOR red 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 NM Run Refactor Event B AA ua Ds c se ser gt After pressing that button the following wizard pops up Mew Constant 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 constants 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 ha
7. Theorem 3 is very similar to Theorem 2 Proving also works in a very similar fashion except that it takes a few steps more as we do not have any axioms on f t Then Theorem 1 usually is useful 5 4 Exercise Theorem 4 Theorem 4 states that Vb f b C b t b C b Once again you will need the right instantiation of a hypothesis to succeed with the proof at some stage Here N b x N U b x b will be a good instantiation This proof is quite lengthy as there are many proofs by cases that you will need to perform A lot of the cases can be solved by successfully adding the negation of a selected hypothesis and thus creating a contradiction 13
8. next to then In the end your proof should look like in Figure 2 10 T 10 E Quick dilds Radin Platfarm File Ed amp Masque Search Project Run Editor Menu Windies Help CH bal A Lee rire GH e x T DI Proving ET Quick E Event B Resource El Java Galois D coti G cb GP ccictx D Galois BH Se Selected Hypotheses Bg oi Ten ca N ry el ten ca N p Ih Bde fet E nw t fct n a e e fgs amp fc amp tra E x e OM ei Xl ver oi viet EI EN Stake Goel AE e xl weet Proof Control 22 Problems NELLE er Oran ee TESI Tactic applied successfully Figure 2 The proof after step 6 As the goal appears to be provable from t f C t r x0 f and z1 x t remove all the other hypotheses if you like to keep your workbench tidy This can be done by choosing the three hypotheses and then clicking the Inverse selection button first and then the Remove hypotheses button To prove the current goal we first prove that x1 x0 t f From that xl gt x0 t follows because of t f C t Add the hypothesis 71 x0 t f by entering it in the proof control and pressing the ah button Once more the proof will branch For the first branch click on the red symbol in the Proof Goal window to translate the goal into predicate calculus You will then need to instantiate a variable but the choice should be obvious if you look at the selected hyp
9. remove or move corresponding modelling elements As an example here is what you obtain after pressing the triangle next to the keyword AXIOMS Q e CONTEXT ctx gt EXTENDS D SETS gt CONSTANTS 7 AXIOMS ect gt THEOREMS END Pretty Print Edit Synthesis Dependencies Carrier Sets Constants Axioms Theorems D By pressing the button you obtain the following 7 AXIOMS e 20 axm UNDEFINED Il eoo You can now enter a new axiom and a comment in the corresponding boxes as indicated below v AXIOMS eo laxml bO e BOOKING bO0 is a constant booking eso You can add another axiom in a similar fashion 7 AXIOMS t axml bO e BOOKING bO is a constant booking laxm2 bl e BOOKING another constant booking e v2 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 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
10. 0 celebrity 1 celebrity 2 celebrity 3 b GS circ b LE closure P LE conc We expanded the project named celebrity This project contains 2 contexts named celebrity ctx 0 and celebrity cp 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 E Project Explorer CH P 5 celebrity P gB8 circ IP LE closure PE 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 Project in the current Workspace Project name alpha 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 Exp
11. 3 Priority of operators INN od 3 2 4 Final syntax for predicates 3 3 Expressions 3 3 1 Some Fine Points 3 3 2 A First Attempt 3 3 3 Operator Groups 3 3 4 Priority of Operator Groups 3 3 5 Associativity of operators 3 3 6 Final syntax for expressions 4 Static Checking 4 1 Abstract Syntax 4 2 Well formedness 4 3 Type Checking 4 3 1 Typing Concepts 4 3 2 Specification of Type Check 4 3 3 Examples 5 Dynamic Checking 5 1 Predicate Well Definedness 5 2 Expression Well Definedness 1 Introduction This document presents the technical aspects of the kernel mathematical lan guage of event B Beyond the pure syntax of the language it also describes its lexical structure and various checks both static and dynamic that can be done on formulas on the language The main design principle of the language is to have intuitive priorities for operators and to use a minimal set of parenthesis except when needed to resolve common ambiguities So the emphasis is really on having formulas unambiguous and easy to read The first chapter describes the lexicon used by the language then chapter two describes its concrete syntax Chapter three introduces the notion of well formed and well typed formula static checks Finally chapter four gives the well definedness conditions for a formula dyna
12. 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 18 HR 0 celebrity 4 3 S Variables Name aca Em Delete Dependencies Variables Invariants Theorems Events 5 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 Bd cas ole 3 Project m WD E O New Ee Wizard After pressing that button the following wizard pops up DI New Invariants Name and predicate yore EE 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 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 CREO TTD D celebrity 4 Invariants Name Predicates Add QcP invl Delete inv2 _ Up Dependencies Variables Invariants The
13. Event Add Var o x Add Guard ey s grdl Add Action 2 grd 2 grdlil actii 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 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 it is shown how one can add comments on a certain guard Progress Proof Control E Problems 3 0O Basic Label grall 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 58 MACHINE celebrity 1 REFINES celebrity 0 SEES celebrity ctx O0 VARIABLES r Q INVARIANTS invl Qc inv C EVENTS I 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 m
14. For this it is advisable for you to have some knowledge of the theory but you can also see this as a pure proving exercise First we try to perform a proof without the predicate prover in order to get familiar with all the tools Then you can try proving three further theorems by yourself 5 1 First proof on Transitive Closure 1 Open the Closure project it is a simple mathematical model in which f is a binary relation The axiom defines so that it is the transitive closure of f You will have to prove that t t C t 2 For that we have to instantiate the s of Ys f C sAs f C s t C s with CN x N N t e UN x N t This instantiation is a Galois transform The project Galois shows the properties of galois transforms Simply said these transforms are a sort of inverse for the subset relation between relations In the proof this is useful as we can easily derive the goal from the implication Because of the main property of the Galois transform t C s is equivalent to t t C t The first part of the condition of the axiom also becomes easy to prove as f C s is equivalent to t f C t However the second part of the condition s f C s does not have such an easily provable equivalence We will just have to believe that the instantiation also works here 3 If you want to check that the instantiation really does work you can use the predicate prover now and it will succeed Afterwards prune the predicate prover step
15. H expression expression Y E WN Ny BOOL TRUE FALSE 2 ident integer literal card P P4 union inter dom ran prj prj gt id min max 20 4 Static Checking This chapter describes how mathematical formulae predicates and expressions are to be statically checked for being meaningful We first describe an abstract syntax for formulae Then we state the static checks that are to be done based on that abstract syntax e well formedness e type check 4 1 Abstract Syntax In this section we specify an abstract syntax for mathematical formulae This abstract syntax is based on the concrete syntax described in Section 3 2 4 on page 10 and Section 3 3 6 on page 18 The difference is that the abstract syntax only conserves the essence of the concrete syntax So all concrete matter like priorities and tokens do not appear anymore The abstract syntax is described using production rules Each rule has its own label It is made of a left hand part which denotes some kind of formula predicate expression identifier list expression list and a right hand part which denotes a list of sub formulae together with some attributes To distinguish an attribute from a sub formulae we enclose the former within square brackets Moreover to make rules short we use single letters possibly subsc
16. Let a be a fresh type variable in FE ityvars E ityvars U a Ey ityenv E ityenv Fy 1tyeqs E ityeqs P anherited E synthesized E styvars P styvars E styenv P styenv E styeqs P styeqs U E type T where and 7 are defined in the following table expr bool E P I4 2nherited E inherited E synthesized P synthesized E type BOOL expr eset E M M inherited E inherited E synthesized M synthesized E type P M type 33 expr ident E I I1 inherited E inherited E synthesized I4 synthesized E type I type expr atom E expr lit Let a be a fresh type variable in E styvars E ityvars U a E styenv E ityenv E styeqs E ityeqs E type T where 7 is defined in the following table integer natural naturall P Z expr int E int lit E synthesized E inherited E type Z pattern Q Q1 Qo Q1 inherited Q inherited Q inherited Q1 synthesized Q synthesized Qo synthesized Q type Q1 type x Q type pattern ident Q I I inherited Q inherited Q synthesized I synthesized Q type I type 34 expr list M Ej Eo En E inherited M inherited Es inherited E4 synthesized E inherited Es 4 synthesized M styvars E ityvars M styenv E ityenv E type Es type ba Dune E3 type M styeqs E ityeqs U En 1 type E type M type E type 4 3 3 Examples In this subsection we present a few example
17. Osaka ER E 0 E O E E E E E E 0 Ex xlx xff Ex zb Ex x0x P H E F Es F if an even number of E F Es F if an odd number of E 1 0 E 0 CEJ F E F B E E ex Jem x i i where iis a literal 1 7 or 1x oor LJ Or taJ il Or iy m AE OE Ee BR 4 Hilt E B xo ume e i where 2 1s a literal 1 computation computation 1 computation computation computation where 2 and are literals where 2 and 7 are literals where 2 and j are literals where 2 and 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 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 gt S E T H Q PA AQA AR S E T H P Q P R F S H P R Q gt R Ft S gt gt IMP_AND_L eo MPORL H P Q ARF SS H PVQ R F S 48 Negation Quantif
18. Shrink Implicative Hypotheses Simplify Type Rewriter Simplify Simplification Rewriter Simplify False Hypothesis Discharge Clarify Goal Mixed Restore Defaults Apply cen 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 P E brp gt amp car v amp celebrity v Q celebrity 1 INITIALISATION inv1 INV INITIALISATION inv2 INV find act 1 SIM O rmv 1 inv1 INV rmv 1 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 ob
19. The before after predicate may contain all variables of the machine they denote the corresponding values just before the action takes place It can also contain some of the variable identifiers of the list such identifiers are primed they denote the corresponding values just after the action has taken place Example suppose we have three variables x y and z Here is a non deterministic action zu Su A Yy gt i 2 Variable x becomes greater than y and the variable y becomes greater than x the new value for x added to z a variable which is not modified A final option is to define a non deterministic action as a variable identifier not a list followed by followed by a set expression This is illustrated below lt variable identifier gt lt set expression gt This form is just a special case of the previous one It can always be translated to a non deterministic case as shown in the following example Suppose a machine with variables A x and y Here is an action x AU y which is the same as x xp uw uc Variable x becomes a member of the set A U y whereas variables A and y are not modified Finally notice that all actions in the same event must be concerend with different variables As an example it is not possible to have the following actions in the same event T 5 x L gt r 5 Witnesses When a concrete event refines an abstract one which is parameterized then all abstract parameters must
20. and f are assigned the same type but that type is arbitrary These two notions of satisfiability are extended to sets of type equations with the additional proviso that the satisfying assignment of type variables is done globally for all type equations in the set For instance the set a Z B BOOL is uniquely satisfiable while the set a Z a BOOL is not satisfiable although each equation taken separately is satisfiable 4 3 2 Specification of Type Check The abstract grammar of expressions is extended with the following attributes e Attribute ityvars resp styvars is inherited resp synthesized and con tains the set of type variables that have been used so far 2 e Attribute ityenv resp styenv is inherited resp synthesized and con tains the current typing environment e Attribute ityeqs resp styeqs is inherited resp synthesized and contains the set of typing equations that have been collected so far e Attribute type is synthesized and contains a type These attributes are added to all non terminals except type which is not defined for predicates there is no type associated with a predicate nor list of identifiers Type checking then consists of initializing the attribute grammar by giving values to inherited attributes of the root R of the tree and then evaluating the attribute grammar Type check succeeds iff after evaluation the set of typing equations R styegs is uniquely sa
21. 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 PVO Veas Vi APS NO Vet R Implication Res AQSA PSO IOS POAR PSO PS PADO RH PSR OR Equivalence PeQ P3Q Q5 P Negation yap lena en eo wd Verne 5 Ses Set Theory Most of the rules are concerned with simplifying set membership predicates ER F e SxT E SA FET EcP S ECS SET Vi res ET In the previous rule x denotes several variables when the type of S and T 1s a Cartesian product 32 BCS OT que gy beonT EeS EeT EESAT FES A EET Ed Di gt DEAN psp E union S ds scS Ecs EEJ eres APIT Ar t ESAPAEET E inter S Vs seS gt EEs EE Tes TES APIT Ve ES APS DET E dom r Jy Hauer Feran r dr rryFer E Fert Fe Eer EcFeSadr EES A EeFer BSF Erer bceFer FeT BeFeSdr EGS Ee Fer E gt F er T Es Fer A FET Ferlw Jr 1 Ew xkFer E FE p q Ar Errep x Fcq p q dom q lt p U q ErPFeid S BES A F E BEe FRG E p q EM Fep A EX Geg Ee G F H epla ErFep A GrHeg rc T re eS oT dom r 2 S FEST FES ea Aran em rece S T reseoT dom r S ran r 2 T leq TEST NADA ieee TS ex fES T fES T A dom f S PES
22. cr cr 1 O e k 0 gt cr l cb l 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 o 0 O crecb 1 e r g A a 1 O ca cr 1 O 0 crecr 1 O k 0 cr 1 cbh 1 State v Goal E et cr lscb 1 37 Here is the result e Y sc 0 O crscb 1 O e ca cr 1 O e crecr 1 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 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 sma
23. eee ee 36 DROP EEDA E SHEE EERE Oe eee eee eee oe ee 36 rrr 37 Tcr 38 TETTE 40 23 3 35 4 24d PS SH NIRE S RSS E BREMEN ME RE 40 TT 40 6 8 The Automatic Post tactid 4 GSA REWile TUIS oss wo x moe So ee co mr WR OX Warte Te de Sod 4 6 8 2 Automaticinferencerules 0 e 4 AE A 50 6 9 Interactive Tactics 50 6 9 1 Interactive Rewrite Rules 50 6 9 2 Interactive Inference rules 56 60 60 SCC EE CBee eee ee ee eee ee ee 61 Ce eeEAG ESSE CREA AG ERED ECAH RES EOE EES Be Le 61 v 61 TT 62 RE mS REMS EUM MN ERBEN B NER REESE RIS RM 63 BO DBracketmbe e oa ce G ox rn Soc Kom Box 4x OE RES Ge4k EEE ES He 63 iii 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 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
24. expr bool E P E bound P bound EL free P free E wff P wff expr eset E M E bound M bound EL free M free E wff M wff expr ident E I E bound Y E free I name E wff TRUE expr atom E expr lit E bound Y E free E wff TRUE 20 expr int E int lit E bound Y E free E wff TRUE pattern Q Q4 Q Q bound Y Q free Q1 free U Q free Q wff TRUE pattern ident Q I Q bound Y Q free I name Q wff TRUE expr list M Ej Eo E M bound Uk k 1 n Ex bound M free Uk k 1 n Ex free Vk k 1 n Ex wff TRUE Vi j 41 l n j l n izj M wff bool Ej bound N E bound Vi j 41 l m j l n izj Ei bound N E free Y 4 3 Type Checking Type checking consists of checking statically that a formula is meaningful in a certain context For that we associate a type with each expression that occurs in a formula This type is the set of all values that the expression can take Then we check that the formula abides by some type checking rules Those rules enforce that the operators used can be meaningful Unfortunately type checking as it is a static check cannot by itself prove that a formula is meaningful For some operators like integer division we will also need to check some additional dynamic constraints e g that the denominator is not zero This will be specified in the well definednes
25. has been created which we need to fill Its name will have to be x if we want it to be a witness for the parameter x Next for the content If we switch between the two machines either by pressing Ctrl F6 or by clicking on their tabs we see that the abstract event has the assignment r x while the concrete one has the assignment r b So x bis the witness Edit the Details and save the file One warning will disappear two to go Try completing the other two witnesses on your own A hint Both witnesses are simple equalities and both can be found by comparing the third guard of the abstract event with the second guard of the concrete one Remember to give the witness the name of the variable it stands for If you completed this step correctly there should be no warning info or error left on the Problems window 2 2 Proving 1 All we have to do now is prove Switch to Proving Perspective Browsing around in the Obligation Explorer Section 5 of the Manual shows you how you can see that the auto prover did quite a good job If you have chosen the witnesses correctly all except for five proofs already should be completed Except for the last one of them all of them could be proved with a different external prover but in order to learn a few new techniques we will prove them with the pO prover Let s start with the proof in Celebrity O Select the proof by clicking on it What you need to prove is that P
26. need sit C aut sit P L and aut P e L 3 Once again the prover automatically rewrites the existential quantifiers in the hypotheses We now look at the proof There is an easy case if sit p outside Solve it 4 For the other case we will need the notion of exit The axioms about exit state that e AXM 3 Every room except the outside has exactly one exit AXM 4 An exit must be a room that communicates with the current one AXM 5 A chain of exits leads to the outside without any cycles or infinite paths AXM 6 Everyone allowed in a room is allowed to go through its exit In our proof we still need to show that anyone who is not outside can walk through a door For this AXM 5 is useless so we add all hypothesis containing exit except for AXM 5 Now we only need to instantiate q and m correctly and concluding the proof should not be too hard For q the choice p is obvious But it is not quite as easy for m Expressed in language m must be the room behind the exit door of the room that p is currently in Try translating this into set theory But do not worry if you get it wrong You can still go back in the proof by righ clicking at the desired point in the proof tree and choosing prune 5 Mathematical proofs By now you should know how to create and edit models and how to do simple proofs with help of the predicate prover In this section we will look at more complex proofs in mathematical settings
27. 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 OG celebrity ctx 1 x 3 CONTEST celebrity ctx 1 EXTENDS celebrity ctx 60 CONSTANTS A AXIOMS axml n 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 xs MACHINE mch 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 it is not repeated here It is also possible to do so in a different way as explained in sections B 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 a
28. parenthesis so formula f A B C should be parsed as f A B C Binary Set Operators This group contains various operators which are more or less compatible each with the other So let s first see how one can safely mix these operators in a formula from a mathematical point of view Table 3 2 on the next page shows operator compatibility We write a cross at the intersection of a row and a column if the two operators are compatible in the following sense operator op is compatible with operator op if and only if the following equality holds A OProw B OPcol C A OProw B OPcol C For instance the cross at the intersection of row two and column three tells us that An B NC An BN and the cross at the intersection of row nine and column seven tells us that A dr amp s A r amp s We can see that the shape is quite irregular and that there are not so many cases where operators are compatible So to have an unambiguous language we should stick to that compatibility relation and forbid any unparenthesized combination of incompatible operators When two operators are compatible we parse them as left associative Otherwise one needs to use parenthesis to resolve ambiguities For instance formula S U T U U is parsed as S UT UU while formula S U T A U is ill formed and is rejected One has to make precise the meaning of that last formula writing either SUT NU or SU T NU There is only one case where we
29. so that you can do the proof yourself 4 If the instantiation succeeded you now should have a new quite lengthy new hypothesis which has the form pl p2 p3 where pl p2 and p3 are predicates This hypothesis will help us to split the proof into three parts First we will prove pl then p2 and last we will derive our goal out of p3 To split the proof click on the red arrow of the implication and choose Apply Modus Ponens using this hypothesis If you now look at the pending subgoals by using the Next Pending Subgoal button in the Proof Control you will see that the proof has been split into the three described parts above 5 We will start off proving the first subgoal f C N x N N t UN x N t First of all we need to translate the statement a bit more towards predicate logic Click on the subset symbol in the goal and choose the first option Remove inclusion in goal As described this translates the inclusion into predicate logic If you look at the proof tree you will see that the prover automatically has done another two steps removing the quantifier and then the implication in the goal 6 Now you will need to completely translate the goal into predicate logic For this click on any red symbol that appears in the proof goal until there is none left Should you have any tilde operators or cross products in the selected hypothesis then it will not hurt to translate them too To do that click on the red
30. somewhat special This operator is indeed as sociative in the algebraic sense However mathematicians often write formula P amp Q amp R when they actually mean P Q A Q gt R Hence we chose to make that operator non associative in the event B language to avoid any ambiguity Finally for the operators that build a predicate from two expressions such as etc the grammar given above doesn t allow formulae like x y z so those operator can not be associative 3 2 3 Priority of operators Another source of ambiguity is the case where formulae contain two different predicate operators without any parenthesis such as P QeR PAQVR P AQ Yr PVQ This kind of ambiguity is generally resolved by defining priorities among operators which define how much binding power each operator has We will use that mechanism here retaining the most commonly used priorities But with the addition that we want to forbid cases where those priorities are not so well accepted For instance some people expect operators A and V to have the same priority while others expect operator to have higher priority So when faced with formula P V Q R some people read it as P V Q R while others read it as P V Q A R which is quite different just replace P and Q by T and R by to convince yourself To solve that ambiguity we decided that operators and V indeed have the same priority but that on
31. the syntactical meaning Getting back to our predicate grammar defined above we see that it is somewhat ambiguous A first point is that it doesn t specify how one should parse formulae containing twice the same binary predicate operator without any parenthesis such as P gt 0Q gt R PAQAR To solve that ambiguity one specifies that each binary operator has a prop erty called associativity The associativities defined for the event B language are the following Associativity gt A V Caution As a consequence formula P gt Q gt R is considered as ill formed and not part of the event B language whereas formula P Q R will be parsed as if it actually were written as P Q R The rationale for these associativities is quite simple Operator is associa tive in the algebraic sense so formulae P Q R and P A QA R have the same meaning Hence one can pick up either left or right associativity for this operator We arbitrarily chose left associativity as it is the most commonly used to our knowledge The same rationale explains the choice of left associativity for operator V On the other hand operator is not associative in the algebraic sense P gt Q gt R is not the same as P gt Q gt R just suppose that predicates P Q and R are all L As a consequence we keep it non associative in the language rather than choosing an arbitrary associativity The case of operator amp is
32. want to allow the combination of two incom patible operators we parse the cartesian product operator as left associative This exception to the above rule is justified by the fact that we want to be consistent with the left associativity we have given to the maplet operator Then one can write a gt b gt c Ax B x C when one actually means am bhecE Ax B xC Interval Constructor This group contains only one operator There is no point in having this operator used twice in the same formula which would give the nonsensical formula a b c So this operator is parsed as non associative 17 UE 56 NO os qose ei UE U x 1 x x x X x O x x x X C9 r X lt x UX x X x Ze lt gt Table 3 2 Compatibility of binary set operators Arithmetic Operators For these operators we choose to retain the Ada language specification for defining priorities and associativity operators and both have the same priority and are parsed as left associative operators x and mod have higher priority and are also parsed as left associative Note that this choice is different from the one made for instance in the C language where there is a special priority for unary We did not retain that last point as it can lead to valid but hard to read expressions like a D which means a b Finally the exponentiation operator has the least priority and i
33. 1 it should be written Ar xy Z rc 1 Ayy Z y 1 The rest of this section formalizes these well formedness conditions using an attribute grammar formalism on the abstract syntax of formulae For that we add three attributes to the nodes of the abstract syntax tree e Attribute bound is synthesized and contains the set of identifiers that occur bound in the formula rooted at the current node e Attribute free is synthesized and contains the set of identifiers that occur free in the formula rooted at the current node e Attribute wff is synthesized and contains a boolean value which is TRUE if and only if the formula rooted at the current node is well formed The value of these three attributes are given by the following set of equations on the production rules of the abstract syntax pred bin P P Pa pred binop P bound P bound U P5 bound P free Pi free U P5 free P wff TRUE P5 wff TRUE P free N P5 bound Y P4 bound 1 P5 free Y PA4 bound N P5 bound Y P wff bool pu Lm pred una P Pi P bound P bound P free P free P wff IT 29 pred quant P L P4 pred quant P bound P bound U L free P free P free Lu free L4 wff TRUE P wff boo P wff TRUE A P boundN L free pred lit P pred lit P bound Pree P wff TRUE pred simp P Ej P bound E bound P free E free P wff E wff pred rel P E E pred relop
34. 3 red orange _w axm4 green orange Dependencies Axioms Theorems Synthesis Pretty Print 2 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 0 does not allow to prove the well definedness of y x 3 The order must be changed to the following axm2 x Z0 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 Navigate Search Project Run Refactor Eve bel a oe d e New Theorems Wizard 13 After pressing that button the following wizard pops up W New Theorems Name and predicate mm Ir 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 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 A
35. ANIZ Project IST 511599 Intormadorcsociey RODIN Rigorous Open Development Environment for Complex Systems RODIN Deliverable 3 6 D30 Public Versions of Basic Tools and Platform Editor Laurent Voisin ETH Zurich Public Document October 29 2007 http rodin cs ncl ac uk Contributors Jean Raymond Abrial ETH Zurich Stefan Hallerstede ETH Zurich Thai Son Hoang ETH Zurich Gabriel Katz ETH Zurich Farhad Mehta ETH Zurich Christophe M tayer ClearSy Francois Terrier ETH Zurich Laurent Voisin ETH Zurich Foreword This deliverable groups together four documents providing support for the users of the RODIN platform 1 User Manual of the RODIN Platform 2 The Event B Modelling Notation 3 The Event B Mathematical Language 4 Tutorials for RODIN All these documents as well as the platform itself are available from the SourceForge web site of the Rodin platform http rodin b sharp sourceforge net User Manual of the RODIN Platform October 2007 Version 2 3 User Manual of the RODIN Platform Contents Project 1 1 1 Project Constituents and Relationships eee l SC EE NUR a ee b dE 2 La Creatino a Ee um amp Oe G wor o RUE we A RON RR S S c9 EES ERE GO eee 3 1 4 RemovingaProject 4 15 EXpOMmine a Project 2 424 052 ee RR Oxo m ROO X 3 eS OW Dom X om oe WORD JR Sede a 4 1 6 Importing a Project
36. BT FESTA ETS 53 fes gt oT fES T A dom f S T fes T fEeS T ran f fESS gt T fes T A dom f S P fes gt T fES T ran f fs O E E V v v Y ee amp 4 Sei gt C D Y Y i ji 7 Y E ER E D C A A E e a V V V V LATINA Sy Ss E Y Y adam me e di T Hom d Ww dw Ww 1 A E m E E 7 n 1 T F Geller Ss ee LC ET wD WwW M M mn E aD EE e e 05 2 6 C SB P DD E amp Pm mm 45 A Ne Non m PRES ag ag TN Sees NT NS ZN NON NN ret Se E r D gi r E t Nah ret Nos U Co ASR ETON OES Noe Na NO Z ss ZN NON 00 p Ne Non ND LL Oc q Ds q D s qes Neer Ne O OO VON E EGE ETS boc c NS SN pNg gt s pUq es riS lUr T r S UT 54 dom pUq dom p U dom q ran pU q ran p U ran q SCT UNT C UNS In the previous rule the type of S and T is P U In the previous rule S and T are sets SCANS SCA J Vends PAGS pog tuper qUr ip aip U r3p n q is alpls sdp q s lt p 4 sdp q s lt p g pi q s p q bs p q gt s p q gt s OS MTY OS UO eT CUSUT LES ATEN T OV S DO qgaspur 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
37. 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 Ev El m Project Explorer XN O celebrity CCS After pressing that button the following wizard pops up New 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 nam 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 indicated below File Edit Navigate Search Project Run Refactor Event B Window Fre Bu Gs x ei th e e el 5 5 De Xo Gr Project Explorer x Cem 2 After pressing that button the following wizard pops up New Enumerated Set
38. D U 001E U 001F 2 2 Identifiers The identifiers of the mathematical language are defined in the same way as in the Unicode standard 4 par 5 15 This definition is not repeated here Basi cally an identifier is a sequence of characters that enjoy some special property like referring to a letter or a digit Some identifiers are reserved for the mathematical language where a prede fined meaning is assigned to them These reserved keywords are the following identifiers made of ASCII letters and digits BOOL FALSE TRUE bool card dom finite id inter max min mod pred prjl prj2 ran Succ union together with those other identifiers that use non ASCII characters Token Code points Token name N U 2115 SET OF NATURAL NUMBERS Ny U 2115 U 0031 SET OF POSITIVE NUMBERS P U 2119 POWERSET Py U 2119 U 0031 SET OF NON EMPTY SUBSETS Z U 2124 SET OF INTEGERS 2 3 Integer Literals Integer literals consists of a non empty sequence of ASCII decimal digits U 0030 U 0031 U 0032 U 0033 U 0034 U 0035 U 0036 U 0037 U 0038 U 0039 Note There are two ways to tokenize integer literals either signed or un signed The first case as the advantage that it corresponds to classical usage in mathematics For instance the string 1 is thought as representing a num ber not a unary minus operator followed by a number But as we use the same character to designate both unary and binary minus this causes prob lems the lexical analy
39. Notation J R Abrial October 2007 Version 1 5 The Event B Modelling Notation Contents D Events D Variant da Actions Witnesses Syntax of the Event B Mathematical Notation Un e 1 Machines and Contexts The primary concept in doing formal developments m Event B is that of a model A model 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 section 2 of a model whereas contexts contain carrier sets constants axioms and theorems of a model Machine Context variables carrier sets invariants constants theorems axioms events theorems Machines and contexts have various relationships 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 An example of machine and context relationship 1s as follows refines extends refines extends The following shows a more formal description of machines and contexts machine lt machine identifier gt refines x lt machine_identi fier gt sees x lt context identifier gt variables lt variable identi fier gt invariants lt label gt lt predicate gt theorems x lt label gt lt predicate gt events lt event gt
40. OR PLUS SIGN MINUS SIGN ASTERISK OPERATOR DIVISION SIGN EXPONENTIATION SIGN 3 Language Syntax This chapter describes the syntax of the mathematical language giving the rationale behind the design decisions made We first present the notation we use to describe the syntax of the mathe matical language Then we present the syntax of predicates and of expressions In each case we first present a simple ambiguous grammar then we tackle with associativity and priorities of operators giving a rationale for each choice made Finally we give a complete and non ambiguous syntax 3 1 Notation In this document we use an Extended Backus Naur Form EBNF to describe syntax In that notation non terminals are surrounded by angle brackets and terminals surrounded by single quotes The other symbols are meta symbols e Symbol defines the non terminal appearing on its left in terms of the syntax on its right e Parenthesis and are used for grouping e A vertical bar denotes alternation e Square brackets and surround an optional part e Curly brackets and surround a part that can be repeated zero or more times 3 2 Predicates The point here is to define a grammar which is quite similar to the one used commonly when writing mathematical formulae but that should also be non ambiguous to the human reader 3 2 1 A first attempt The grammar commonly used for predicates can loosely be defined as follows
41. P S Pla P S P a ta 8 7 05 ityvars a nb A AO ah T B P a ide oo AS P S E ityeqs n E P 5 E P S Pla styvars la On 6 fs e styenv e E E 19 20 B P a 8 P 7 GEN PU P a styeqs ME _ SES B zP y environment is S P S x gt P S Formula r TRUE The type checking dataflow for this formula is given in Figure 4 4 on the following page Assuming that initially z denotes an integer non empty initial typing envi ronment we obtain the following values for attributes atyvars 1 2tyenv atyeqs z gt Z 2o 38 ityvars a yenv x e Z luede Y pred rel equal expr lit Figure 4 4 Type check of formula x TRUE styvars a ene Se oD ityvars a A 5 E caue 6 ityenv rr Z june _7 luede styvars a styvars a z styenv iz Z g Styenv rr Z styegs Z a type BOOL SE age a In the end we obtain a system of two typing equations with one typing variable This system is not satisfiable therefore the formula does not type check remember that we initially assumed that variable x denotes an integer If the initial typing environment would have been empty then the formula would type check 39 5 Dynamic Checking Static checks are not enough to ensure that a formula is meaningful For in stance expression x y passes all the static checks described above nevertheless it is meaning
42. P bound E bound U ba Doud P free E free U Ba free E wff TRUE E 5 wff TRUE Ei free Ex bound Y E bound N E free Y FA bound 1 E gt bound P wff bool P e ident list L I5 In L bound Y L free k k 1 n Ip name L wff bool Vi gj 7E1 nAgel nAt j gt I name I name expr bin E Ej Es lexpr binop E bound EA4 bound U Es bound EL free Ei free U ba free E wff TRUE E5 wff TRUE E free N E5 bound Y E bound N Ea free Y FA bound O Es bound Y E wff bool A ae expr una E Ej expr unopl E bound EA4 bound E free Ei free E wff FA wff expr lambda E Q4 P4 Ej 24 E bound P bound U E4 bound U Q1 free E free P free U E free V Q4 free Q wff TRUE P uff TRUE E wff TRUE P freeQ E1 bound Y P bound N E4 free Y P bound N E4 bound Y P bound N Q4 free Y E bound N Qi free E wff bool gt e E o D E expr quantl E L PD E expr quant E bound P bound U E bound U L free E free P free U FA free Lu free L wff TRUE P wff TRUE E wff TRUE P freeN E4 bound Y P bound N E4 free Y Pi bond O E4 bound P bound N Lu free Y E bound N Lu free E wff bool E AA o e expr quant2 E Ej P expr quant E bound P bound U E bound U Ei free E free P free Ei free P wff TRUE Pi bond N E4 bound P bond Ei free E wff bool
43. a new event might be normal it means that it is not concerned by the variant section This is used quite often when using refinement to add more detail to a specification without considering any liveness property of the system 3 Variant The variant section appears in a refined machine section 1 containing some convergent events section D This machine section contains either a natural number expression which must be decreased by each convergent event or a finite set expression which must be made strictly smaller by each convergent event 4 Actions An action can be deterministic in which case it is made of a list of distinct variable identifiers followed by followed by a list of expressions The latter must be of the same length as the former Variables which do not occur in the list are not modified This is illustrated below lt variable identifier list gt lt expression list gt Here is an example of a deterministic action in an event situated in machine with variables x y and z L Y LTZ Y T Variables x and y are modified as indicated whereas variable z is not modified Alternatively an action can be non deterministic in which case it is made of a list of distinct variable identifiers followed by followed by a before after predicate Variables which do not occur in the list are not modified This is illustrated below lt variable identifier list gt lt before after predicate gt
44. ample we could have an abstract machine on one side of the editing surface and the concrete machine on the other Most of the perspective editing is simply drag and drop First of all you need to find the Fast View Bar Usually it is at the bottom end of the Eclipse window But it also can be on the side or hidden inside the Shortcut Bar For our purposes it probably is best to have it on the right side of the screen Place it there by dragging it with the mouse Now add some items to it To do that press the New Fast View button on the bar It might be useful to leave the Goal the Problems and the Proof Control window at the bottom of the screen as you may want them to stay open while editing A good choice for the Fast view may be e Project Explorer e Obligation Explorer e Search Hypothesis E Quick dilds Radin Platfarm File Ed amp Masque Search Project Run Editor Menu Windies Help ri isi Gr WECKER D si s n oe z T DI Pring Emai Event B y Resource El nva Galois D cowfd G cb GP ccictx 3 Galois BH Se Selected Hypotheses omg EI fen e W d el ten ca N p Ih Bde tet D Bn t fct n e YS CH Ice A Gifs tra EI vo et a xl xet oi viet oi EN Stake Goel en a xl weet Proof Control 22 Problems qgp u me fa a wn de Y FPeODAR Tactic applied successfully Figure 1 Our self made Quick perspective Cache Hypothesis Proof Tree Proof Information Progress Window All
45. and conclude the proofs 3 First of all we take a look at the error It states that an event called celebrity is not refined Double click on the error in the Problem Window to open the Celebrity_1 machine If you look at its events by pressing the Events tab you can see that it actually does have a celebrity event The problem is that it is not declared as a refinement In order to do so right click on the event and select New Refine Event This declares that the event is a refinement of an event with the same name in the abstract machine As this is the case here we can now save the project and the error disappears If the event in the abstract machine had a different name you would have to edit it For more on this issue see Section 3 9 1 of the Manual 4 Next we deal with the warnings The three remaining warnings state that wit nesses are missing In any abstract event that uses parameters if the concrete event has no parameter with the same name the tool needs a witness so that it notices what value the parameter should take Witnesses are also needed for variables that have a nondeterministic assignment in an abstract event and do not appear in the concrete model See also Section 3 9 4 of the Manual To create the wit ness double click on the warning to open the concrete model here Celebrity_2 Then right click on the celebrity event and select New Witness An empty witness
46. 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 AQ PA ALA AQ JL PA AQA ARQA AR L PA AQA AQA AR PA AQA AR Disjunction PV VTV VQ T Pv VLV VQ PV VQ Pv VQV ViQV VR T PV VQV VQV VR PV VQV VR Implication qx gt E Je e T Pat I PL ue PSP 41 Equivalence Negation Quantification Pel P Ter P Pel P LSP P Pep 1 Es dr alo T epp P EZF E F E F EcF OUP Sher EGF EcF a Lb a gt b a aD A O hs ep e dob E FALSE E TRUE E TRUE E FALSE gt FALSE E TRUE E TRUE E FALSE E Vr PA AQ Va P Va Q PV Uoc Peis tI Uu VES ss le sse P 42 Equality Set Theory pode I EXE 1 EsrF GoeH E GAF HA TRUE FALSE l FALSE TRUE L Maris SE 39 UNA emm Sac d flussi ssa ep ame SSMUS Us rer EE EE AU sot TO e UN DAGA E Ses T quc dq Al B C DA oan ee le Do gt Aste N PE Lax PE oon Y D gt S OS Y neg 9 dom ran g Y pe ae dom rrea yreb x y ran x a y 5 b a b 43 PLANE D Ee F E F wh
47. 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 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 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 o
48. by opening the Problems window El Problems 5 Progress Proof Control Properties 11 error O warnings O infos Description 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 xml PEN ze axm3 KEP c eP ze axm4 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 RE 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 tactics Install Update True Goal Discharge G ttee P1 Discharge Run Debug Goal in Hypotheses Discharge B4free PP Discharge sequent 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
49. cktrack from the current node button in the proof control The instantiation for x should now be obvious After the instantiation you get a new hypothesis If you Apply the Modus Ponens on this the smiley in the Proof Control will turn blue This means that all the non reviewed goals have been proven So you will now have to prove the second subgoal Click on Select the next review subgoal to get there The proof of the second subgoal begins similar to the others Remove the inclusion in the goal and simplify the goal as far as possible Next translate the new selected hypotheses into predicate logic by clicking on the e symbols in the selected hypothesis until there is none left There should be one selected hypothesis that starts with a negation Remove the negation in it Now we get a hypothesis beginning with a universal quantifier It should look like this just the variable names might differ Vx0 x z0 te x0c z2 N x N Nt The hypothesis stated above can also be brought into a more easily comprehendible and directly appliable form In the end it should state something like Vx0 10 rct z0c N z2 N z0 z2 t where names may vary Get the hypothesis into the right form yourself using rewrites similar to step 12 Now the instantiation for z0 should be obvious as there is only one variable that maps to x In Figure 3 x1 The rest of the subproof is the same to steps 7 and 8 exce
50. create that pair that is use a maplet operator Set Comprehension There are now two forms of set comprehension The most general one is x P x E x which describes the set whose elements are E x for all x such that P x holds For instance the set of all even natural numbers can be written as x x c N 2 x The second form F P is just a short hand for the first one which allows to write things more compactly The difference from the first form is that the variables that are bound by the construct are not listed explicitly They are inferred from the expression part Continuing with our previous example the set of all even natural numbers can then be written more compactly as 2 a x N which corresponds more to the classical mathematical notation The rule for determining the variables which are bound by this second form is to take all variables that occur free in E Thus if we denote by x the list of the variables that occur free in E then the second form is equivalent to x P E Lambda Abstraction For lambda abstraction classical B 1 uses the form Ax P E where x is a list of variables P a predicate and E an expression This notation is fine when x is reduced to only one variable For instance expression Ax x N x 1 denotes the classical succesor function on natural numbers It is equal by definition to the set x z N x 4 1j But things get more complicated when x represents more t
51. ctor Set of relations constructors Binary set operators Interval constructor Arithmetic operators Relational and functional image Unary relation operator Tightly bound unary operators Predicate conversion Set enumeration and comprehension Given a list of quantified identifiers a predicate and an expression these operators produce a new expression Given two expressions it produces a pair Given two sets these operators pro duce a set of relations Given two sets these operators pro duce a new set Given two integers this operator produces a set Given one or two integers these op erators produce a new integer Given a relation and an expression these operators produce a new ex pression Given a relation this operator pro duces a new relation Given an expression these operators produce another expression Given a predicate this operator pro duces a new boolean expression Given a list of expressions or a list of quantified variables a predicate and an expression this operator pro duces a set Table 3 1 Groups of similar expression operators 15 bounded when one encounters such an operator one can find easily where the expression involving that operator starts and where it ends unary and bool operators are always followed by a formula enclosed within parenthesis set enu merations and comprehensions are enclosed within curly brackets This is a
52. d we obtain a system of two typing equations with three typing variables This system is satisfiable but not uniquely Hence formula Y Y does not type check Formula x C S A c x The type checking dataflow for this formula is given in Figure pred bin land 20 ZA pred rel pred rel 2 subseteq 1 2 subset O expr ident 6 expr ident 10 13 expr int 14 emptyset expr ident 18 UE O O a9 CT oi Figure 4 3 Type check of formula x ES C x Here we assume that variable S denotes a given set Thus our initial typing environment is S P S The attribute values computed by the 37 type checking algorithm are atyvars atyenu atyegs dy 2 styvars 5 6 styenv styeqs type styvars styenv styeqs type atyvars 19 ityenv atyegs styenv 14 styeqs type styvars styenv 17 18 styeqs styvars type In the end we obtain a system of four typing equations with four typing This system is uniquely satisfiable taking a y S and B P S Hence formula x C S C x type checks and the resulting typing variables ityvars a S P S 3 4 nenn S P S Z luede Y ta 8 ityvars La 5 S P S a S 5 P S gt 7 8 ityenv B luede La B styvars La B ls 8 SE w c g ger e B Pa P S 5605 P S Pla La B ityvars La B y FOEDE ityenv eeu zo 19 zr p E ityegs n S
53. d 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 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 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
54. dding 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 md 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 J ES mL Abstract Contexts Select abstract contexts of this context mm m E Dependencies Carrier Sets Constants Axioms Theorems 2 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 following menu New x Delete E Extend Prove in c Go Into Team Compare With Replace With After pressing the Extend button the following wizard pops up iH New EXTENDS Clause Please enter the name of the new context cae You can then enter the name
55. defined in Table 4 1 on the next page expr una E Ej expr unopl Let a and 0 be distinct fresh type variables in FE ityvars E ityvars U la B E ityenv E ityenv E ityeqs E ityeqs E styvars Ej styvars E styenv Ej styenv E styeqs Ey styeqs U E type T where and 7 are defined in Table 4 2 on page 32 expr lambda E Q P Ej Q1 inherited E inherited P inherited Q1 synthesized Ei inherited P synthesized E synthesized Ey synthesized E type P Qi type x E4 type 30 E type Pla x f 8 funimage Es type a Ej type Pla x wn HEI e E type o rel trel srel strel pfun tfun pinj tinj psur tsur tbij P a P a x 6 yp typ Om Cp II II E type P a domres domsub Ez type Pla x 8 E type Pla x B ranres ransub Ez type P 5 Z plus minus mul div mod expn Table 4 1 Typing equations and resulting type for binary expressions 31 TT x B x f Amen Le Table 4 2 Typing equations and resulting type for unary expressions 32 expr quantl E L P Ei expr quant Let a be a fresh type variable in Lj ityvars E ityvars U a L ityenv E ityenv Li ityeqs E ityeqs Pi inherited L synthesized E anherited P synthesized E styvars E styvars E styenv Ej styenv E styeqs E styegs U E type T where and 7 are defined in the following table expr quant2 E Ej P4 expr quant
56. denote the necessary condition for the event to be enabled whereas the actions together represent the way the variables of the corresponding machine are modified Events can have no guards they can be also simple and guarded keyword where or parameterized and guarded keywords any and where When an event lies in a machine which refines another one then the event may specify if any the abstract event s it refines keyword refines When a refining event refines an abstract event which is parameterized one may provide some witnesses keyword with which are presented in section 5 All this is denoted as follows event identifier gt status normal convergent anticipated refines x event identifier gt any x lt parameter identifier gt where x label gt lt predicate gt with x lt label gt lt witness gt then x label gt action gt end Notice that guards witnesses and actions are labelled As said previously such labels must be distinct within a given section Most of the time the status section states that the event is normal A convergent event must be a new event in a refined machine one that does not appear in the abstraction All convergent events in a machine are concerned with the variant section of that machine see section 3 An anticipated event is a new event which is not convergent yet but should become convergent in a subsequent refinement Notice that
57. e cannot mix them together without using paren thesis So PAQV R is considered ill formed One should write either PAQ VR or PA QV R The priorities defined for the event B language are the following from lower to higher priority Vx P and 3x P mixing allowed P gt Qand PSQ mixing not allowed PAQ and PVQ mixing not allowed ei We choose to give quantified predicates the lowest priority in order to ease their reading when embedded in long formulae The main consequence of this choice is that the scope of the variables introduced by a quantifier is the longest sub formula For instance in formula Vx P Q gt R the scope of variable x extends until predicate Q as can be easily seen by looking at matching paren thesis The following formulae show some examples of how those priorities are used to replace parenthesis in some common cases PAQ R isparsedas PAQ gt R Va dy P is parsed as War dy P Vxr P Q is parsed as Vx P Q Vr P Q is parsed as Yz PAQ Vx P is parsed as Vx P Q AQ One should notice the difference with classical B where Vx P Q is parsed as Vx P Q whereas again it is parsed here as Yx P gt Q P Q is parsed as P P AQ is parsed as P 3 2 4 Final syntax for predicates As a result we obtain the following non ambiguous grammar for predicates predicate 4 quantifier unquantified predicate VI ident list F ident list q
58. 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 GQ EQV postponed HP P amp Q G P Set Theory H G E P F Q H P f Ee HIGH F Q H G E F QF H gt G E F Q f G H E QUE E gt Fj G H P f lt g G F Q OV_L 56 H GE dom g Q g G H G e dom g F Q f G OV_R H F Q f 9 G In the four previous rules the lt operator must appear at the top level Hr Q f 5nT nDIS R DIS_R Hr Q f SVT In the two previous rules the occurrence of f must appear at the top level Moreover A and D denote some type Similar left distribution rules exist HE WOK nr QUOD HF Q fKE SIM H In the previous rule the occurrence of f must appear at the top level A similar left simplification rule exists HE WD O g 2 HF Qis fiz Hr Q f g x SIM H In the previous rule the occurrence of f g must appear at the top level A similar left simplification rule exists Finiteness H uel H finite T 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 fnite S V V finite T H F finite S n n T finn R H F finite S IMA H f
59. ent 21 In order to define the variant use the variant wizard as shown below File Edit Navigate Search Project Run Refactor E rz unala lier le w 8 Project Expl 22 Obligation New Variant Wizard c a Pi a x After pressing that button the following wizard will pop up R New Variant Expression va riant aea 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 Navigate Search Cie Els i zx a Pr Save Ex 33 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 28 4 2 Errors The Problems Window When the Static Checker discovers an error in a project a little x X 1s added to this project and to the faulty component in the Project Explorer window as shown in the following screen shot Project Explorer n am D sath eo gt P brp P EP car E celebrity b celebrity ctx O PO celebrity ctx 1 The error itself is shown
60. eorems Creation Wizard SEI a EVE e amp a GAG ee o 3 5 1 Events Creation Wizard 3 52 Direct Editing of Events eee eee eee eines INN Of Pec Geer 2 es a os x o3 8 eae eee ee 2 3 9 eh ee eee eee eee ean beh ee ees e hae ee eee bee ee ae 3 9 Adding more Dependencies 3 9 1 Abstract Event EEN o RR RR OR EO RE RO OR S 2 9 2 putting an Eventi e s uen e ma na ND nes e o Pech a ee 3 9 3 Merging Events x eme ooh om o E 64586560 8 be 45468 SoS 3 9 4 _ Witnesses gt oca OH URUR V X Gh uo E P B IP OR ROW V NER Ee CR ON SOR PV 305 Variant 2 9 Ew Se m EGGS E Sx WB WA P EE a EE 4 Saving a Context or a Machine 4 Automatic Tool Invocations 4 2 Errors The Problems Window 4 3 Preferences for the Auto prover 5 The Proof Obligation Explorer 6 The Proving Perspective Gl Loading PIOOh s sre aa ara terad a pa eaa ae aR E 62 The Proof Vice a o uos os Suede E aa eee eee eRe ee ee ee ee 6 2 1 Description of the Proof Tree ii 17 17 18 18 18 19 19 20 20 20 21 21 21 22 24 24 25 25 25 26 26 26 27 28 28 29 30 3l 62 2 Decoration 0 0 ee ee ee 35 DOR WW E ee ee eee SE 35 02 Midi EEN 36 O25 o ri 2 he bo x39 0909 eee eee
61. erators become unary and take a relation as argument The argument is then their domain The upgrade path from classical B is quite straightforward just replace prj A B by prj 4 x B 3 3 2 A First Attempt An ambiguous grammar for event B expressions can loosely be defined as follows expression expression binary operator expression unary operator expression expression expression expression expression expression X ident pattern predicate expression quantifier ident list predicate expression quantifier expression predicate L ident list predicate expression H lt expression predicate H bool C predicate Y lt P expression list C expression eat d N Ni BOOL TRUE FALSE ident integer literal 13 piss E car ello eno L4 6a IP to 2 6 2 7 ESS mod binary operator gt Lg unary operator card P Py union inter dom ran prjy pij id min max quantifier uem al ident pattern ident pattern gt ident pattern C ident pattern Y ident expression list exp
62. ere F is a single expression S x F 2 F where F isa single expression E F E F where E and F are single expressions Im Goen ll f arg br y Et ee dt PLU gt ale LE gt UT 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 lt type expression and t denotes an expression of type Ty JR UR SJ CDU GT emu S Castle ssh etos VU imm cum 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 rid Y Vir ZU TUE E FUE E E AU UA oem TT ATA VS eti t gt E Pl otc le qe IS me ACS Peas DCS SCA ws ex OCA Av LASER A DE SS ACS X us dS S E Aer uu NAN CB A BCS AC BUS Finiteness Cardinality finite 9 T finite a b T finite S UT finite S finite T finite P S finite S finite S x T S 8 v T g V finite S A finite T finite r finite r finite a b T card Z 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 5 e EE O card S S 8 card S 20 AS 2 eU card 5 E card 0 8 9 OS cardo o Sg card S T as Tr tandis used 45 Arithmetic ta
63. escribed 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 Tim e e 1 0 et cr lt ca ct r A 8 1 cr ca et a 0 ca cr ct r 1 ca cr et a l 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 40 6 8 The Automatic Post tactic In this section we present the various rewrite 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 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
64. han one variable For instance what is the meaning of expression Aa b P E In classical B the latter expression is defined as being the set a b P a bh E This is clearly unsatisfactory for event B as it turns out that in the former expression the comma that appears between a and 6 is not only a separator between two variables but also a hidden pair constructor as one can see when writing the equivalent set comprehension The crux of the matter is that the list of variables x introduced above is much more than a simple list Indeed it describes the structure of the domain of the function defined by the lambda abstraction For instance when one writes in classical B the expression Aa b P E one means that the domain of that function is A x B where A and B are the types of bound variables a and b Hence the use of a comma is not appropriate here as advocated in the paragraph above about Pair Construction The cure is easy just say that x is not a list of variables but a pattern that specifies the structure of the domain of the lambda abstraction The example above is then to be written as Aa b P E Moreover this can be generalized to arbitrary domain structure by allowing arbitrary patterns after the lambda operator The only constraints are that those patterns should be constructed out of distinct variables pair constructors and parenthesis The definition of the lambda abstraction Ax P E becomes X P
65. ication H P x Q XSTL H 2x P x F Q x not free in H and Q H P x ALL R H ve P 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 P x In the last two rules x 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 Id Preferences GER Post Tactic Pr c 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 P Install Update True Goal Discharge B4free ML Discharge b Run Debug False Hypothesis Discharge PP restricted Discharge v Sequent 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 Simp
66. in P and select that hypothesis Then instantiate N and R correctly For instance if you want to instantiate H with c then P c is a good choice for R by typing the instantiations in the Goal Window and then clicking on the red existential quantifier Now all open branches of the proof tree can be proved with pO After this we have completed all the proofs and the model is ready for use 3 Customizing a perspective suitable for RODIN 50 far you needed two different perspectives to work with RODIN But really it is possible to work with only one perspective In this section we try to customize a perspective so that we do not need any other If you have experience with customizing Eclipse perspectives you may only want to read the next paragraph which contains a few thoughts about a good perspective for RODIN As a start we should think about what we want the perspective to look like The proving perspective already is pretty nice We just could use little bit more editing space and the windows of the Event B perspective To create more space we could move all windows that currently are on both sides of the editing area onto one side as they never really need to be used simultaneously For even a bit more space we could dock all of these windows onto the so called Fast View Bar so that they disappear when they are not needed Like that there should be enough space to even work split screen with different components for ex
67. inite S V T H finite S H finite 7 H finite r fin_rel_R 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 fin_rel_img_R 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 SH H finite S H finite f fin fun1 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 ft e SHT H finite 5 i 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 fES T H F finite s H finite f s fin_fun_img_R Ht fe seo 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 gt n lt x H finite S F dn Ve rEeS gt xn H finite S E Animes emo H finite S E lte gt EM In the four previous ru
68. inuing our traversal of the tree we get styvars a B yj styenv ix 8 12 d e D xy 13 14 P Z ityvars La B Y ityenv x GB men i Play M type Z We now reach the second occurrence of variable x and now it is present in the typing environment so we just read its type from there and propagate it styvars La B y styenv ze Jo e SE P a type P 15 16 Reaching operator lt we add two new typing equations and propagate them to the root styvars a 5 7 styenv xr 6 D a 17 18 P Z Pla styeqs 7 7 B Z In the end we obtain a system of four typing equations with two type vari ables This system is uniquely satisfiable by taking a Z and 0 Z Hence the formula type checks Moreover its resulting typing environment is x Z 36 pred rel equal expr lit emptyset expr lit emptyset Figure 4 2 Type check of formula Y Formula o Y The type checking dataflow for this formula is given in Figure 4 2 The attribute values computed by the algorithm are supposing that the initial typing environment is empty ityvars Y ityvars a styvars La Bj styenv Y 1 2tyenv Y 2 ityenv 3 ge ilyegs ityeqgs iB type ityvars a B styvars o B y styvars o B y styenv Y styenv Y 4 ityenv Y 5 6 O ityeqs E gt styeqs U E Di type 7 y a In the en
69. is not empty Enter P in the proof control and open the Search Hypothesis Window Like this you get all hypothesis that have P in them We need to find one that works toward the goal c P does that so add it to the selected hypothesis Section 6 7 of the manual explains how and click on pO in the Proof Control The proof succeeds Next we look at celebrity acti SIM of Celebrity 1 Here we need to prove x c You have no hypothesis about c selected so look for them like you did for hypothesis with P in the last proof This time you can see that c Q is all you need to conclude the proof So add it to the selected hypothesis and the proof will succeed using pO remove 1 inv2 INV is a little more complex In order to prove the statement it suffices to prove x c so type this into the proof control and press the Add Hypothesis button ah Now press pO until it does not get you any further Now try selecting the right hypothesis by yourself in order to complete the proof If you cannot find it you may also just select all hypotheses 5 In order to move to the next proof obligation you may also use the Next Undis charged PO button of the Proof Control The next proof can be solved the same way as the last one You just need to add at least two hypotheses this time 6 In the proof in Celebrity_2 you have to fill in an existential quantifier First look in the list of hypothesis if you find any variable that is
70. is the disjunction of all guards since there is only one guard here it would be Jp l pe L aut sit p L 2 Save the machine You will see that the autoprover fails to prove the theorem DLF THM Let us analyze whether this is an inconsistency in the model In order to succeed with the proof we need a tuple p gt that is in aut but not in sit Searching the hypotheses we find AXM4 of doors_ctx1 which states that there is a room l where everyone is permitted to So for every person p in P pr l and p gt outside is in aut Since these are different at least one of them cannot be in the function sit Now all we would need to prove is that P is nonempty This holds as carrier sets always are nonempty but is a bit hard to derive Add the hypothesis P using the ah button Then click on the Auto Prover button The button with a robot on it Other provers do not work here After successfully adding the hypothesis we can conclude the proof as follows 3 Add AXMA the one with the existential quantifier to the selected hypothesis You see that it automatically is instantiated as l Next click on the of P in the search hypothesis window This creates a selected hypothesis x c P We can now instantiate p in the goal with x 4 In order to instantiate l we need a case distinction Type sit x l this into the proof control and click on Case Distinction dc to look at the two cases sit x l a
71. ities separately for each group defining how operators of each group can be mixed Quantification Operators In this group there is not much room for ambi guity as when we encounter two quantification operators it comes right from their syntax that the second one will be embedded in the first one The only op tion left is whether the second quantified expression should be enclosed within parenthesis or not We decide not to enforce parenthesis in this case As a consequence formula o Z Ayy z yU 0 16 is parsed as Ne z zIQwv z vu 0 Pair Constructor This group contains only the maplet operator so we only have to define an associativity property for that operator Although the maplet operator is not associative in the algebraic sense it is very common usage to parse it as left associative so we shall keep that property Then an expression of the form a gt b gt c will be parsed as a gt b gt c Set of Relations Constructors No operator in this group is associative in the algebraic sense However we decide to parse them as right associative That choice is justified by the fact that we will parse function application as left associative this will be stated when we reach the Relational and functional image paragraph on the following page As a consequence one can write f a b when one actually means f a b Then to be consistent one should also be able to describe properties of function f without
72. les S must not contain any bound variable 59 H F Un Vromes mia H SCZ N H finite S H n Vr zeS gt vn H SCN H finite S Cardinality H a lt b F Q b ad 1 H b lt a Q 0 H Q card a bi H a lt b P a b 1 F Q H b lt a P 0 Q H P card a b F Q In the two previous rules card a b must appear at top level H 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 characters 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 geg inter CEDE B 3 Assignment Operators ESES 61 B 4 Binary Operators Symbol ASCII Symbol ASCII Symbol ASCII 62 B 5 Quantifiers B 6 Bracketing 63 The Event B Modelling
73. less if y is zero The aim of dynamic checking is to detect these kind of meaningless formulas This is done by generating and then proving some well definedness lemma The rest of this chapter specifies how to produce these well definedness lem mas This is done by specifying a WD operator that takes a formula as argument and the result of which is the well definedness lemma of that formula 5 1 Predicate Well Definedness Table on the next page specifies the WD operator for predicates In that table letters P and Q denote arbitrary predicates letters E and F denote expressions and letter L denotes a list of identifiers 5 2 Expression Well Definedness Tables on page and on page specify the WD operator for expres sions In these tables letter P denotes an arbitrary predicate letters E and F denote expressions letter Q denotes a lambda pattern letter L denotes a list of identifiers letter J denotes an identifier letter n denotes a literal integer We also denote by Fg the list of the free variables that appear in expression E that is E free and by Fo the list of the free variables that appear in pattern Q Finally letter x denotes a fresh variable that is a variable that does not occur free in the formula for which we compute the well definedness lemma 40 Table 5 1 WD lemmas for predicates Al WD F WD E AE dom F F LE lt F C id ran F WD E AWD F A F 0 E P E Pi E do
74. lify For all Goal Simplify Implicative Hypotheses with Conjunctive RHS Simplify SEM 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 correspond 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
75. ligation name you are transferred into the Proving Perspective which we are going to describe in subsequent sections 3l 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 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 evt is the event name grd is the guard name Well definedness of an event Action evt act WD COS 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 is the invariant name evt is the event name Invariant Preservation evt inv INV e inv is the invariant name 32 Next are the proof obligations concerned with machine refinements evt is the concrete event name Guard Strengthening evt grd GRD grd is the abstract guard name Guard Strengthening merge evt MRG evt is the concrete event name l t is the concrete event name Action Simulation evt act SIM e act is the abstract action name Equality of a preserved Variable evt v EQL nae SE p v is the preserved variable Nex
76. ll editing area within which you can enter parameters used by some buttons of the Proof Control window the smiley section 6 5 38 e M o O crecs 1 O r 0 a state Y Goal 3 et cr lecs 1 Problems Progress amp Proof Control gt Cache Hypothesis wr por hr de sh se 4B eo FP Ct DIY ED 0 QD O73 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 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 wind
77. lorer window and then right click with the mouse The following contextual menu will appear on the screen New x B S c Go Into Team d Compare With d Restore from Lacal History You simply click on Delete and your project will be 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 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 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 previou
78. lso the case of atomic expressions like integer and boolean literals or identifiers On the other hand the operators of the other groups are not bounded by themselves so one needs to define priorities and associativity laws for them in order to resolve potential ambiguities We will first start by defining priorities between groups then we will refine each group separately 3 3 4 Priority of Operator Groups We arbitrarily choose to define relative priorities such that groups of opera tors are sorted by increasing priority in table on the previous page As a consequence quantification operators have the lowest priority That order has been chosen because it reduces the number of needed paren thesis when writing most common expressions Here are a few example to illustrate this Each expression is stated twice first without parenthesis then fully parenthesized AUB C isparsedas AU B C a b c is parsed as MM a b dua Le r s Also we give the lowest priority to quantification operators so that when embedded in a formula they have to be written surrounded by parenthesis This is consistent with the choice made for quantified predicates An example formula is a b c is parsed as r lUs is parsed as a bUC isparsedas a b U r s is parsed as xx Z c 1 3 22 3 3 5 Associativity of operators Now that priorities of groups have been defined we will resolve remaining ambigu
79. lso gives an introduction on working with the prover After section 1 and 2 the user should have developed a feel of the basic windows of RODIN and when they are needed He might want to combine the two default perspectives into one Section 3 explains how this can be done This section may be omitted by users who feel comfortable switching between two perspectives Section 4 shows how to use apply reasoning on models in the prover Section 5 shows a proof in a mathematical setting and then provides a few examples on which the user can work on by himself In these proofs everything except the basic rewrite rules has to be done by the user Files For this tutorial you will be needing 4 example files They are e Celebrity zip which will be needed in section 2 e Doors zip which contains the model that is used in section 4 e Closure zip This is the model on which you perform proofs in section 5 e Galois zip This model is not really needed but serves as an explanation to why the proof in section 5 works 1 A First Example The Birthday Book To begin with let us start with a simple model of a birthday book similar to the one in the Z Notation Reference Manual This little book is a simple tool that can be used to keep birthdays of different people All we can do with it is writing people s birthdays into it So the initial model only has one event We create the model as follows 1 1 The Event B Perspective 1
80. m F ran E prj E prja id E union E Table 5 2 WD lemmas for binary and unary expressions 42 AQ P E VFo WD P A P gt WD E VL WD P A P WD E VFE WD P A P gt WD E AGE SITT WOO te Z Ni BOOL TRUE FALSE e n Table 5 3 WD lemmas for other expressions 43 Bibliography 1 Abrial J R 1996 The B Book Assigning Programs to Meanings Cam bridge University Press 2 LLL Abrial J R and Mussat L 2002 On Using Conditional Definitions in Formal Theories In D Bert et al Eds ZB2002 Formal Specification and Development in Z and B LNCS 2272 pp 242 269 Springer Verlag 3 Burdy L 2000 Traitement des expressions d pourvues de sens de la th orie des ensembles Application la m thode B Th se de doctorat Con servatoire National des Arts et M tiers 4 The Unicode Consortium 2003 The Unicode Standard 4 0 Addison Wesley 44 Tutorials for RODIN October 26 2007 Introduction This tutorial should provide the user with a tour through the most important functional ities of RODIN so that he gets a understanding of how the program works The tutorial is divided into 5 sections In the first section a very simple project is created from scratch The essential steps in working with components are illustrated here The second section provides an example that shows how events of different machines can be connected together It a
81. mic check Revision History Date Contents 2005 05 31 Initial revision Rodin Deliverable D7 2006 05 24 Added min and max unary operators 2007 10 26 Minor corrections in the text 2 Language Lexicon This chapter describes the lexicon of the mathematical language that is the way that terminal tokens of the language grammar are built from a stream of characters Here we assume that the input stream is made of Unicode characters as defined in the Unicode standard 4 0 4 As we use only characters of the Basic Multilingual Plane all characters are designated by their code points that is an uppercase letter U followed by a plus sign and an integer value made of four hexadecimal digits For instance the classical space character is designated by U 0020 Each token is formed by considering the longest sequence of characters that matches one of the definition below 2 1 Whitespace Whitespace characters are used to separate tokens or to improve the legibility of the formula They are otherwise ignored during lexical analysis The whitespace characters of the mathematical language are the Unicode 4 0 space characters U 0020 U 00A0 U 1680 U 180E U 2000 U 2001 U 2002 U 2003 U 2004 U 2005 U 2006 U 2007 U 2008 U 2009 U 200A U 200B U 2028 U 2029 U 202F U 205F U4 3000 together with the following control characters these are the same as in the Java Language U 0009 U 000A U 000B U 000C U 000D U 001C U 001
82. n person So our event needs an additional guard that restricts p to people for whom there is no entry yet in the book This can be done in the proving perspective Just switch to the machine and add the additional guard p d dom birthday using the editor On adding guards Manual section 3 5 2 If you save the document now you will see that the auto prover can conclude Congratulations You have built your first model with RODIN 2 The Celebrity Problem The next model that you will work with is the so called celebrity problem In the setting for this problem we have a knows relation This relation is defined so that no one knows himself the celebrity knows nobody but everybody knows the celebrity The goal is to find the celebrity The provided development once completed yields a linear time algorithm for the problem 2 1 Modeling 1 Make sure that you have no existing Project named Celebrity If you do then re name it Section 1 7 in the Manual Then import the archive file Celebrity zip For this choose Import in the File menu and then select Existing Projects into Workspace Then select the according archive file Read more on importing projects in section 1 6 of the Manual 2 The tool takes a few seconds to extract and load all the files Once it is done it shows that there are a few problems with this project In the first part of this section our goal is to fix these problems
83. nd 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 e ale e F rier Eeploren UE E O celd New Variable Wizard After pressing that button the following wizard pops up Run Refactor Event B New Vaniable Identifier EE Initialisation 4 45 Ivar Invariant linv2 var c 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 variables press the Add button When you re finished press the OK button 3 2 2
84. nd sit x l Before starting with the cases the prover now wants you to prove that x dom sit This can be done with pO as sit is a total function In the first case x is situated in l so it cannot be in outside So you can instantiate l with outside In order to prove that x is allowed to outside you will need to select the hypothesis P x outside C aut Then you can finish this case with p0 If you look at the proof tree you see that you now have reached the other branch of the case distinction In this case you can simply instantiate with l as x is not situated there Finally click on pO to finish the proof 4 2 First Refinement Now we get to the a bit harder proof The deadlock freeness proof for the first refinement There is not much that has changed The constant com has been added in order to describe which rooms are connected Additionally we have a constant exit which will be explained later 1 Open door 1 and add a theorem called DLF stating dq m q m aut sit q gt m com to it then save the file Once again the prover fails to prove deadlock freeness automatically 2 At the beginning of the proof there are no selected hypothesis at all So we need to select a few The old deadlock freeness theorem will be useful AXM7 of doors ctx2 too To begin with we try to avoid using exit as we want to keep things as simple as possible But since s t and aut are inside the theorem we also are likely to
85. ne 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 n New Local Variable a 4 New Guard a grd2 a New Action 4 act New Refine Event e New Witness P 3 rmv 2 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 rmv 1 o x 2 gradil xER D grd xb bek 4 act11 R R Xx 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 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 refinem
86. ng button as shown below B mel x amp Bd Create new component celebrity gt Cire 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 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 3 Context med 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 o 3 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 context 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
87. nherited pred simp P Ei Let a be a fresh type variable in FE ityvars P ityvars U a E ityenv Pityenv E ityeqs P ityeqs P styvars Ej styvars P styenv E styenv P styeqs E4 styeqs U ET type P a pred rel P E E pred relop Let a be a fresh type variable in E ityvars P ityvars U a Ey ityenv Pityenv E ityeqs P ityeqs Es inherited E synthesized P styvars E2 styvars P styenv E styenv P styeqs E styeqs U where is defined in the following table E type 0 equal notequal E type a EA4 type Z It le gt 8e Es type Z bi Dune a In notin E type P a subset notsubset E type P a subseteq notsubseteq E type P a ident list L J LB In I inherited L inherited L inherited I synthesized I inherited I _1 synthesized L synthesized I synthesized 29 ident I name if I name dom I ityenv then I synthesized I inherited I type I ityenv I name else let o be a fresh type variable in I styvars I ityvars U a I styenv I ityenv U I name a I styeqs ityeqs I type a expr bin E Ej Es lexpr binop Let a D y and be distinct fresh type variables in FE ityvars E ityvars U Ja 6 y 6 EA4 ityenv E ityenv E ityeqs E ityeqs E inherited Ey synthesized E styvars E 5 styvars E styenv E2 styenv E styeqs Eo styeqs U E type T where and 7 are
88. nt list predicate expression LJ expression predicate PY ident list predicate expression TV expression predicate pair expression ident pattern 4 gt ident pattern C ident pattern ident relation set expr gt relation set expr set expr relational set op set expr DIR See les 9 gt o interval expr U interval expr interval expr x interval expr interval expr lt 4 interval expr m PS em em interval expr oi interval expr interval expr interval expr domain modifier relation expr interval expr lt lt interval expr interval expr interval expr interval expr range modifier interval expr N interval expr A interval expr range modifier D gt interval expr arithmetic expr arithmetic expr term CE term y factor 4 x mod factor 7NI image image primary expression expression simple expr P 19 simple expr unary op bool C predicate Y unary op C expression C expression Y T ident list predicate expression Y expression predicate
89. nus converse card pow powl union inter dom ran prjl prj2 id min max expr quant qunion qinter cset expr lit integer natural naturall bool true false emptyset int lit is an integer number expr binop expr unop l 4 2 Well formedness Each occurrence of an identifier in a formula that is a predicate or an expres sion can be either free or bound Intuitively a free occurrence of an identifier refers to a declaration of that identifier in a scope outside of the formula while a bound occurrence corresponds to a local declaration introduced by a quantifier in the formula itself For a formula to be considered well formed we ask that beyond being syn tactically correct it also satisfies the two following conditions 1 Any identifier that occurs in the formula should have only free occurrences or bound occurrences but not both 22 2 Any identifier that occurs bound in the formula should be bound in ex actly one place i e by only one quantifier These conditions have been coined so that any occurrence of an identifier in a formula always denotes exactly the same data This is a big win in formula legibility For instance the following formula is ill formed it doesn t satisfy the first condition Ave e ely a a it should be written Agee Lys a ee N And the following formula is also ill formed failing to satisfy the second condition AxxeZlat 1 Ar xe Z x
90. o the first proof obligation indicates that it already has been proved and the red icon next to the second proof obligation tells that the proof is not yet completed Proof obligations can have three colors red green and blue The blue color means that the proof has been reviewed meaning that it has been discharged without proof by the user Click on the second prove obligation to display the proof This fills a couple of other windows e The Proof Tree Section 6 2 of the Manual Here you see a tree of the proof that you have done so far and your current position in it By clicking in the tree you can navigate inside the proof Currently you have not started with the proof yet so there is no new place to move to e The Proof Control Manual section 6 4 This is where you perform interactive proofs e The Selected Hypothesis window Manual section 6 7 The hypothesis that are currently being used for the proof are displayed here You can add hypothesis into it from the Search Hypothesis window and from the Cached Hypothesis window See section 6 4 in the Manual on how to open these windows e The goal window Manual section 6 3 This window shows what needs to be proved at the current position inside the proof tree Currently we need to show that birthday is still a partial function from PERSON to DATE if it is extended by an entry There is no way to prove the goal if a birthday is already entered into the book for a certai
91. o the set of all possible types For instance the typing environment a gt Z b 5 P Z x BOOL c 5 a says that identifier a has type Z identifier b has type P Z x BOOL De is a relation between integers and booleans and identifier c is typed by type variable a If an identifier has been defined as a carrier set then it will appear in the typing environment as the pair i gt P 2 A typing equation is a pair of types In the sequel we will write typing equations as T1 o instead of the more classical pair 7 T This is mere syntactical sugar to enhance legibility A typing equation is said to be satisfiable if and only if there exists an assignment to the type variables it contains such that when replacing these type variables by their value the two components of the pair are equal i e denote the same type For instance typing equation a x BOOL Z x f is satisfiable take Z for a and BOOL for 5 In contrast type equation Pla Z and Z S are unsatisfiable in the last sentence remember that S denotes a carrier set Similarly a typing equation is said to be uniquely satisfiable if and only if there exists a unique assignment of type variables that satisfies it For instance a Z is uniquely satisfiable the only assignment that satisfies it is to take Z for a while the type equation a 0 although satisfiable is not uniquely satisfiable to satisfy it we only need that o
92. of the windows that you cannot create directly when clicking on the New Fast View Bar can be found in Others General Once you are done the window should look like in Figure Click on Save Perspective As in the Window menu to save the perspective 4 Location Access Controller In this section we will take a closer look at a few more complex proofs For this we will use the model of the Location Access Controller which is saved in the doors zip project archive Explanations on the model can be found in the chapter entitled Location Access Controller of the Event B book Our task is to develop the proofs for deadlock freeness of the initial model and of the first refinement Import doors zip Looking through it you will see that everything already has been proved This is true however RODIN does not do any deadlock freeness proof yet so you will have to add them yourself 4 1 Initial Model First let us look at the initial model constisting of doors_ctx1 and doors 0 There are two carrier sets in the model one for people and one for locations Then there is a location called outside and a relation aut which reflects where people are allowed to go Everyone is allowed to outside The model only has one event which changes the location of a person So proof of deadlock freeness means proving that someone can always change room 1 Add a new theorem to doors O called DLF and change the predicate so that it
93. orems 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 d Geb Er e gt Project Explorer 3 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 D 5 D celebrity 4 Si D Theorems E Name Predicates Add Delete H thm B thm3 Down Dependencies Variables Invariants Theorems Events 5 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 D Ce File Edit Navigate Search Project Run Refactor Event RB Winc e E dad oa mir ICH 4 amp Project Explorer 33 O celebrity 3 New Event Wizard Ts 21 After pressing
94. otheses The second part of the proof can be solved by removing the C in t f C t and then instantiating correctly For the time being we do not yet want to prove the second subgoal but proceed with the last one 5o review this subgoal by pressing the blue button in the proof control The prover automatically skips to the next subgoal The proof of the third subgoal will only require the hypothesis t C N x N t CN x N N So you can remove all the others Remove the inclusion in the hypothesis and in the goal in order to transform them towards predicate calculus Then click on the E of the hypothesis x z0 t t in order to introduce 71 11 11 12 13 14 15 16 You can now instantiate x with zl and x0 with x0 in the hypothesis with the quantifiers as is done in the proof of the theorem in the Galois project After translating the hypothesis into predicate logic by pressing all E you get a rule that states Jx xl x Et Azm z0 E N x N t Click on the to get a hypothesis with a universal quantifier Now you will want to get this hypothesis into a better appliable form By using rewrites clicking on the red symbols you should be able to transform it into Vr rl EtAxENAzTzl E N x 20 t Try to get the hypothesis into the right form yourself Should you completely mess something up you can still go a few steps back in the proof tree by clicking on the Ba
95. ouse yields the following contextual menu New X Delete Rename E Refine Prove fer S SH c 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 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 ks INITIALISATION b x find remove Copy x E Paste a grdl e New Event s grd2 New Local Variable 4 New Guard D y New Action act1l e New Refine Event P rmv 2 e New Witness 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 3x INITIALISATION b x find 4 remove 1 rmv 1 o x B grdl xeR D grd xbbek D y y b actll R R x Ps rmv 2 3 9 2 Splitting an Event An abstract event can
96. ow 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 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 1s d
97. 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 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 X Search auto rewrite sz H goal frees r0 c v gt goal v amp ovr in roomke r e snd c r0 v eh rO r vw ah c c T goal ML v eh c c 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 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 decorate
98. pt for the variable names So you can either repeat these steps or try to copy the proof To copy the proof right click on the part that you need on the proof tree where you added the hypothesis and choose copy Then right click on your current location and select paste By all chance the proof did not work due to the different names Look in the proof tree for where the wrong name has been used and prune that part You will have to redo that bit of the proof again 5 2 Exercise Theorem 2 In Theorem 2 you have to prove that t f union t f For this you have to prove both directions t C f U t f and f U t f f Start with the second part as it is much 12 Quick edletx Rodin Platform File Bde WAlinigete Search Project Bun Fdeor Mero Window Help ri ll Gr amp 9 jd Ea He TY EI Proving E Quick E Event 8 jS Resource DI Java Galois iD crwfd G ccietx 13 D ccictx A Galois 4 er Selected Hypotheses d eg 3 Y v sl e fcs a GITES trs E EI xl xet E b a len Di yeh Dr r x2 e Set E r4 Zeh a XZEN e xo x i SU KET A XDEH a xzeh EQ x2et Sabe Fi Goal El v D xl xoet Proof Control I3 Problemas qm d m e om oe ab ze e We re gag A e Tactic applied paccesifulle Figure 3 The proof at step 15 easier The first part also should not be too hard if you instantiate the hypothesis with the quantifier as early as possible 5 3 Exercise Theorem 3
99. receive a value in the concrete event Such values are called the witnesses Each witness is labelled with the concerned abstract parameter The witness is defined by a predicate involving the abstract parameter Most of the time this predicate is a simple equality Next is an example showing two witnesses On the left hand side we have an abstract event named pass with two parameters On the right hand side we have a concrete event named new pass refining pass new_pass refines pass any d where grdl d ran dap p l aut with sit p gt l com p p dap d Le Le dsttd sit p l then actl sit dap d dst d act2 dap dap gt d end When the concrete event is also parameterized then an abstract parameter which is the same as a con crete need not be given an explicit witness it is always the corresponding concrete parameter 6 Syntax of the Event B Mathematical Notation It is defined in a separate document entitled The Event B Mathematical Notation The Event B Mathematical Language Christophe M tayer ClearSy Laurent Voisin ETH Zurich October 26 2007 Contents 1 Introduction 2 Language Lexicon TIA 22 SS ai be eee e e BG OR ee M OE Re ee Ow WD S ora oras ss TI PEE 3 Language Syntax 3 1 NO LION Xo Xe XR XS SERRE RSG 3 2 Predicates 22222 cr Rn rn 3 2 1 hrsbattempt 4 6 xo eoo Ae Rm RR EORR 3 2 2 Associativity of operators 3 2
100. ression list expression expression As can be seen there are many expression operators in the event B language So we ll need to take a divide and conquer approach to make things easier to grasp we will first try to group all those operators into some categories 3 3 3 Operator Groups Basically there are several kinds of expressions The most important ones are shown in Figure 3 1 This figure reads as follows there are three top level kinds of expressions sets pairs and scalars Relations and sets of relations are some special kinds of set For instance a relation between a set A and a set B is a subset of A x B The set of all relations between A and B is the set of all subsets of A x B Integers and booleans are also some special kind of scalar expression expression scalar relation set of relations Figure 3 1 Kinds of expressions We now define groups of similar expression operators see Table on the following page The groups are defined by considering the shape of the operator binary unary quantified etc but also the kind of operator arguments and result For each group we will give one operator which will be used in the sequel as a distinguished representative of its group When examining that table we can remark an interesting point the oper ators that belong to the last three groups have the special property of being 14 Quantification operators Pair constru
101. ripted to denote formulae a P denotes a predicate E an expression L a list of identifiers I an identifier M a list of expressions and Q a pattern for lambda abstraction The production rules for predicates are pred bin P P P gt pred binop pred una P Pi pred quant P L P4 pred quant pred lit P pred lit pred simp P Ej pred rel P Ej E pred relop where pred binop land lor limp leqv pred quant forall exists pred lit btrue bfalse equal notequal It le gt ge DECIDE l in notin subset notsubset subseteq notsubseteq 21 The production rules for lists of identifiers and identifiers are ident list L li La In ident Z name where Ji name is a string of characters The production rules for expressions are expr bin E Ej E expr binop expr una E Ej expr unop expr lambda E Q4 P1 Ej expr quantl E L Py E expr quant expr quant2 E Ej P expr quant expr bool E P expr eset E amp E Mj expr ident E 1 expr atom E expr lit expr int E int lit pattern Q Q Qo pattern ident Q J expr list M Ej Eo Ej where funimage relimage mapsto rel trel srel strel pfun tfun pinj tinj psur tsur tbij bunion binter setminus cprod dprod pprod bcomp fcomp ovl domres domsub ranres ransub upto plus minus mul div mod expn umi
102. s dynamic checks see chapter 5 on page 40 The result of type checking is twofold Firstly it says whether a given formula is well typed that is abides by the type checking rules Secondly it computes an enriched context that associates a type with every identifier occurring free in the formula In the sequel of this section we shall first specify more formally concepts such as type type variable typing environment and typing equation Then we shall specify type checking using an attribute grammar formalism as was done for well formedness Finally we give some illustrating examples of type checking 4 3 1 Typing Concepts As said previously a type denotes the set of values that an expression can take Moreover we want this set to be derived statically based on the form of the 26 expression and the context in which it appears As a consequence a type can take one of the three following forms e a basic set that is a predefined set Z or BOOL or a carrier set provided by the user i e an identifier e a power set of another type such as P Z e a cartesian product of two types such as Z x BOOL A type variable is a meta variable that can denote any type In the sequel we shall use lowercase Greek letters a B y to denote type variables A typing environment represents the context in which a formula is to be type checked A typing environment is a partial function from the set of all identifiers t
103. s of the type checking algorithm in action on various formulae Formula 1eZ Al1 lt z Figure 4 1 shows the dataflow for the type checking of this formula Each step of the type checking algorithm is shown as a circled number with edges relating them The numbers appearing on the left of a node corresponds to the computation of inherited attributes numbers on the right to the computation of synthesized attributes pred bin land 18 pred rel Ee pred rel 17 ES JAN a expr ident 6 e expr lit 8 BD expr int e 3 expr ident 16 integer 1 UE Ober Figure 4 1 Type check of formula x Z 1 lt x Assuming that the typing environment is initially empty the initial compu tation at step 1 is ityvars Y 1 2tyenv Y ityeqs Y 39 Then we process down the tree adding a type variable at the operator ityvars Y ityvars a 2 ityenv Y 3 4 w yenv Y luede Y ityeqs Y Examining the first occurrence of variable x we find that it is not present in the environment so we create a new type variable for it This is then propagated in the tree siyvars 0 9 ityvars 0 0 EE 5 6 FER 7 ityenu rr Bb 8 no 7 ityegs i type D v type P Z We now reach the operator again where we add our first type equations and propagate the attribute values styvars o 3 ityvars La B y EE e eg styeqs o D ityeqs en P Z P a P Z P a Cont
104. s parsed as non associative Relational and Functional Image We choose to make these operations left associative although they are not associative in the algebraic sense This follows common usage and is indeed important to have easy to read formulas If these operators were not associative one would have to write quite intricate formulas just to express successive function application f a b c With the left associativity we ve added this becomes f a b c Unary Relation Operator This group contains only one operator 7t which can be repeated obviously so that r is parsed as r 1 3 3 6 Final syntax for expressions As a result we obtain the following non ambiguous grammar for expressions An important point is that non terminals are named after the group of the top level operators appearing in their production rule This can be somewhat misleading as for instance pair expression can be derived as formula Z which is clearly not a pair This naming policy was chosen not to leave any information just 18 numbering non terminals 1 2 would miss some structural property of the grammar expression ident pattern pair expression relation set expr relational set op set expr domain modifier relation expr range modifier interval expr arithmetic expr term factor image primary AT ident pattern predicate expression LJ Gde
105. s 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 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 correspondi
106. sis is no longer context free but depends on the syntax of the language There are basically two solutions to this problem One taken in some func tional languages in the ML family and in the Z notation is to use different characters to represent the unary and binary minus operator However this comes against mathematical tradition and is thus rejected The second solution is to consider that integer literals are unsigned This second solution has been chosen here 2 4 Predicate symbols The tokens used in the pure predicate calculus are Token Code point Token name U 0028 LEFT PARENTHESIS U 0029 RIGHT PARENTHESIS e U 21D4 LOGICAL EQUIVALENCE gt U 21D2 LOGICAL IMPLICATION A U 2227 LOGICAL AND V U 2228 LOGICAL OR U 00AC NOT SIGN En U 22A4 TRUE PREDICATE L U 22A5 FALSE PREDICATE V U 2200 FOR ALL U 2203 THERE EXISTS U 002C COMMA U 00B7 MIDDLE DOT The symbolic tokens used to build predicates from expressions are Token Code point Token name U 003D EQUALS SIGN S U 2260 NOT EQUAL TO lt U 003C LESS THAN SIGN lt U 2264 LESS THAN OR EQUAL TO gt U 003E GREATER THAN SIGN gt U 2265 GREATER THAN OR EQUAL TO U 2208 ELEMENT OF d U 2209 NOT AN ELEMENT OF C U 2282 SUBSET OF g U 2284 NOT A SUBSET OF C U 2286 SUBSET OF OR EQUAL TO Z U 2288 NEITHER A SUBSET OF NOR EQUAL TO 2 5 Expression symbols The following symbolic tokens are used to build sets of relations or functions Token EECHER Code poin
107. t U 2194 U E100 U E101 U E102 U 21F8 U 2192 U 2914 U 21A3 U 2900 U 21A0 U 2916 Token name RELATION TOTAL RELATION SURJECTIVE RELATION TOTAL SURJECTIVE RELATION PARTIAL FUNCTION TOTAL FUNCTION PARTIAL INJECTION TOTAL INJECTION PARTIAL SURJECTION TOTAL SURJECTION BIJECTION The following symbolic tokens are used for manipulating sets Token xXx CDA Code point U 007B U 007D U 21A6 U 2205 U 2229 U 222A U 2216 U 00D7 Token name LEFT CURLY BRACKET RIGHT CURLY BRACKET MAPLET EMPTY SET INTERSECTION UNION SET MINUS CARTESIAN PRODUCT The following symbolic tokens are used for manipulating relations and func tions Token r s 1 VV Code point U 005B U 005D U 21A6 U E103 U 2218 U 003B U 2297 U 2225 U 223C U 25C1 U 2A64 U 25B7 U 2A65 Token name LEFT SQUARE BRACKET RIGHT SQUARE BRACKET MAPLET RELATION OVERRIDING BACKWARD COMPOSITION FORWARD COMPOSITION DIRECT PRODUCT PARALLEL PRODUCT TILDE OPERATOR DOMAIN RESTRICTION DOMAIN SUBTRACTION RANGE RESTRICTION RANGE SUBTRACTION The following symbolic tokens are used in quantified expressions Token Code point A U 03BB U 22C2 U U 22C3 U 2223 Token name LAMBDA N ARY INTERSECTION N ARY UNION SUCH THAT The following symbolic tokens are used in arithmetic expressions Token Code point i U 2025 U 002B U 2212 U 2217 U 00F7 U 005E Token name UPTO OPERAT
108. t 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 eut 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 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 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 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 in the Proof Tree window As we shall see in section 6 2 each node of the
109. 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 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 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 Y v O O cr lt cb 1 O e r 0 O e a 1 O e ca cr 1 O e
110. that button the following wizard pops up Mew Events Parameter identifier s am 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 it and then press button Up or Down 22 O celebrity 3 Qcelebrty 2 h Events var grd Elements Contents Add Event bk INITIALISATION Add Var P x find Add Guard Im WEN rmv 2 Add Action Up ap 22 7 Dependencies Variables Invariants Theorems Events i 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 celebrity 3 celebrity O Events Elements Cantents Add
111. tisfiable Moreover in case of success the resulting typing environment is R styenv where all type variables have been replaced by the values that satisfy the latter set of typing equations Initialization of the attribute grammar consists of the following three equa tions where R denotes the root of the treo R ityvars Y R ityenv initial typing environment R ityegs Please note that the initial typing environment must not contain any type variable The rest of this section describes the equations for each production rule of the attribute grammar In some places we use a shortcut to denote some set of equations The notation A inherited B synthesized means A ityvars B styvars A ityenv B styenv A ityeqs B styeqs We also use the term fresh type variable to denote a type variable which doesn t occur in attribute tyvars of the left hand side of a production rule For instance in the equations of production rule pred rel denotes a type variable such that a P ityvars The set of equations of the attribute grammar is pred bin P P Pa pred binop P inherited P inherited P5 inherited P synthesized P synthesized P synthesized pred una P P P anherited P inherited P synthesized P synthesized 28 pred quant P L P pred quant L inherited P inherited P anherited L synthesized P synthesized P synthesized pred lit P pred lit P synthesized P i
112. uantifier ident list ident 1 ident y 6 simple predicate simple predicate unquantified predicate simple predicate gt simple predicate lt A literal predicate V literal predicate simple predicate literal predicate 4 literal predicate literal predicate atomic predicate 10 ES FTT finite C expression pair expression relop pair expression C predicate atomic predicate relop Ke 3 Be G Sl E A ue Ne Please note that for relational predicates we are using jpair expressionj instead of expression That change will only allow expressions without quan tifiers on each side of the relational operator As a consequence when one wants to use a quantified expression on either side one will have to surround it with parenthesis For instance predicate Ax z Z x id Z is not well formed one must write instead Ax x Z x id Z 3 3 Expressions The design principle for the syntax of expressions is the same as that of pred icates namely to enhance readability To fulfill this goal we use the same techniques minimize the need for parenthesis where they are not really needed and prevent mixing operators when such a mix would be ambiguous 3 3 1 Some Fine Points Before presenting a first attempt of the syntax of expressions we shall stud
113. ve 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 9 celebrity ctxl x Constants Mame Add o red Delete o green P o orange o Dit o pit Carrier Sets Constants Axioms Theorems o 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 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 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 12 C celebrity ctx1 X Axioms Name Predicates Add axml COLOR red greel Delete axm2Z red green axm
114. x gt E where X is the list of the variables that occur in x 12 Other Quantified Expressions The other quantified expressions are the quantified union and intersection In this paragraph we shall only consider quantified intersection but everything will also apply to quantified union mu tatis mutandis A quantified intersection expression has the form lr P E where x is a list of variables P a predicate and E an expression It s defined as being a short form for the equivalent expression inter x P EI which mixes generalized intersection and set comprehension But as we have seen above we also have a short form for writing set comprehension The question then arises whether we could also define a short form for generalized intersection The answer is yes We then have a second form which is E P and which is defined has being equal to inter 1E PY Projections In classical B 1 the first and second projection operators take two sets as arguments like for instance in the expression prj A B In that expression arguments A and B are used for two different purposes On the one end they allow to infer the type associated to the instantiated operator On the other hand they define the domain of the instantiated operator which is A x B This approach seems unnecessarily restrictive as it puts a strong constraint on the domain of the operator namely that it must be a cartesian product So in event B these op
115. y some fine points about pairs set comprehension lambda abstraction quantified expressions and first and second projections Pair Construction Pairs of expressions are constructed using the maplet operator Contrary to classical B 1 it is not possible to use a comma anymore This change is due to the ambiguity of using commas for two different purposes in classical B as a pair constructor and as a separator For instance set 1 2 can be seen as either a set containing the pair 1 2 or as a set containing the two elements 1 and 2 That was very confusing In event B a comma is always a separator and a maplet is a pair constructor Below are some examples showing the consequences of this new approach Classical B Event B r yco reyes CA RL Trey zrt f z y fx y The last example is particularly blatant of the confusion between separator and pair constructor in classical B When looking at formula f x y one has the impression that function f takes two separate arguments But this is not always true For instance variable x could hide a non scalar value For instance 11 suppose that x a b then the function application could be rewritten as either f a b y or even as f a b y In that latter case function f now appears to take three arguments This is clearly not satisfactory In fact function f only takes one argument which can happen to be a pair In that latter case one should use a pair constructor to
116. y in the birthday book but not every person has an entry in it birthday should be a partial function from PERSON to DATE At initialization we want the book to be empty The symbol for partial functions can be written by typing in gt Section 8 of the Manual contains all on how to write Event B symbols in ASCII The Z Notation Reference Manual can be found at http spivey oriel ox ac uk mike zrm index html 7 Last we create the event Open the New Event Wizard as seen in Section 3 5 1 of the Manual on the top tool bar Name the new Event AddBirthday It has two parameters p and d where p is a PERSON and d is a DATE enter these as guards As action write birthday birthday U p gt d Remember Section 8 of the manual explains how to write Event B symbols Now save the machine If you have done everything correctly the type checker should not return anything to the problems window at the bottom of the screen It appears that we have successfully created a model of the birthday book But have we 1 2 The Proving Perspective Now we switch to the proving perspective You see several windows on the screen e The Proof Obligation Explorer Section 5 of the Manual Here you can browse through proof obligations As you can see BirthdayBook CO has no proof obliga tion and BirthdayBook_0 has two The A in the icons of the obligations means that the automatic prover attempted both obligations The green icon next t

RODIN Deliverable D30

Contents

Download Pdf Manuals

Related Search

Related Contents