Home

User Manual for Rodin v.2.3 - Rodin Handbook - Event

1. 42 2993 LE so 2 wc bee eee eR RRR SE ewe we HEELERS OEE eE EO 44 210 Location eres Controller eee ee ee dstre ndondi EEO DES ee BEES ESS 47 L101 Dial Model oases ek oras EA 4 7 2 10 2 First Refinement lt 49 AQ O IIA 52 Reference 53 ot The Rodin Plato IL osos occ ecos 53 3 1 1 Eclipse in General a 53 3 1 2 The Event B Perspective a a a a 54 3 1 3 Customizing a perspective suitable for RODIN 24 97 3 14 The Event B Editor 58 LO The Proving Perspective esco 66 AF DE Pre cc ewe eee eee ewe AAA 73 AL o sonas ERR ER ew TE HARES da TT 3 2 Event B Modeling notation s ee sea awaa aoee a a E s EA 83 3 2 1 About the notation that we use no aoc sooo e so a e a a a a ae 85 HE E E E E E BEES EES 85 Sees DISCOS hb oc bb ek eee AGERE ew ORE RR 86 3 2 4 Generated proof obligations a 90 3 2 5 Visibility of identifiers cuadra 91 3 2 6 Well Definedness 0 2 00 ee ee eee erddaw ea dki addas 92 Jer Malbhematical Noaltalion s re sesa sa aad gde rea 94 Se Inou ss scoa dibaan eni i h a poea eww ee ene ee EERE A 94 Rate ARM E a E E Eee RES 96 DER o a AAA Ad 97 DOE APNO cera doors AA as 98 a III 99 3 3 6 ASCII Representations of the Mathematical Symbols 100 ee INMI cos oros rss 101 341 o IEEE 102 Pee a EN 102 Cee POC TW e esos DEE EGS 103 A o IEEE 104 3 4 5 Ho
2. AS INVARIANTS gluing peds_go TRUE lt peds_colors green In its current state this gluing invariant can be violated if the event set_peds_go is triggered for instance the variable peds go will change but peds colors will not We expect that this will result in undischarged proof obligations We can check this by expanding the machine in the Event B Explorer Indeed we now see two undischarged proof obligations compare with figure 2 14 To fix this we have to modify the two events in question Let s start with set_peds_go First we change the event from extended to not extended in the Editor as shown in figure 2 15 This change will copy the guard and action from the abstract machine so that we can modify it We can now replace the action with the corresponding action regarding peds_colors replacing peds_go true with peds_colors green While we are at it we can also rename the name of the event to something more fitting e g set_peds_green Next we perform the corresponding change on set_peds stop change the action to peds_colors red and rename the event set_peds red Lastly the event set_cars also contains a reference to peds_go that must be replaced in the second guard replace peds_go FALSE with peds_colors red Once all references to peds_go have been replace we can remove the variable peds_go from the VARIABLES section You will also need to change the INITIALISATION event to not extended and remove th
3. A AXIOMS richer_relation2 richer N id In addition we know that the relation is transitive AXIOMS richer_relation3 Vz y z x gt y richer Ay gt z richer gt 1H z richer Finally the relation is trichotomous one person is always richer than the other or vice versa never both directions AXIOMS richer_relation4 Vxr y persons A y persons Ax y x gt y E richer amp y gt x richer 2 6 INTRODUCING CONTEXTS 29 Modelling the Crime Since the objective of the puzzle is to find the killer we have to create a new constant killer which is an element of persons a CONSTANTS killer AXIOMS killer_type killer persons In addition the puzzle have some more relationships between the different persons which are all modelled as axioms We know that the killer hates his victim and is no richer than his victim a AXIOMS killer hates killer gt Agatha hates killer_not_richer killer Agatha richer Charles hates no one that Agatha hates and Agatha hates everybody except the butler a AXIOMS charles_hates hates Agatha N hates Charles Y agatha hates hates Agatha persons butler The butler hates everyone not richer than aunt Agatha and the butler hates everyone whom Agatha hates However no one hates everyone AXIOMS butler_hates_1 Vx 1 gt Agatha E richer gt butler gt x hates butler_hates_2 hates
4. Celebrity_1 b Celebrity 2 Pb Celebrity_3 Description 1 o 1items selected Figure 3 7 Double clicking on an element opens the Event B editor and marks the corresponding position 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 Search Hypothesis Cache Hypothesis Proof Tree e Proof Information e Progress Window All 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 3 8 Click on Save Perspective As in the Window menu to save the perspective 3 1 4 The Event B Editor Once a context or a machine is created a window appears in the editing area as shown in figure 3 9 By default you are in the Edit mode which allows you to edit the modelling elements of the context which are the dependencies keyword EXTENDS the carrier sets keyword SETS the constants keyword CONSTANTS and the axioms keyword AXIOMS By pressing the triangle gt next to each 3 1 THE RODIN PLATFORM 99 E Quick dds Rodin Platform File Ede Alevigqete Search Project Aum Editor hlenu Winder Help ri ial Greif ies Beret eer Ty El Proving E Quick E Event B ij Reso
5. N amp Conjunction V or Disjunction gt gt Implication lt gt Equivalence not Negation Description These are the usual logical operators Definition The following truth tables give an overview P Q PAQ PvQ P gt Q PSQ 4445 JF JFE 4H H Ala ak all 1e cit es Tr elt ale Eee T Types All arguments are predicates WD Please note that although operators like A and V are principally commutative their well definedness conditions are not Therefore if their arguments have well definedness condi tions the order matters E g x 40Ay x 3 is always well defined but y x 3Ax lt z 0 still has the well definedness condition x 0 Quantified predicates Equality Membership 3 3 MATHEMATICAL NOTATION Subsets 3 3 3 Sets and relations Sets set extensions empty set set comprehension power set finite Partition Relations Domain and Range Domain and Range Restrictions Constant relations identity the projection functions Sets of functions gt Partial functions gt gt Total functions gt gt Partial injections gt gt gt Total injections gt gt Partial surjections gt gt gt Total surjections gt gt gt gt Bijections 97 Description A partial function from S to T is a relation that maps an element of S to at most one element of
6. TRUE EVENTS Initialisation begin acti cars_go FALSE act2 peds_go FALSE end Event set_peds_go when grdi cars_go FALSE then acti peds_go TRUE end Event set_peds_stop begin acti peds_go FALSE end Event set_cars any new_value where 22 CHAPTER 2 TUTORIAL ProB tutorial_prob mac bum Rodin Platform File Edit Navigate Search Project Run ProB Window Help Ci a ar e uninitialised state set peds go set peds sto pi Formulas o set cars gt H 123 Agatha P 3 CruiseControl e I gt Paper gt 12 Paper TL 13 Sandbox H 12 Traceability 3 Trofficlight ia 1 items selected Figure 2 9 The ProB Perspective grdi new_value BOOL grd2 new_value TRUE peds_go FALSE then actl cars_go new_value end END 2 5 Mathematical notation Goals In order to understand how basic properties of a model can be expressed in Event B we need a brief introduction of predicates terms and data types In Event B we use a mathematical notation to describe the systems we want to model This allows us to be very precise about the model s properties 2 5 1 Predicates In the traffic light example we have already encountered several predicates The invariants of a model and the guards of an event Also the proof obligations generated by Rodin are predicates 2 5 MATHEMATICAL NOTATION ProB tutorial_prob mac bum Rodin P
7. Well Definedness is mentioned Event B Concepts 2 7 This is another theoretical section that provides more background about the previous examples For instance we analyze the anatomy of a machine and introduce all elements that a machine or context may have We point to literature about the theory but won t go into the details of the calculus We describe the sees and refines concepts which will be applied in the next section We will briefly mention concepts like data refinement and witnesses but leave the details to the literature 11 12 CHAPTER 2 TUTORIAL Expanding the Traffic Light System 2 8 We apply what we learned in the previous section by intro ducing a context with traffic light colors and a refinement to integrate them We will introduce another refinement for the push buttons Proving 2 9 So far all proof obligations were discharged automatically Now we switch for the first time to the proving perspective and explore it We change the auto prover configuration invalidate proofs and show that with the new configuration they don t discharge any more We prove a simple proof by hand We describe the provers available Complete Abrial Example 2 10 We pick an interesting example from the Abrial book if we get per mission We could also take one of the Rodin Wiki Tutorial examples e g Location Access Controller Outlook 2 11 This concludes the tutorial but we will provide many pointers for further reading In
8. A Va x persons hates x 4 persons noone_hates_everyone Vx x E persons A hates x 4 persons solution killer Agatha END 2 7 Event B Concepts In Event B we have two kind of components We already encountered a context that describes static elements of a model The other component is a machine that describes the dynamic behavior of a model 2 7 1 Contexts A context has the following components Sets User defined types can be declared in the SETS section See also Constants We can declare constants here The type of each constant must be given by the axioms Axioms The axioms are a list of predicates They describe what can be taken for granted when developing a model The axioms can be later used in proofs that occur in components that use see this context Each axiom has a label attached to it 2 7 EVENT B CONCEPTS 31 Theorems Axioms can be marked as theorems In that case we declare that the predicate is provable by using the axioms that are written before the theorem Theorems can be used later in proofs just like the axioms Extends A context may extend an arbitrary number of other contexts Extending another context A has the effect that we can make use of all constants and axioms declared in A and we can add new constants and axioms Rodin automatically generates proof obligations often abbreviated as PO for properties that should be proven Each proof obligation has a name that explains whe
9. For the traffic light for the cars we will present a different approach and use only one event with a parameter The event will use the new traffic light state as the argument The parameter is declared in the any section and typed in the where section AN Event set_cars an y new_value where grdi new_value BOOL then acti cars_go new_value end Note how the parameter is used in the action block Invariants If this model would control a traffic light we would have a problem as nothing is preventing the model from setting both traffic lights to TRUE The reason is that so far we only modeled the domain the traffic lights and their states and not the requirements We have the following safety requirement REQ 1 Both traffic lights must not be TRUE at the same time We can model this requirement with the following invariant please add this invariant to the model a cars_go TRUE A peds_go TRUE Obviously this invariant can be violated and Rodin can tell us that The Explorer provides this information in various ways Go to the explorer and expand the project tutorial 03 the machine mac and the entry Proof Obligations You should see four proof obligations two of which are not discharged wy Make sure that you understand the proof obligation labels Also the proof obligations can also be found via other entries Elements that have non discharged proof obligations as children are marked with a
10. This handbook consists of three parts Introduction You are reading the introduction right now It helps you to orient yourself and to find information quickly Tutorial If you are completely new to Rodin the Tutorial is a good way to get up to speed quickly It guides you through installation and usage of the tool and gives you an overview of the Event B modeling notation Reference The reference section provides comprehensive documentation of Rodin and its components Frequently Asked Questions Common issues are listed by category in the FAQ Index Particularly for the print version of this handbook we included an index In the electronic versions you may want to try the search functionality as well 1 1 1 Formats of this Handbook The handbook comes in various formats Eclipse Help Rodin is shipped with Rodin and can be accessed through the help system The handbook will be updated through the standard Rodin update mechanism Online Help You can access the handbook online at http handbook event b org PDF Help Both online versions also include a link to the PDF version of the handbook Phyiscal Book If there is enough interest we may make the handbook available through a print on demand retailer 8 CHAPTER 1 INTRODUCTION 1 1 2 Rodin Wiki This handbook is complemented by the Rodin wiki http wiki event b org Sometimes the handbook will refer to the wiki for more information Also plugin and developer informat
11. constants axioms and theorems of a project Figure 3 1 shows an overview We remind the reader of the various relationships existing between machines and contexts This is illus trated in the following figure A machine can be refined by another one and a context can be extended by another one no cycles are allowed in both these relationships Moreover a machine can see one or several contexts A typical example of machine and context relationship is shown in figure 3 2 http www eclipse org 2http en wikipedia org 59 54 CHAPTER 3 REFERENCE Machine Context variables carrier sets invariants constants events axioms Figure 3 1 Overview Machine and Context Machine Context refines extends Machine Context refines extends Figure 3 2 A typical example of machine and context relationship Rodin Nature Eclipse Projects can have one or more natures to describe their purpose The GUI can then adapt to their nature Rodin Projects must have the Rodin Nature If you create an Event B project it automatically has the right nature If you want to modify an existing project you can edit the project file and add the following XML in the lt natures gt section N lt nature gt org rodinp core rodinnature lt nature gt 3 1 2 The Event B Perspective Figure 3 3 shows an overview of the opening window of the Event B Perspective The following subsections identify the different
12. particular we will point to the literature from the Deploy project the Wiki and to plugins that solve specific problems 2 2 Before Getting Started Before we get started with the actual tutorial we are going to go over the required background to make sure that you have a rudimentary understanding of the necessary concepts v You can skip this section if e you know what formal modelling is e you know what predicate logic is e you know what Event B and Rodin refer to e you know what Eclipse is 2 2 1 Systems Development Ultimately the purpose of the methods and tools introduced here is to improve systems development By this we mean the design and management of complex engineering projects over their life cycle Examples include cars air traffic control systems etc Taking an interdisciplinary approach to engineering systems is inherently complex since the behaviour of and interaction among system components is not always immediately well defined or understood Defining and characterizing such systems and subsystems and the interactions among them is one of the goals of systems engineering In doing so the gap that exists between informal requirements from users operators marketing organizations and technical specifications is successfully bridged 2 2 2 Formal Modelling We are concerned with formalizing specifications This allows us a more rigorous analysis thereby improving the quality and
13. refined machines 92 CHAPTER 3 REFERENCE Abstract Variables Variables that are defined in an abstract machine Concrete Parameters Parameters that are defined in the event itself This does not include parameters of refined events Abstract Parameters Parameters that are defined in an abstract event concrete abstract concrete abstract sets constants variables variables parameters parameters axiom x x invariant x x x x variant x x x x guard x x x x x witness x x x x x x action x x x x x 3 2 6 Well Definedness In classical set theory see e g H B Enderton Elements of Set Theory Academic Press 1977 the formula 1 0 1 0 is true because 1 0 denotes some set or number we just do not know which one In Event B however 1 0 does not denote a particular set or number and therefore receives a specialized treatment The formula 1 0 1 0 is then neither true nor false it is ill defined Formally there is a syntactic transformation D mapping terms and formulae to a well definedness condi tion which itself is a formula The term or formula E is well defined iff D E can be proved and otherwise ill defined For example Diz y S y 0 D PV Y D P ADW V DIP AG V DW AY Dy OV x y y z is equivalent to y 4 0OVy 0 whencey 4 0 gt 1 y y x is well defined Because D preserves the symmetry of disjunction 1 y y x V y 0 is also well defined Well definedness is similar to well typedne
14. s proof calculus To help the reader differentiate between the two syntactic transformations D and we provide a summary of what is used where In the documentation of Inference rules Inference Rules and All Rewrite Rules WD refers to In the Rodin source code the term well definedness predicate refers to C E and at the time of writing the API of org eventb core ast provides no method for computing D In Rodin the goal of a well definedness 94 CHAPTER 3 REFERENCE proof obligation is created by The above rules are sound but the analog rules with D replaced by are not and they may therefore neither be added to the proof calculus nor be used to justify new inference rules ledit Design Decisions Revisited In the following we review some properties of the syntactic transformation DOM which should be preserved when introducing new operators and predicates in Event B We also list some properties of D and to illustrate some design decisions underlying their definitions edit Important Properties of DOM Technically domain conditions map sequences of terms to formulae But not every such mapping may be used as a domain condition Only variables appearing in the sequence x of variables appear free in DOM f x DOM f t DOM f x x t DOM f x syntactically only contains definite operators An operator f is definite iff DOM f x T for e
15. t Search hypotheses Figure 2 20 Search Hypothesis View you may also just select all hypotheses To add the selected hypothesis to the Selected Hypotheses View just click on the green plus button Now click on the p0 button to prove the goal x c with the Predicate prover on selected hypothesis The goal should be discharged and the Proof Control View should now show the original goal c Q x Click a second time on the p0 button in order to finalize the proof The simley in the Proof Control View should now become green indicating that all sequents of the proof tree are discharged as shown in figure After saving the proof the proof obligation remove_1 inv2 INV in the Event B Explorer should also become a green chop O There are alternative ways to prove the proof obligation For instance we can use the lasso button to load those hidden hypotheses that contain identifiers in common with the goal into the Selected Hypotheses View and we can also use it with the selected hypotheses In order to move to the next undischarged proof obligation you may also use the Next Undischarged PO button The small right arrow icon of the Proof Control View 3 1 5 The next proof can be solved the same way as the last one As an exercise try to prove Celebrity_2 A small hint We have to fill in an existential quantifier First look in the list of hypothesis to see if you find any variable that is in P and select that hypothesis Then
16. x The validity of the witness must be proven i e that x is a place holder for the parameter p or variable v for which the witness is written Witness feasibility Name eventlabel witnesslabel WEFIS Goal A c A I c v A J c v w AT c u w w gt W c v w t u x A witness W c v w t u x may contain well definedness conditions Well definedness of a witness Name eventlabel witnesslabel WWD Goal TODO 3 2 EVENT B MODELING NOTATION 89 Witness TODO From Wiki When a concrete event refines an abstract one which is parameterized then all abstract parameters must 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 pass any any D d l where where grdi d ran dap grdl p gt l aut with grd2 sit p gt l com p p dap d then l L dst d actl sit p l then end actl sit dap t 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 concrete need not be given an explicit witne
17. 102 Proof Tactics 103 proofs purging 107 purging proofs 107 reasoner 107 status of an event 90 superposition refinement 90 surjection 97 Tactics 103 theorem axiom as theorem 85 invariant as theorem 86 true as predicate T 96 Variable 18 variable 86 common variable 87 variant 90 well definedness 95 witness 88 Yellow Highlighting 19 116
18. 2 3 As this is the case here we can now save the project and the warning should disappear The three remaining warnings state that witnesses 3 2 3 are missing Double click on the warning to open the concrete model here Celebrity_2 Then expand the celebrity event and add a witness in the WITH section Click on the green plus sign to create a new entry A default witness witl has been created with a default value T e g the predicate true which we need to change Its name will have to be x if we want it to be a witness for the parameter x of the corresponding abstract event in the machine Celebrity_1 The abstract event has the assignment r x while the concrete one has the assignment r b So the content of the witness is x b The event should now look as follows Event celebrity refines celebrity when grdi R 2 with x lt Dp then acti 7 i end Edit the content and save the file One warning will disappear and only two will remain wy 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 in the Rodin Problems View The following section 2 9 2 shows the final Celebrity_2 machine 2
19. 9 2 The Final Second Refinement MACHINE Celebrity_2 REFINES Celebrity_1 2 9 PROVING SEES Celebrity_c0 VARIABLES r R b INVARIANTS invit REP inv2 be P inv3 b R inv4 Q RU Db EVENTS Initialisation begin acti r eP act2 b R WEePAR PX 10 end Event celebrity refines celebrity when eral H 0 with 2 D then aetli rip end Event remove_1 2 refines remove_1 any x where grdi TER grd2 re bek with y b y then acti R R z end Event remove_2 2 refines remove_2 any x where grdi TER grd2 x b k with y b y then acts bin acti R R a end END 43 44 CHAPTER 2 TUTORIAL 2 9 3 The First Proof In this section we prove the model of the Celebrity Problem To do this click on the box in the upper right hand corner that has a little plus sign to switch to the Proving Perspective You can switch between perspectives using the shortcut bar as shown in figure 2 17 Proving Resource Other amp Figure 2 17 Switch Persepctive A If the Proving Perspective is not available in the menu select Other Proving This will open a new window which shows all available Perspectives We should now see the window in figure 2 18 Proving Rodin Platform File Edit Navigate Search Project Run ProB Window Help mi e jw 4 as tt Proof Tree 3 gt m G m E eH A proof tree is not o avallable A E Celebrity gt i tutorial 03 gt i
20. Agatha C hates butler A Vx x persons hates x 4 persons noone_hates_everyone Vz x E persons A hates x 4 persons Finally we have to model the solution AXIOMS solution killer Agatha We mark the axiom solution as a theorem by clicking on the not theorem button as shown in figure Glee solution killer Agatha not theorem eo 0 Figure 2 12 Mark an Axiom as Theorem wy Theorems describe properties that are expected to be able to be derived from the axioms This concludes the tutorial The following Section shows the complete Context 30 CHAPTER 2 TUTORIAL 2 6 3 The Final Context CONTEXT agatha SETS persons CONSTANTS Agatha butler Charles hates richer killer AXIOMS person partition partition persons Agatha butler Charles y hate_relation2 hates persons persons richer_relation richer persons persons richer N id A Vr y 2 1 gt y E richer Ay gt z richer gt x z richer A Vr yx E persons A y E persons Ax y x gt y E richer Sy gt qx richer killer_type killer persons killer_hates killer gt Agatha hates killer not_richer killer gt Agatha richer charles_hates hates Agatha N hates Charles Y agatha hates hates Agatha persons butler butler_hates_1 Vzx 1 gt Agatha E richer butler x hates butler_hates_2 hates Agatha C hates butler
21. DLF Let us analyze whether this is an inconsistency in the model Switch to the Proving Perspective and double click on the proof obligation DLF THM 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 the axm4 of doors_ctx1 which states that there is a location where everyone is allowed to go AXIOMS axm4 311 L outside AP x 1 C aut So for every person p in P p gt l and p gt outside are in aut Since these are different at least one of them cannot be in the function sit All we need to prove now is that P is nonempty This holds since carrier sets are always nonempty but is a bit hard to prove A In the Proof Control view first disable the post tactics there is a small downward pointing arrow in the upper right hand corner above the toolbar Click on this arrow and make sure that the option Enable post tactic is unchecked in the dropdown menu We turn off the post tactics because we want to see the proof develop in its different stages 2 10 LOCATION ACCESS CONTROLLER 49 Now add the hypothesis 3x x 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 Click on the existential quantifier of the expression Jx x P appearing in the Selected Hypothesis view as demonstrated in figu
22. Its invariants can refer to the variables of the concrete and the abstract machine If a invariant refers to both we call it a gluing invariant The gluing invariants are used to relate the states between the concrete and abstract machines The events of a concrete machine can now refine an abstract event To ensure that the concrete machine does only what is allowed by the abstract one we must show two things e The concrete events can only occur when the abstract one can occur e Ifaconcrete event occurs the abstract event can occur in such a way that the resulting states correspond again i e the gluing invariant remains true The first condition is called guard strengthening The resulting proof obligation has the label con crete_event abstract_guard GRD We have to prove that under the assumption that the concrete event is enabled i e its guard are true and the invariants both the abstract and the concrete hold the abstract guards holds as well Thus the goal is to prove that the abstract guard the invariants and the concrete guards can be used as hypothesis in the proof The second condition that the gluing invariant remains true is just a more general case of the proof obligation which ensures that an event does not violate the invariant So the proof obligation s label is again concrete_event concrete_invariant INV The goal is to prove that the invariant of the concrete machine is valid when each occurence of
23. Rodin GUI elements i e Views which are visible and explain their functions Menu bar The menu bar provides file and edit operations and other useful Event B specific operations We will briefly describe the most important menu items here 3 1 THE RODIN PLATFORM 313 Menu bar Tool bar Event B Editor Outline View Event B Celebrity Celebr ty cO buc Rodin Platform Event B ProB Window Help MEN gir e 7 ep ae oz Outline axml axm2 v 5 Celebrity ve Pb Celebrity_cO gt Celebrity_c1 b SETS b Celebrity_0 aa b CONSTANTS gt O celebrity 2 rey Pint Eat Sybase Dependence O gt Q Celebrity_3 Z Rodin Problems 3 E Properties Tasks 3 Y O Ya symbols amp 0 P i Doors 0 errors 0 wamings 0 infos ele lulnl o He i tutorial 03 Description ges gt aAvV3 b tutoral 05 a gt lt gt EXTENDS g Event B Explorer Rodin Problems View Symbols View Figure 3 3 Overview of the Event B Perspective Rename menu When opening a machine or context file the following actions for automatically renaming the Event B model elements are available for the user One action is available when editing context files see figure 3 4 e Automatic Axiom Labelling this action will rename the axioms alphanumerically renaming according to their order of appearance Automatic Invariant Labelling Automatic Guard Labelling Automatic Action Labelling Customize prefixes Figure 3 4 Automatic rename actions
24. Selecting a profile for the Auto Tactics Stops when applies given tactics in given order all tactics have been applied Compose until Success applies given tactics in given order a tactic application succeeds Compose until failure applies given tactics in given order a tactic application fails applies given tactic repeatedly the child tactic application fails Selectors A selector combinator applies its given tactic to the set of nodes it selects Selected nodes are computed from the given node The given node may be open or closed It succeeds if the tactic application is successful for at least 1 selected node Selects On all pending all pending children of the given node the given node itself if it is open Post Actions A post actions applies its given tactic to the given node The given node must be open otherwise it fails Then it performs a specific treatment which is guarded by a trigger condition Trigger Condition Post Action Attempt the given node still has pending children subtree not closed prune proof tree at given node Loop on All pending JloopOnAllPending T T loop onAllPending composeU ntil Success T Tn 3 2 EVENT B MODELING NOTATION 83 ES Tactic Profile Edit the tactic profile name and the ordered list of tactics for this profile Tactics Profile name MyFirstTacticProfile List of ordered tactics to be used in this profile applied from top to bottom Available S
25. T A function is total if its domain contains all elements of S i e it maps every element of S to an element of T A function is injective is an injection if two distinct elements of S are always mapped to distinct elements of T It is also equivalent to say that the inverse of an injective function is a also a function A function is surjective is a surjection if for every element of T there exists an element in S that is mapped to it A function is bijective is a bijection if it is both injective and surjective Definition S T f fEeSoTA Ve z yenrefrevyefser y So3T f feSrTAdom f S SHT flfEeSeTafteTrs S gt T S D Nn Ss gt TT S T f feSrTaran f T 98 CHAPTER 3 REFERENCE S T S T A S oT S gt T S gt N0 5 gt T Types With S Pa T P 8 and for each operator O of gt gt gt WD SOT P P a x B For each operator O of 4 gt gt gt gt gt gt L SOT E S AL T 3 3 4 Arithmetic Sets of numbers N Nie Description Definition INT NAT NAT1 Types WD Integers Natural numbers starting with 0 Natural numbers starting with 1 Range of numbers The set of all integers is denoted by Z It contains all elements of the type The two subsets N and Ny contain all elements greater than or equal to 0 and 1 respectively The range of numbers between a and b is denoted by a b N n neZAn
26. T button or the E button You do this for axioms carrier sets constants and extended contexts Right clicking in this view will bring up a contextual menu that allows you to add a new carrier set constant axiom or extended context Synthesis Machine The Synthesis tab for machines is very similar to the one of contexts except that you have a global view of your machine s elements refined machine seen context variable invariant event variant Pretty Print Selecting the Pretty Print tab gives you a global view of your context or machine as if it had been entered through with an input text file as seen in Figure 3 24 66 CHAPTER 3 REFERENCE ctx 6 Celebrity co 3 gt p Element Content 22 axml PEN 2 axm2 ceP axm3 ke PA dc oP axm k c P c axm5 kn id o k o c o P Pretty Print Edit Synthesis Dependencies Figure 3 23 The Synthesis tab of the Event B editor ctx celebrity ctx_1 2 CONTEXT celebrity _ctx_1l EXTENDS celebrity _ctx_0 CONSTANTS A AXIOMS axm n gt axm2 a P 10 END Pretty Print Edit Synthesis Dependencies Figure 3 24 The Pretty Print tab of the Event B editor 3 1 5 The Proving Perspective When proof obligations POs 3 2 are not discharged automatically the user can attempt to discharge them interactively using the Proving Perspective This page provides an overview of the Proving Perspective and its use If the Provi
27. a modified variable is replaced by its new value The hypotheses we can use are 2 8 EXPANDING THE TRAFFIC LIGHT SYSTEM CONTEXTS AND REFINEMENT 33 e We assume that the invariant of both the concrete and abstract machines hold before the event occurred e The abstract invariants where the modified variables are replaced by their new values are valid because we know that the abstract event does not violate the invariants e The event occurs only when the guards of both the concrete and abstract machines are true These two conditions are the central piece to prove the correctness of a refinement We now just explain a few common special cases Variable re use Most often we do not want replace all variables by new ones It is sometimes useful to keep all of the variables We can do this just by repeating the names of the abstract variables in the variable section of the concrete machine In that case we must prove for each concrete event that changes such a variable that the corresponding abstract event updates the variable in the same way The proof obligation has the name concrete_event abstract_action SIM Introducing new events An event in the concrete machine might not refine any event in the abstract machine In that case it is assumed to refine skip which is the event that does nothing and can occur any time The guard strengthening is then trivially true and doesn t need to be proven It still must be proven that the gluin
28. allows the reuse of the specification to develop an implementation This comes at the cost of higher up front investments This differs from the traditional development process In a formal development we transfer some effort from the test phase where the implementation is verified to the specification phase where the specification in relation to the requirements is verified 2 2 3 Predicate Logic Predicate logic is a mathematical logic containing variables that can be quantified Event B supports first order logic which is technically speaking just one type of predicate logic http en wikipedia org wiki Systems_engineering Managing_complexity 2 3 INSTALLATION 13 2 2 4 Event B Event B is a notation for formal modelling based around an abstract machine notation Event B is considered an evolution of B also known as classical B It is a simpler notation which is easier to learn and use It comes with tool support in the form of the Rodin Platform 2 2 5 Rodin Rodin is the name of the tool platform for Event B It allows formal Event B models to be created with an editor It generates proof obligations 3 2 that can be discharged either automatically or interactively Rodin is modular software and many extensions are available These include alternative editors document generators team support and extensions called plugins to the notation which include decomposition or record support An up to date list of p
29. applied auto matically on all proof obligations after a the machine or context is saved Using this button you can invoke the auto prover within an interactive proof e executes the post tactics Y loads the hidden hypotheses that contain identifiers in common with the goal and with the selected hypotheses into the Selected Hypotheses window backtracks from the current node i e prunes its parent ok prunes the proof tree from the node selected in the proof tree F finds hypotheses containing the character string in the editing area and displays them in the Search Hypothesis view Ey displays the Cache Hypotheses view This view displays all hypotheses that are related to the current goal a loads the preceding undischarged proof obligation oP loads the next undischarged proof obligation displays information regarding the current proof obligation in the corresponding window This information corresponds to the elements that directly took part in the generation of the proof obligation events invariant etc pn moves to the next pending node of the current proof tree e loads the next reviewed node of the current proof tree You can also disable enable post tactics which allows you to decide if post tactics should run after each interactive proof step In addition you can open the preferences for post tactics For this open the menu of the Proof Control view via the little triangle on the top right corner of t
30. complex proofs For this we use the model of a Location Access Controller The goal is to develop the proofs that ensure there are no deadlocks present in the initial model and in the first refinement Through the model used in this section we study a complete system and remind the proof rules of formal development The system s task is to control the access of certain people to different locations of a site The system is thus based on whether a person has or does not have access to a particular location Before describing the initial model import the archive file Doors zip that contains the model To do this select File Import General Existing Project into Workspace Then select the according archive file and click on Finish It will take Rodin a few seconds to extract and load all the files 2 10 1 Initial Model Let us look at the initial model which consists of doors_ctx1 and doors_0 There are two carrier sets in the model context One is for people P and the other is for locations L There is a location called outside outside and a relation aut which reflects where people are allowed to go Everyone is permitted to go outside The model machine has one event pass which changes the location of a person and one variable sit which denotes where a person is located Deadlock Freeness Looking through the initial model you will see that everything already has been proved This is true but Rodin does not do any deadlock
31. development platform comprised of extensible frameworks tools and runtimes for building deploying and managing software across the lifecycle The Eclipse Foundation is a not for profit member supported corporation that hosts the Eclipse projects and helps cultivate both an open source community and an ecosystem of complementary products and services From Wikipedia Eclipse is a multi language software development environment comprising an inte grated development environment IDE and an extensible plug in system It is written mostly in Java and can be used to develop applications in Java and by means of various plug ins other programming languages including Ada C C COBOL Perl PHP Python R Ruby including Ruby on Rails framework Scala Clojure Groovy and Scheme It can also be used to develop packages for the software Mathematica The IDE is often called Eclipse ADT Ada Development Toolkit for Ada Eclipse CDT for C C Eclipse JDT for Java and Eclipse PDT for PHP Eclipse provides the technical foundation of Rodin Project Constituents and Relationships The primary concept in doing formal developments with the Rodin Platform is that of a project A project contains the complete mathematical development of a Discrete Transition System It is made of several components of two kinds machines and contexts Machines contain the variables invariants theorems and events of a project whereas contexts contain the carrier sets
32. events TODO Screenshot of selecting the context menu In refinements the Edit View of the Editor hides some information from the abstract machine by default This can be particularly important when you modify a refined event The Pretty Print View shows all the element with elements from the abstract machine in italics 2 8 EXPANDING THE TRAFFIC LIGHT SYSTEM CONTEXTS AND REFINEMENT 30 For this tutorial make sure that you right click on the machine and select refine from the drop down menu If you have created a machine the normal way and later edited the refines section the tutorial will assume that you have events e g sets_peds_go and variables that you do not have First we have to make the machine aware of the context by adding a sees statement MACHINE maci REFINES mac SEES ctxl We start with the traffic lights for the pedestrians which consist of just two colors red and green We introduce a new variable to represent the traffic light colors called peds_colors with corresponding invariant and an initialization the changes are shown in the following VARIABLES peds_colors INVARIANTS inv4 peds_colors red green EVENTS Initialisation extended begin init4 peds_colors red end END Next we will create a gluing invariant that associates peds_go from the abstract machine with the variable peds_colors that we just created The gluing invariant will map TRUE to green and FALSE to red
33. indicated in figure 4 2 The Export wizard will pop up In this window select General Archive File click Next button 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 4 3 9 How to import a Event B Project A zip file corresponding to a project which has been exported elsewhere can be imported locally In order to do that click on File Import from the menubar In the import wizard select General Existing Projects into Workspace and click Next 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 4 3 10 How to change the name of a Event B Project Select the project whose name you want to modify and then click on File Rename Modify the name and click on OK The name of your project has been modified accordin
34. instantiate b and R correctly For instance if you want to instantiate b with c then P c is a good choice for R by typing the instantiations in the Goal View and then clicking on the red existential quantifier Now all open branches of the proof tree can be proved with p0 After this we have completed all the proofs and the model is ready for use This concludes the tutorial Please note that this tutorial gave you only an introduction to proving 2 10 LOCATION ACCESS CONTROLLER AT Proving clebritytelcbrity ops Rodin Plattorm File Edit Navigate Search Project Run ProB Window Help ry Ea ajaja as l Proof Tree 4 10 Celebrity 1 3 gt Celebrity 1 T ol E B ramova 1 inv2 INV vi ah xec Wl o o G T goal Bo We a Ps v Gf simplification rewrites bo Events 7 a slds PP v Go simplification rewrites Proof Obligations SINMIALISATION inv INITIALISATION in Selected Hypotheses celebrity act1 SIM Goal ine remove L inv1 INV ceg ix remove 1 inv2 INV SF remove _2 inv1 INV iPremove 2 inv2 INV PD Celebrity 2 xm yek Proof Control 2 O Statistics 2 Rodin Problems O jE wW Symbo Propert E w f amp La gt Property Value Y pt le Tactic applied successfully Figure 2 21 The green smiley indicates that all sequents of the proof tree are discharged 2 10 Location Access Controller Goals In this section we will take a closer look at a few more
35. passed to New PP The lasso operation selects any unselected hypothesis that has a common symbol with the goal or a hypothesis that was selected before In the configuration unrestricted all the available hypotheses are passed to New PP How the Prover Proceeds First all function and predicate symbols that are different from and not related to arithmetic are translated away For example A C B is translated to Vx x A gt x E B Then New PP translates the proof obligation to CNF conjunctive normal form and applies a combination of unit resolution and the Davis Putnam algorithm 106 CHAPTER 3 REFERENCE Some Strengths e New PP outputs a set of used hypotheses If an unused hypotheses changes the old proof can be reused e New PP has limited support for equational reasoning Some Weaknesses New PP is unsound There have been several bug reports Most notably see 1 e New PP does not support arithmetic hence Fg 1 1 is discharged but Fe 1 1 2 is not Note that arithmetic reasoning when the formula is not ground is a long standing challenge e New PP is unaware of set theoretical axioms in particular Hr JA Vr rEASIEBVIEC because the union axiom is not available within New PP Roughly spoken New PP can only reuse sets that already appear in the formula but it is unable to introduce new sets Note that set theoretical reasoning is perceived as a hard problem e If unnecessary hypotheses ar
36. persons We model this by creating a partition in the AXIOMS section AXIOMS person_partition partition persons Agatha butler Charles y 28 CHAPTER 2 TUTORIAL A Please note the curly braces around the constants It s very easy to forget these which will result in typing errors that are very hard to interpret for a novice yy There is a wizard for creating the contants the set and the axiom automatically Therefore click on the New Enumarated Set Wizard tool bar item This will bring up the wizard where we can enter the name of the set and the constants in the corresponding text fields The wizard will create the enumarted set the constants and the axiom automatically Modelling the Relations Persons who hate each other and Who s how rich We create two more constants hates and richer to model the relations Persons who hate each other and Who s how rich The relations are abstract which means that they say nothing about the concrete persons Agatha the butler and Charles We define the concrete relationships between the persons later in this section The first constant hates is an arbitrary relation between persons AXIOMS hate_relation hates persons persons The second constant richer is also a relation between persons AXIOMS richer_relation1 richer persons persons However we know that the relation is irreflexive no person is richer than itself
37. proof node This allows reuse of part of a proof tree in the same or even in another proof Goal and Selected Hypotheses Each sequent in the proof tree have corresponding hypotheses and goals A user will work with one selected sequent at a time by attempting various strategies in an effort to show that the goal is true The Goal and Selected Hypotheses views provide information to the user about the currently selected sequent Figure 3 27 shows an example Create Token inv INV YW P O0 ueliser 4 ranfutok O e teToken tok Hypotheses O actlirt cauth tuy State Y Goal ES amp itrcedomlutokuit ur Goal Figure 3 27 Open proof obligation TO CHAPTER 3 REFERENCE A hypothesis can be removed from the list of selected hypotheses by selecting the check the box situated next to it you can click on several boxes at once and then by clicking on the o button at the top of the selected hypotheses window Note that the deselected hypotheses are not lost You can find them again using the Search Hypotheses F button in the Proof Control view Other buttons are used as follows o WI Select all hypotheses e Invert the selection ct next to the goal Proof by contradiction 1 The negation of the goal becomes a selected hypothesis and the goal becomes 1 e et next to a selected hypothesis Proof by contradiction 2 The negation of the hypothesis becomes the goal and the negated goal becomes a selec
38. properties of the previous section are preserved An example for a non strict operator retaining the monotonicity property is lazy multiplication mult the term mult t u denotes the same value as t u if both t and u are well defined it denotes 0 if either t or u denotes 0 and it is ill defined otherwise edit Predicates and Sets are Definite We have decided to make predicates definite i e a formula p t is well defined provided each element of t is Therefore sets are also definite i e t A is well defined provided t and A are It may be possible to allow for indefinite predicates and sets without compromising soundness of the proof calculus In that case it may be desirable to retain soundness of the following rewrite rules p t t a p x t x p x p t t is a term p a predicate and x a variable ID 3 3 Mathematical Notation Note about the current state of the documentation It would be nice for some laws like the com mutative law of addition in arithmetic to be included but this will not be part of the first iteration of the documentation The Z reference manual does this References to related proof rules would be nice to have too but again this is not part of the first iteration 3 3 1 Introduction Data types In Event B we have 3 kinds of basic data types 3 3 MATHEMATICAL NOTATION 95 e Z is the set of all integers e BOOL is the set of Booleans It has two elements
39. respective axiom invariant guard etc Goal that should be proved Hypotheses that can be used 3 2 EVENT B MODELING NOTATION 9 3 2 1 About the notation that we use Variable substitution We denote a sequence of identifiers with x 21 1 and x 7 2 As a convention we use 1 kn 15 sUn e c for constants e v and w for abstract variables and concrete variables e t and u for abstract and concrete parameters 3 2 2 Contexts A context describes the static part of a model It consists of e Carrier sets e Constants e Axioms e Extended contexts Carrier Sets A new data type can be declared by adding its name an identifier to the Sets section The identifier must be unique i e it must not have been already declared as a constant or set in an extended context The identifier is then implicitly introduced as a new constant see below that represents the set of all elements of the type A common pattern for declaring enumerated sets sets where all elements are explicitly given is to use the partition operator If we want to specify a set S with elements e we declare S as a set n as constants and add the axiom partition S e1 n Extending a context Other contexts can be extended by adding their name to the Extends section The resulting context consists of all constants and axioms of all extended contexts and the extending context itself Thus for a context o
40. the above tactical tactics 3 4 4 Provers In the end provers perform the actual work Rodin comes with one prover installed NewPP It is strongly recommended to install the third party provers from Atelier B provers as described in Section adding the PP and ML provers More provers may be available as plugins We will now give a very brief overview over the existing provers pointing out their strengths weaknesses PP PP is recommended as the prover to try first as it is sound and generally pretty good Names in the proof control P0 Pl PP Names in the proof tree PP Names in the preferences Atelier B PO Atelier B P1 Atelier B PP Input In the configuration P0 all selected hypotheses and the goal are passed to PP In the configuration P1 one lasso operation is applied to the selected hypotheses and the goal and the result is passed to PP In the configuration PP all the available hypotheses are passed to PP How the Prover Proceeds The input sequent is translated to classical B and fed to the PP prover of Atelier B PP works in a manner similar to newPP but with support for equational and arithmetic reasoning Some Strengths e PP has limited support for equational and arithmetic reasoning 3 4 PROVING 105 Some Weaknesses e PP does not output a set of used hypotheses e PP is unaware of some set theoretical axioms e PP has similar problems concerning well definedness as New PP e
41. the green plus icon Then you can finish this case with the p0 prover select the items from this case from the proof tree and hit the h0 button If this doesn t work hit the lasoo button to select all of the necessary hypotheses and try again Now you have reached the other branch of the case distinction in the proof tree In this case you can simply instantiate with since x is not situated there Finally use the p0 button to finish the proof 2 10 2 First Refinement Now we are going to explain the main complexity of our model the deadlock freeness proof for the first refinement 50 CHAPTER 2 TUTORIAL The difference between the first refinement and the initial model is that a new constant com been added in order to describe which rooms are connected Additionally we have a constant exit which will be explained later The event INITIALISATION does not change but the event PASS is refined as a consequence We assume that a person can move to another location if they have the authorization to be in 1 already defined in the abstraction and also if the location is connected to the location p where the person is at this precise moment represented by sit p We need to add a new guard that is more exact that that of the machine it refines sit p gt l com gt sit p H l We are faced with a difficulty here it is not possible to prove that the refined event PASS does not happen less often than the abst
42. the parameters of the abstract events we mean all the parameters of E and Fo Parameters An event may have an arbitrary number of parameters Their names must be unique i e there must be no constant or variable with the same name The types of the parameters must be inferable by the guards of the event We denote the parameters of all abstract events with t and the parameters of the concrete event with u Similarly to variables an event can have parameters in common with the event it refines If the refined event has a parameter t which is not a parameter of the refinement a witness W c v w u t for the abstract parameter must be specified see below 88 CHAPTER 3 REFERENCE Guards Each guard consist of a label and a predicate H c w u Variables or parameters of abstract machines are not accessible in a guard We write G c v t for the conjunction of all guards of all refined events Like axioms and invariants guards can be marked as theorems too The following proof obligation is Check the generated where Gy denotes the conjunction of the guards occurring before the theorem proof obligations A guard as theorem and text for the role of witnesses and in the case of refinement Name eventname guardlabel THM Goal A c A I c v w A Gic w u gt Ginm c w U If the guard G contains WD conditions the following proof obligation is generated WD condition of a guard Name eventname guardlabel WD
43. 1 1 2 2 3 1 Install Rodin for the first time Step 1 Download The first step is to download Rodin Rodin is available for download at the Rodin Download page Rodin is available for Windows Mac OS and Linux No matter which platform you use the distribution is always packed in a zip file Download the zip file for your system anywhere on your PC wy It is recommended that you download the latest stable version 14 CHAPTER 2 TUTORIAL Step 2 Install and Run Rodin To install Rodin extract the contents of the zip file in a desired folder You can run the tool by using the rodin executable Starting Rodin should bring up the window as shown in figure 2 1 Here you can specify the path where Rodin stores your projects Workspace Launcher Select a workspace Rodin Platform stores your projects in a folder called a workspace Choose a workspace folder to use for this session Workspace MIRES E la y Browse C Use this as the default and do not ask again Figure 2 1 Eclipse Workspace Launcher After specifying a path click on the OK button Rodin should start and bring up the window shown in figure 2 2 When using a Linux distribution a Welcome window may open up Exit out of this window to get to the main screen Other problems can also occur when installing Rodin in Linux See the release notes for details As already mentioned in Section 2 2 6 the GUI of an Eclipse application consists of Views Edi
44. 109 110 CHAPTER 4 FREQUENTLY ASKED QUESTIONS 4 2 General Tool Usage 4 2 1 Do I lose my proofs when I clean a project No This is a common misunderstanding of what a project clean does A project contains two kinds of files e those you can edit contexts machines proofs e those generated by a project build proof obligations proof statuses roughly speaking for each proof obligation discharged or not discharged The cleaner just undoes what the builder does i e it removes proof obligations and statuses but it never modifies any proof A status may change from discharged to not discharged when the proof is no more compatible with the correspondin gproof obligation because hypotheses changed for instance but the proof itself is still there You can try to replay it A confusion might arise from the possibility to launch automatic provers upon build The cleaner does not undo these automatic proofs why would it Once a proof is made the platform does not modify or delete it by itself Even obsolete proofs are preserved 4 2 2 How do I install external plug ins without using Eclipse Update Manager Although it is preferable to install additional plug ins into the Rodin platform using the Update Manager of Eclipse this might not always be practical In this case a manner to install these plug ins is to emulate either manually or using ad hoc scripts the operations normally performed by the Update Manager This ma
45. 11 2 6 2 Populate the Context In this section we model the Agatha puzzle step by step 2 6 INTRODUCING CONTEXTS 27 Event B tutonal 05 agatha buc Rodin Platform File Edit Navigate Search Project Run Rename Event B ProB Window Help ri Q e lot os ee Event B E Event B Explorer a Ria a agatha ah l oa Or Out US A G amp oe E E CONTEXT agatha if gt i tutorial 03 gt EXTENDS 2 tutorial 05 T agatha tole b CONSTANTS p AXIOMS END Pretty Print Edit Synthesis Dependencies El Rodin E Prope Tasks E Yi Symb z sProgr 75 O errors 0 warnings O infos gt le luli Ele Te Te lo Description aAwW3 2 cou Ha AA HA A ee xx 8 ll aah J Jj el ffje NI N PI nuU v mi ki EN ES E Figure 2 11 Context file opened with Structural Editor Modelling the Persons We have three persons in the Agatha puzzle Agatha herself the butler and Charles We model the three persons as constants one constant for each person in the corresponding CONSTANTS section CONSTANTS Agatha butler Charles These constants or persons respectively are part of a set Nas persons Now the constants itself are not very useful since they have no type In addition the constants will be highlighted in red indicating a problem The semantics of the sets and constants are specified in the axioms As already mentioned above the persons are part of the set
46. BOOL TRUE FALSE e User defined carrier sets These are defined in the Sets section of a context There is no assumption made about carrier sets unless it is stated explicitly as an axiom From all data types a 8 two other kinds of data types can be constructed e P a contains the sets of elements of a e a Xx B contains the pairs where the first element is of type a and the second element of type 2 A note about the notation We use the Greek letters a 6 y to represent arbitrary data types For an expression E we write E a to state that E is of type a In the following descriptions of Event B s mathematical construct we describe the types of all constructs and their components For example we will describe the maplet E gt F which is defined as EH F a x p with E a and F PB We do not make any restrictions on the types a and 6 For predicates we just describe the data types of their components The predicate itself does not have a type For example consider the components types of the equality of two expressions E F E a and F a By stating that E and F are both of type a we express that both expressions must have the same type but do not make any further assumptions about their types Well definedness A predicate which describes the condition under which an expression or predicate in Event B can be safely evaluated is the well definedness condition An example with integer division makes
47. E he EH Ee ee EEE SC Ow HS 20 3 perations ON He scans a cad be Reet e ead eee e eee PGS SEES EE Se Ha G 2 5 4 Introducing user defined types 2 Roe FO ck hee we REESE eee EES eRe a Se ee we 200 ANTIE ss eh ee ee a SR RE RHE ee RE ee ew OER a ew a 20 Introduce Comnet s sre thee OEE EERE AAA ERE Ee HO aw GS 2 Rk Re AA AAA AN 202 PFop late the LOIS 4444484 44 PRA EGEE EGER ESE Ra Ew eS EES 20 3 The Fmal Context ce owe eee ee ewe Ew Hee RE SEES EE a 2 7 Event B Concepts 2 5 46 6448 He wed RRS ER RE ewe ee hee ee AAA O O 00 00 00 00 00 NNN CONTENTS 0 E E E E E E E E E 30 Sr MEUS Gt eee he Oa ee RS IEA 31 W a carros AAA ARA 31 Cig INCOME 4442444458288 ee a AAA Kw EAE OES 32 2 8 Expanding the Traffic Light System Contexts and Refinement 33 258 1 Data Rellnement 668 6 6 00 2 HM a REE EE HE 33 2 8 2 A Context with Colors 34 2 8 3 The Actual Data Refinement 34 2 8 4 The refined machine with data refinement for peds_go 0 4 36 2 8 5 Witnesses dk cesa AA DER ee ww ee 37 200 DISCUSSION ses oo REG KR RRR CRE REEDED REED RES 38 2 8 7 The Refined Machine with All Data Refinement 0 0 00 39 2 8 8 One more Refinement The Push Button 0 0 0 0 0 0 0008 40 pe IEEE da oh He 41 A EEE 41 20 1 TheCelebrity Problem so oasis ana rr 41 2 9 2 The Final Second Refinement
48. Even though the traffic light doesn t violate the safety property from the abstract machine it doesn t behave the way described in Section We still have to ensure that the lights are activated in the proper sequence We can impose this behavior by adding four guards each of which define one transition grd_y_r cars_colors yellow gt new_value_colors red grd_r_ry cars_colors red gt new_value_colors red yellow y grd_ry_g cars_colors red yellow gt new_value_colors green grd_g y cars_colors green gt new_value_colors yellow 2 8 6 Discussion Notice that we have used two very different approaches to model the traffic lights for cars and pedestrians For the pedestrians we created one event for each state transition For the cars we handled all states in one single event You will often be confronted with situations where many modelling approaches are possible You should consider two main factors when modelling 1 readability of the model and 2 ease of proof In this case both approaches are equally good although we wouldn t recommend mixing different approaches in one model We did it here only to demonstrate both approaches We will cover deadlock freeness later in Section 2 10 1 If you are interested in the topic it may interest you to examine the traffic light model for deadlocks Consider cars_colors green red This is a legal 2 8 EXPANDING THE TRAFFIC LIGHT SYSTE
49. Goal A c AI c v w A Go c w u gt L G c w u Actions An action is composed of a label and an assignment Section 3 3 5 gives an overview of how they are assigned They can be put into two groups deterministic and non deterministic assignments Each assignment affects one or more concrete variables If an event has more than one action they are executed in parallel An error will occur if a new value is assigned to a variable in more than one action All variables to which no new value is assigned keep the same value in new and old state Witnesses Witnesses are composed of a label and a predicate that are is to establish a link between the values of the variables and parameters of the concrete and abstract events A Unlike other elements in Event B that have a label the label of a witness has a meaning and cannot be chosen arbitrarily If the user does not specify a witness Rodin uses the default witness T Witnesses are necessary in the following circumstances e The abstract event has a parameter p that is not a parameter of the concrete event In this case the label of the witness must be p and the witness has the form W c v w u p TODO I did not check this might be slightly different e The abstract event assigns non deterministically using or a value to a variable x that is not a variable of the concrete machine In this case the label of the witness must be x the witness has the form W c v w t u
50. If unnecessary hypotheses are present they may prevent PP from finding a proof even when the proof obligation obviously holds ML The ML prover can be quite helpful when the proofs involve arithmetic Names in the proof control MO M1 M2 M3 ML Names in the proof tree ML Names in the preferences Atelier B ML Input All visible hypotheses are passed to ML The different configurations refer to the configuration proof force of the ML prover How the Prover Proceeds ML applies a mix of forward backward and rewriting rules in order to dis charge the goal or detect a contradiction among hypotheses Some Strengths e ML has limited support for equational and arithmetic reasoning e ML is more resilient to unnecessary hypotheses than newPP and PP Some Weaknesses e ML does not output a set of used hypotheses e Not all set theoretical axioms are part of ML New PP New PP is unsound There have been several bug reports Some have been fixed but at this point We do not recommend New PP for inexperienced users Names in the proof control nPP R nPP with a lasso symbol nPP Names in the proof tree Predicate Prover Names in the preferences PP restricted PP after lasso PP unrestricted Input In the configuration restricted all selected hypotheses and the goal are passed to New PP In the configuration after lasso a lasso operation is applied to the selected hypotheses and the goal and the result is
51. Invariant preservation Name eventlabel invlabel INV Goal A c AI c v w A G c w c v w 90 CHAPTER 3 REFERENCE Rodin simplifies this proof obligations by replacing x with x for variables that are not changed and x by E c w u for variables that are assigned by an deterministic x E assignment There are special cases regarding initialisation Action feasibility in the initialisation Name INITIALISATION actionlabel FIS Goal A c gt F a Invariant establishment Name INITIALISATION invlabel INV Goal A c c v w Ensuring a correct refinement An event can refine one or more events of the abstract machine We first consider the refinement of only one event For refining more than one event i e merging events please see below in section 3 2 3 A concrete event must only be enabled if the abstract event is enabled This condition is called guard strengthening Merging events This section will be written in a later iteration Extending events This section will be written in a later iteration Superposition should be mentioned here Termination This section will be written in a later iteration CONTENT The variant section appears in a refined machine section 1 containing some convergent or anticipated o events section 2 This machine section contains either a natural number expression which must be decreased by each convergent event and not be increased by each an
52. L gt Y L 9 A b LWW L S Y E L G ALW L Vz p E Yr L L 32 0 Va L p Only Conditions 7 8 9 11 12 differ from the corresponding conditions in the definition of D The two syntactic transformations D and are related as follows L E gt D E is provable for every term or formula E Based on this observation the transformation D is avoided in Rodin s proof calculus as follows To prove the user has to prove and L If an inference rule contains well definedness conditions D E the rule may not be added to the list of rules available in Rodin If the well definedness conditions D E only appear as goals of antecedents and hypotheses of the consequent the rule obtained by replacing D E by L E is made available in Rodin For example instead of adding the rule TODO FORMULA the rule TODO FORMULA is added to the list of inference rules If a well definedness condition D E appears as a hypothesis of an antecedent or as the goal of the consequent the rule may not be added to the list of rules available in Rodin Therefore the above rules are unavailable in Rodin Note that avoiding D in Rodin s proof calculus is not necessary for soundness it is just a way of making sequents arising in proofs smaller The price of avoiding D in Rodin s proofs is that some formulae and sequents become unprovable edit Distinction between D and L As L E is stronger than D E mixing them up easily leads to inconsistency in Rodin
53. M CONTEXTS AND REFINEMENT 39 state but it would block set_cars_colors forever A model checker such as ProB could find it In this case however this is not a problem because with the given initialization and events this state is not reachable in the first place We hope that this section helped you to understand the power of abstraction The safety invariant from Section 2 4 3 was very simple We could now introduce colors because we are confident that the invariant will still hold assuming of course that our gluing invariant is correct 2 8 7 The Refined Machine with All Data Refinement MACHINE macl REFINES mac SEES ctxl VARIABLES peds_colors cars_colors INVARIANTS inv4 peds_colors red green inv5 cars_colors E COLORS gluing peds peds_go TRUE peds_colors green gluing cars cars_go TRUE green cars_colors EVENTS Initialisation begin init4 peds_colors red init5 cars_colors red end Event set_peds_green refines set_peds_go when grdi green cars_colors then act2 peds_colors green end Event set_peds_red refines set_peds_stop begin acti peds_colors red end Event set_cars_colors refines set_cars any new _value_colors where grdi new_value_colors E COLORS grd2 green new_value_colors gt peds_colors red grd_y_r cars_colors yellow gt new_value_colors red grd_r_ry cars_colors red gt new_value_colors red yellow y grd_ry_g cars_c
54. Perspective To do this switch to the Proving Perspective Select the project from the Event B Explorer and select and expand the component context or machine Finally select double click the proof obligation of interest A number of views will be updated with details of the corresponding proof Note that pressing the o button on the top left hand side of the Event B Explorer will remove all discharged proof obligations PO s from the view The Proof Tree The proof tree view provides a graphical representation of each individual proof step as seen in figure 3 26 The tree is made up of sequents A line of the tree is shifted to the right when the corresponding node is a direct descendant of the node of the previous line Each sequent is labeled with a comment which indicates which rule has been applied or which prover discharged the proof By selecting a sequent in the proof tree the hypotheses of the sequent are loaded to the Selected Hypotheses window and the goal of the sequent is loaded to the Goal view Decoration The symbol to the left of the leaf indicates the state of the sequent e o indicates that this sequent is discharged Are the squares next to the nodes from the up to date version of Rodin I have triangles 68 h Proof Tree 3 G L H Li a remove e in goal lv type rewrites simplification rewrites Predicate Prover simplification rewrites Se type rewrites a simplification rewrites
55. User Manual for Rodin v 2 3 Work in Progress Handbook Rev 13274 rodin handbookQOformalmind com handbook event b org September 28 2011 Contents 1 Introduction LI LIMON censor ARA AAA li Pormats of this Handbook se e o r d 26564544 Se ee RG SE See ERS wee lbs AAN te 6a a ke eR RR OMAHA ERE eae Re eS LLI TODE on eG hee EEG RH EG eo he Eee L2 cho eee eee ee osas L3 MOOUVONONS lt lt lt ee ee REE ee ki aata eee SAE RB aw we 1 4 Acknowledgements ooa Lo DIPL ge HOHE EH SOR ee ARA 1 6 Creative Commons Legal Code ee 2 Tutorial A III 2 2 Belore Gelling Started se RANA AAA RANA 2 2 1 Systems Development ooa Za Torma NCCE ck aw ewe ewe bd nesse he ewe eee Sw Re ee ww mo 220 Predicate LORIG ow kk ohh Oe wee REE EE EEDA we oe VOD aro bb we wee ERO wee ER Eee we REE a oS oe IO a REE ERE Eee OR EE ERR EERE PEE REE RHEE DES ot eee eee ee AA CEH eee Hee do MIO pe EERE Re EIA 2 3 1 Install Rodin for the first time Zoe INSTALL new OWI s acs RARA e a 2 4 The First Machine A Traffic Light Controller 241 FOIE oe Sb he ESE EER REE SEES GREE A A 2 4 2 Camille a text based editor ee 243 Building the Model gt gt s asa ee SER ee we eRe me Ree Rw a 24 4 The Final Traffic Light Model 22 6466 dee eee owe eee EE a es 40 Mathematical GON lt lt lt odioso rss ira 20 1 Predicates isss eke ER RED RRR HEE ERE EES RE EERE EER SS Aoa EIS es urraca SHES ME E
56. We can now interact with the model by triggering events this is done by double clicking on an enabled event or by right clicking it and selecting a set of parameters if applicable We first trigger INITIALIZA TION After that all events are enabled Next we trigger set_peds_go and set_cars with the parameter TRUE As expected we will get an invariant violation In the state view we can drill down and find out which invariant was violated and the history view shows us how we reached this state Figure 2 10 After modifying a machine ProB has to be restarted which is done again by right clicking the machine and selecting ProB Triggering events to find invariant violations is not very efficient But ProB can perform model checking automatically To do so select Model Checking from the Checks menu from the Events View the view on the left After optionally adjusting some parameters the checking can be triggered by pressing Start Consistency Checking Upon completion the result of the check is shown ProB has many more functions and also supports additional formalisms Please visit the ProB Website for more information This contribution requires the ProB plugin The content is maintained by the plugin contributors and may be out of date 2 4 4 The Final Traffic Light Model MACHINE mac VARIABLES cars_go peds_go INVARIANTS invi cars_go BOOL inv2 peds_go BOOL inv3 cars_go TRUE A peds_go
57. a slds EC rewrites set equality in goal a simplification rewrites Ee type rewrites simplification rewrites dom utokult u ctokutt SB simplification rewrites G R type rewrites SB simplification rewrites ER a goal O m O TASIRCHAN HE Copy af Prune Figure 3 26 The Proof Tree a indicates that this sequent is not discharged G indicates that this sequent has been reviewed CHAPTER 3 REFERENCE Internal nodes in the proof display the symbols in reverse colours Note that a reviewed sequent is one that is not discharged yet by the prover Instead it has been seen by the user who decided to postpone the proof Marking sequents as reviewed is very convenient since the provers will ignore these leaves and focus on specific areas of interest This allows the proof to be discharged interactively in a gradual fashion In order to discharge a reviewed sequent select it and prune the tree at that node the node will become brown again undischarged and you can now try to discharge it Navigation within the Proof Tree There are three buttons on the top of the proof tree view e c allows you to see the goal of corresponding to each node e allows you to fully expand the proof tree allows you to fully collapse the tree only the root stays visible Manipulating the Proof Tree Hiding The button next to each node in the proof tree allows you to expand or
58. a quatifier Y v de ah ae E EE E Ga Figure 3 30 The Proof Control View nFF A invokes the new predicate prover A drop down list indicates alternative strategies G indicates that a node has been reviewed In an attempt by the user to carry out sequents in a certain order they might decide to postpone the task of discharging some sequents until a later stage To do this the sequent can be marked as reviewed by choosing the correct node and clicking on this button This indicates that by visually checking the sequent the user is convinced that they can discharge it later but they do not want to do it right now p0 external provers can be invoked from the drop down list to test sequents using different forces de begins a proof by cases The proof is split into two branches In the first branchf the predicate supplied by the user is added to the Selected Hypotheses and the user attempts to discharge this branch In the second branch the predicate supplied by the user is negated and added to the Selected Hypotheses The user then attempts to discharge this branch ah adds a new hypothesis The predicate in the editing area should be proved by the user It is then added as a new selected hypothesis 12 CHAPTER 3 REFERENCE ae adds an abstract expression The expression in the editing area is given a fresh name e gt invokes the auto prover which attempts to discharge the goal The auto prover is
59. able must be given a type by the invariants Invariants This are predicates that should be true for every reachable state Each invariant has a label Events An event can assign new values to variables The guards of an event specify under which conditions it might occur The initialization of the machine is a special case of an event 2 7 3 Events We saw in 2 4 how an event basically looks like using the example of a traffic light Event set_cars any new _value where grdi new_value BOOL then acti cars_go new_value end 32 CHAPTER 2 TUTORIAL We have the event s name set_cars a parameter with the name new_value a guard with label grd1 and an action with label actl An event can have an arbitrary number of parameters guards and events The guards specify when an event might occur i e under which combinations of the values of the machine s variables and the parameters The actions describe what changes apply to the variables Only the variables that are explicitly mentioned in the actions are affected All the other variables keep their old values Beside the simple assignment there are other forms of actions or which are explained in the reference section 3 2 3 The initialization of the machine is a special form of event It has neither parameters nor guards Now our aim is to prove that the invariants always hold To do this we must prove two things e The initialization leads to a sta
60. achines With some restrictions the abstract variables v and concrete variables w can have variables in common If a variable v is declared in a machine M it can be re used in the direct refinement M 1 In that case it is assumed that the values of the abstract and concrete variable are always equal To ensure this special proof obligations are generated see below in section 3 2 3 Once a variable disappears in a refinement i e is not declared in machine M 19 it cannot be re introduced in a later refinement Events A possible state change of a machine is defined by an event The condition under which an event can be executed is given by a guard The event s action describes how the new and old state relate to each other Events occur atomically i e one event happens at a time leading to a new state Two events never happen at the same time Time is also not factored into the execution of the event An event has the following elements e Name e Parameters e Guards Witnesses Actions Status ordinary convergent or anticipated The status is used for termination proofs see section 3 2 3 for details An event can refine one or more events of an abstract machine To keep things simple we will first consider events with only one refined event If there are several refinement steps e g event E is refined by Es and Ex by 3 we call Ej and E gt the abstract events and Es the concrete event Likewise if we refer to
61. added to this project and to the faulty component in the Event B Explorer The error itself is shown in the Rodin Problems view i e syntax errors of the active Event B editor 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 Symbols View The symbols view is intended to give users a convenient way to type in mathematical symbols into the various model editors If an editor is open and a text field is active the cursor is blinking then clicking a symbol inserts it at the current position as demonstrated in figure 3 6 The ASCII code corresponding to the symbol over which the mouse hovers is also displayed as a tooltip so that the user can also learn how to input symbols directly 3 1 THE RODIN PLATFORM ov 0 0 Outline E E Pi See ae elebrity_c0 3 Y Celebrity_ T o axml jaxm3 ke P c P not theorem axm laxm4l kk c P Y c not theorerr ias am laxm5 kn id ol not theorem it axm5 e6352 ID o c y Print Edit Synthesis Dependencies y eP din Problems amp E Properties ej Tasks Y o Symbols 5 om rs O warnings O infos E Miel hana td ll Ee Soe gt C C t ription gt ga x lt e ll Figure 3 6 Clicking a symbol inserts it at the current position Event B Explorer Projects can be found in the RODIN platf
62. aming when elements should be alphanumerically ordered as well as when new elements are created 18 CHAPTER 3 REFERENCE Preferences type filter text z Colors and Fonts lt Fyent B Preferences for Event B editor colors and fonts Appearance Show borders Colors and Fonts Text foreground Comment foreground MN Modelling UI Context Editor Machine Editor Prefix Settings Proving Ul Sequent Prover Auto Post Tactic Restore Defaults Apply 9 cone 7 Figure 3 38 Colors and Fonts preferences Figure 3 39 shows that modifying prefixes on the workspace level or on the project level will affect the names used at creation of new Event B elements One can see that the prefixes for variables and invariants which were originally set to var or inv have been replaced by variable and invariant New elements are then named using those prefixes How to set prefixes Prefix settings can be accessed through in two different ways depending on the scope of their application Window Preferences Event B Modelling Ul Prefix settings or directly via Rename Customize prefixes Project specific settings The user can select profiles locally for a project To do so you can select the Prefix Settings property page available via right click on a project and select the Properties item You can also click on the Configure project specific settings link on the Prefix Settings preference pa
63. and external provers and is applied automatically after each interactive proof step However it can also be invoked manually by clicking on the e button in the Proof Control view Note that the post tactic can be disabled quickly by clicking on the little arrow marked with an A of the Proof Control view right upper corner and then on Disable post tactic option B as shown in figure 3 37 Principles The ordered list of rewrite tactics inference tactics and external provers that should be applied is called a profile There are two default profiles One is for auto tactics and one is for post tactics These 3 1 THE RODIN PLATFORM 7 gt Proof Control O ES Figure 3 37 Proof Control view menu default profiles are immutable in time but can be duplicated for further modification by the user The user can edit a profile and select it to run as automatic or post tactic The idea is to have a set of available tactic profiles to be used as needed Moreover these edited profiles are shipped with projects if defined at the project level or can be imported or exported if defined at a workspace level This makes it easy to share the profiles There are two ways to run the automatic or post tactics e Manually by clicking on the ih button or the e button in the Proof Control view to launch the auto tactic with the selected auto tactic profile and the post tactic with the selected post tactic profile respectively e Automatically if such p
64. antifier the type of the variable must be clear In this case Rodin can infer that x must be of type integer because the operator lt is defined only on integers Sometimes the type cannot be inferred e g in Va b la b gt bX a ASCII la b a b gt b a 24 CHAPTER 2 TUTORIAL a and b could be integers boolean values or some other type In this case we must make the type of the variables explicit by stating that a and b are elements of the appropriate sets Let s use integers again Va b a E LZADbELNAFbD gt bLbAH A ASCII la b a INT amp b INT amp a b gt b a The conjunction operator A has a stronger binding that the implication gt so the above is equivalent to Va b a E LZALEZAMAFD gt bXHa If you are unsure which of the operators bind stronger we advise you to use parenthesis to avoid mistakes Existential quantification on the other hand is used to state that there is an object of a certain type fulfilling a given property Let s express the statement that there is a Boolean value different from TRUE Jx x BOOL z 4 TRUE ASCII x x BOOL amp x TRUE As you can see we again added type information for x We put the type information for the universal quantification on the left side of the implication but for existential quantification we add it via a conjunction A 2 5 2 Data types We have seen that each identifier i e a variable constant or parameter must have a distinguished typ
65. archive file and click on Finish Rodin 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 as you can see in the Rodin Problems View compare with figure 2 16 In the first part of this section our goal is to fix these problems Let s take a look at the warning stating that the event label celebrity is misused Inconsistent use of event label celebrity Double click on the warning to open the Celebrity_1 machine Select the event celebrity The problem is that the event is not 42 CHAPTER 2 TUTORIAL Rodin Problems O Properties 4 Tasks cS Se O errors 5 warnings O infos Description A Resource Path Y E Warnings 5 items amp Abstract event celebrity not refined although not disabled Celebrity_1 bum Celebrity amp Inconsistent use of event label celebrity Celebrity_1 bum Celebrity Witness for x missing Default witness generated i Celebrity 2 bum Celebrity bo Witness for y missing Default witness generated Celebrity 2 bum Celebrity b Witness for y missing Default witness generated Celebrity 2 bum Celebrity Figure 2 16 Warnings in the Rodin Problems View declared as a refinement To solve the problem expand the event and add a new entry in the REFINES section Click on the green plus sign to create a new entry This declares that the event is a refinement of an event with the same name in the abstract machine 3
66. are stored in proof files Each time a new proof obligation is generated by the tool a corresponding initially empty proof is created However proofs are never removed automatically by the Rodin platform As time passes and a model is worked out obsolete proofs e g proofs that do not have a corresponding proof obligation anymore accumulate and clutter proof files The purpose of the proof purger is to allow the user to delete obsolete proofs Why proofs become obsolete Proof obligations are named after the main elements related to it such as events and invariants Therefore each time such an element is renamed manually the corresponding proof obligations get a new name However the existing proof is not renamed and a new proof gets created with the new name Therefore after a lot of model editing there are more and more obsolete proofs stored in proof files Selecting purge input In any view right clicking an Event B project or file will display a popup menu containing a Purge Proofs entry If several files or projects or both are selected purging will apply to all of them Firstly the proof purger tries to find obsolete proofs in the selection If no obsolete proof is found a message will pop up telling that no proof needs to be purged Otherwise a new window will pop up displaying a list of all POs that are considered obsolete that is all proofs that exist in some proof file and that do not have any corresponding pro
67. athematical proof to verify consistency between refinement levels More details are available in http www event b org 4 1 2 What is the difference between Event B and the B method Event B 2 2 4 is derived from the B method Both notations have the same inventor and share many common concepts set theory refinement proof obligations However they are used for quite different purpose The B method is devoted to the development of correct by construction software while the purpose of event B is to model full systems including hardware software and environment of operation Both notations use a mathematical language which are quite close but do not match exactly in particular operator precedences are different 4 1 3 What is Rodin The Rodin Platform is an Eclipse based IDE for Event B that provides effective support for refinement and mathematical proof The platform is open source contributes to the Eclipse framework and is further extendable with plugins 4 1 4 Where does the Rodin name come from The Rodin Platform was initially developed within the European Commission funded Rodin project IST 511599 where Rodin is an acronym for Rigorous Open Development Environment for Complex Systems Rodin is also the name of a famous French sculptor one of his most famous work being the Thinker 4 1 5 How to contribute and develop Glad to hear that you want to help Please see the Developer FAQ page
68. collapse the subtree starting at that node 3 1 THE RODIN PLATFORM 69 Pruning The proof tree can be pruned at a selected node This means that the subtree of the selected node is removed from the proof tree The selected node becomes a leaf and displays the symbol a The proof activity can then be resumed from this node After selecting a node in the proof tree pruning can be performed in two ways e by right clicking and then selecting Prune e by clicking on the of button in the proof control view Note that after pruning the post tactic is not applied to the new current sequent The post tactic should be applied manually if required by clicking on the post tactic button in the Proof Control view This is especially useful when you want to redo a proof from the beginning The proof tree can be pruned at its root node and then the proof can proceed again with invocation of internal or external provers or with an interactive proof Before pruning a particular node the node and its subtree can be copied to the clipboard If the new proof strategy subsequently fails the copied version can be pasted back into the pruned node see the next section Copy Paste By selecting a node in the proof tree and then right clicking with the mouse you can copy the part of the proof tree starting at that sequent including the node and its subtree Pasting the node and subtree back in is done in a similar manner with a right mouse click on a
69. diting area For example if we search for hypotheses involving the character string cr then after pressing the Search Hypothesis EY button on the Proof Control view we obtain the windows as shown in figure 3 32 This view also integrates a quick search area A that allows us to search quickly hypotheses involving short character strings such as cr a search hypothesis button B that behaves the same as the button of 74 CHAPTER 3 REFERENCE Ey Search Hypothesis 3 5 A Fa e B C cens creta csscr a lar 0 ca cr 1 r 0 A a 1 cr lt ca a 0 ca cr E A EA A A E 40808000 r 1 ca cr Figure 3 32 The Search Hypotheses View the proving window a refresh button C that updates the window manually for more control and a drop down menu D to set the preferences of the view up By pressing return key or the button B once a short string has been entered into the input area A hypotheses can be searched quickly as if we used the Proof Control as described before The drop down menu D allows some preferences about the searched hypotheses to be set If we change preferences for the search we might need to manually update the view with the button C By selecting the Consider hidden hypotheses in search option we can review all hypotheses that have been unselected in the Selected Hypotheses window To move hypotheses to the Selected Hypotheses window select the wanted hypothesi
70. e Celebrity 1 bo Variables b Invariants x e yek b 4 Events 7 Proof Obligatio 7 O INITIALISATI ME O INITIALISATI GE PY 0 celebrity actl GS remove_1 in remove 1 in Proof Control z vog ero pr by p mmm F oe acd 0 3 amp Symbols O ey b E 1 Items selected Selected Hypotheses Figure 2 19 Proof Obligation Make sure that you understand the different buttons in the Proof Control View 3 1 5 In order to prove the proof obligation it suffices to prove x c Type this into the Proof Control View 3 1 5 and press the Add Hypothesis button ah In order to revert a step click on a node in the Proof Tree View and click on the scissors button in the Proof Control View or open the context menu of a node and select Prune The new goal is x c Now try selecting the right hypotheses by yourself in order to complete the proof To do this click on the Search hypothesis button in the Proof Control View On the left side we should see now the Selected Hypotheses View compare with figure 2 20 If you cannot find the right hypotheses 46 CHAPTER 2 TUTORIAL Search Hypothesis El O Celebrity 1 E 7 move L inv2 IN Jf rpms oi He O ct ceq mj ct Pc ct xEQ O ct lt eP lected Hypothese E keP c P O ct Goal amp IE AE El XSL O ct knidsg o ct Proof Control Es O ct Scr I ct ceg Fo ppv i ct xEQ O ct xX H yek Ol amp
71. e If we can introduce an identifier anywhere we usually must also add a predicate with which the identifier s type can be determined In the traffic light example a variable cars go was introduced and typed by an invariant cars_go BOOL In the next section we ll see constants that will be typed by axioms also predicates and later we ll see parameters that will be typed by guards again predicates In general each term in Event B has a certain type When saving a Event B component Rodin starts the type checker to ensure that types a correctly used For example the terms on both sides of an equality must have the same type If this is not the case Rodin shows an error message For each type there exists a set that denotes exactly all elements that belong the type We will now briefly give an overview about all types you might encounter Integers We have already seen numbers which are of type integer Z Example terms of type Z are 5 x 7and7 y 3 Booleans We have already seen the Boolean type BOOL in the previous section 2 4 It has exactly two elements BOOL TRUE FALSE Deferred sets An user can introduce a new type by adding its name to the Sets section of a context We see that in more detail in the next section 2 6 Sets If we have terms of a certain type we can easily construct sets of that type E g 1 and 2 x denote integers Z and 1 2 xp is a set of integers P Z P S ASCII POW denotes the p
72. e V hyp mp instantiated with and the hypothesis that was considered by this rule the line below Input Sequent Furthermore it is possible to view the antecedents created by this rule in details i e child proof tree nodes and the actions performed on the hypotheses selection deselection etc Auto tactic and Post tactic The auto tactic automatically applies a combination i e ordered list of rewrite tactics inference tactics and external provers to newly generated proof obligations However they can also be invoked by the user by 76 CHAPTER 3 REFERENCE GR Rule Details 3 Rule Y hyp mp instantiated with P d x Vs xEsAC s os f S Input Sequent Vs s lt C s gt s 0 goal Antecedentl ET Deselect Ws 5 lt C s 5 0 Antecedent2 EP x Ws xEsaC s os fes x cC P x Ws xEsaC s os fes x Deselect Ys 5sCcC s s 0 Antecedent3 P Vs xEsaAC s es gt fEsS x 0 goal Deselect Ws 5 lt C s s 0 Figure 3 35 Rule Details View clicking on the ih button in the Proof Control view Note that the automatic application of the auto prover can be quickly toggled with the Prove Automatically menu item available from the Project menu See Figure 3 36 Search Project Run Editor Menu Window Help Close Project Build Working Set Clean w Build Automatically Properties Figure 3 36 Toggle auto prover via project menu The post tactic is also a combination of rewrite tactics inference tactics
73. e action which initialises the variable peds_go Now you shouldn t have any errors or warnings and all proof obligations should be discharged If you get the error message Identifier peds_go has not been declared then there are references to the refined variable left somewhere in the model It can be helpful to use the Pretty Print view as it will show the inherited elements from the abstract machine as well 36 CHAPTER 2 TUTORIAL macl e o Variables Pe Invanants H Events Proof Obligations G INTIALISATION inv4 INV G INTIALISATION gluing INV set_peds_go gluing INV set_peds_stop gluing INV Figure 2 14 Mapping between Abstract and Concrete Events 7 set peds go extended ordinary uO gt REFINES pS extended a et sel peds go er gt ANY ept gt WHERE ett lt WITH erd 7 THEN ept END Figure 2 15 Switch from extended to not extended 2 8 4 The refined machine with data refinement for peds_go MACHINE macl REFINES mac SEES ctxl VARIABLES cars_go peds_colors INVARIANTS inv4 peds_colors red green gluing peds_go TRUE lt peds_colors green EVENTS Initialisation begin acti cars_go FALSE init4 peds_colors red 2 8 EXPANDING THE TRAFFIC LIGHT SYSTEM CONTEXTS AND REFINEMENT 37 end Event set_peds_green refines set_peds_go when grdi cars_go FALSE then act2 peds_colors
74. e present they may prevent New PP from finding a proof even when the proof obligation obviously holds We therefore advise to unselect unnecessary hypotheses e New PP does not take well definedness into account Lemma Hz b f f b is not discharged In fact this sequent has exactly the same translation as Fg b dom f which is not provable e New PP tends to run out of memory if the input is large 3 4 5 How to Use the Provers Effectively It is very hard in general to predict whether a certain automatic prover can or cannot discharge a given proof obligation within a given amount of time This is also the case for many other automatic first order theorem provers Therefore applying the 11 configurations in a trial and error fashion is often frustrating The following guidelines may be useful Add New PP restricted PP restricted PO Atelier B PO and ML Atelier B ML to the auto tactic If the auto tactic runs out of memory remove New PP If the model is small add New PP after lasso PP after lasso and P1 Atelier B P1 to the auto tactic Whenever you think that the current proof obligation should be discharged automatically invoke the auto tactic the green robot instead of some particular automatic prover If the auto tactic fails it is usually best to simplify the proof obligation in some way The most important ways of simplifying the proof obligation are Remove unnecessary hypotheses add
75. e several other combinators and auto tactic editors The following is a list of combinators present by default One may notice the absence of child specific combinator i e combinators that apply tactic T1 on the first child T2 on the second child etc even though this kind of combinator exists in other provers The reason is that we are concerned mainly auto tactics and these are tactics that are attempted in a general context Provers with child specific combinators are used to make manual proof because they require proof specific adaptation Composers A composer combinator applies its given tactic s to the given node The given node may be open or closed It succeeds if at least 1 tactic application is successful 32 CHAPTER 3 REFERENCE Preferences MES Auto Post Tactic c Pb General Event B Customize Event B Tactics Configure project specific settings t Appearance l Auto Post Tactic Profiles P Modelling Ul Proving Ul Profile Details Sequent Prover True Goal Discharge parece Auto Post Tactic False Hypothesis Discharge gt Help Goal in Hypotheses Dischal Install Update Functional Goal Discharge Run Debug Belongs to domain Dischar e Team Functional image memberst Duplicate Bounded Goal with finite Hy Datatype Destructor WD Di Atelier B ML Discharge Partition Rewriter Simplify Simplification Rewriter Simp gt Restore Defaults Apply Cancel OK Figure 3 42
76. e the notion E 11 t to specify which free identifiers may occur in the expression EF Deterministic Assignments Description Definition Types WD deterministic assignment X1 Tp E c w u E c w u assigns the expressions E to the variable x with 2 1 n All x must be distinct identifiers that refer to variables of the concrete machine Cc w u represent the sequence of all constants variables of the concrete machine and parameters of the concrete event There is a special form of the assignment wich does a relational overwrite x F c w u E c w u The before after predicate of 1 n E c w u En c w u is xi Ei c w u A A h E c w u The assignment is equivalent to z1 n x Ey c w u A Ax E c w u 1 n The special form is syntactic sugar for x Ej c w u Eo c w u w a4 E c w u gt Exs c w u x a and E c w u e a fori 1 n Dl EW DO asis Enl L x E c w u Es c w u w u L E c w u n AL E c w u L E c w u A L E2 c w u D amp Non deterministic assignments Description Definition non deterministic assignment with a before after predicate X1 Tp Q c W U 1 4 assigns to the variables z1 1 any value such that the the before after predicate Q is fulfilled All x are identifier that refer to a variable of the concrete machine c w u represent the sequ
77. e view rewrite rules also as inference rules In the future more rules will be added to this list so that more sequents will be provable In particular the following rules may also be used to prove a sequent TODO FORMULA A formula is provable if and only if the sequents F gand D are provable It can be checked see F D Mehta Proofs for the working engineer Diss ETH Zurich 2008 that for each term or formulae E the formula D E is provable iff F D E is provable We therefore say that a term or formula is well defined iff its well definedness condition is provable A term or formula is ill defined iff it is not well defined Informally well definedness conditions appear in two ways during proofs When proving a formula we also have to prove its well definedness When proving a sequent we may always assume that the hypotheses and the goal of the sequent are well defined L Well Definedness As D E in the worst case grows exponentially in the size of E D is never evaluated explicitely in the Rodin platform To avoid evaluating D we define the syntactic transformation as follows Again x ranges over variables f over operators p over predicates t over sequences of terms of length t and over formulae All terms and formulae are well formed and well typed L x T L f t DOMENE AAA L ti LAE o Ve L LH AZ L t L T S L 1 T 50 L G L 9 0 Lle A o gt LY L 0V 0 9 A 96 c w
78. ect must have the Rodin Nature 3 1 1 to work A project can have more than one nature Next create a new Event B Component Either use File New Event B Component or right click on the newly created project and select New Event B Component Use mac as the component name and click Finish as shown in figure 2 6 This will create a Machine 3 2 3 file New Event B Component This wizard creates a new Event B component machine context etc that can be opened by a multi page editor Project tutorial 03 Browse Please choose the type of the new component Machine O Context a cancel Figure 2 6 New Event B Component Wizard The newly created Component will open in the structural editor The editor has four tabs at the bottom The Pretty Print shows the model as a whole with color highlighting but it cannot be edited here This is useful to inspect the model The Edit allows editing of the model It shows the six main sections of a machine REFINES SEES etc in a collapsed state You can click on the little triangle to the left of a section to expand it 18 CHAPTER 2 TUTORIAL The editor is form based This means that in well defined places an appropriate control text field dropdown etc allows modifications wy Alternative editors are available as plug ins The form editor has the advantage of guiding the user through the model but it takes up a lot of space and can be slow for big m
79. ed e Export them e Remove them e Restart Rodin e Go back to the preference page and import update sites back from the previously exported file 4 3 Modeling 4 3 1 Witness for Xyz missing Default witness generated A parameter has disappeared during a refinement If this is intentional you have to add a witness telling how the abstract parameter is refined 4 3 2 Identifier Xyz should not occur free in a witness You refer to Xyz in a witness predicate where Xyz is a disappearing abstract variable or parameter which is not set as the witness label 4 3 3 In INITIALISATION I get Witness Xyz must be a disappearing abstract variable or parameter The witness is for the after value of the abstract variable hence you should use the primed variable The witness label should be Xyz and the predicate should refer to Xyz too 112 CHAPTER 4 FREQUENTLY ASKED QUESTIONS 4 3 4 I ve added a witness for Xyz but it keeps saying Identifier Xyz has not been defined As specified in the modelling language manual the witness must be labelled by the name Xyz of the concrete variable being concerned 4 3 5 What are type expressions in Event B The type expressions are defined recursively as follows e Built in types Z BOOL Note that N is NOT a type expressions e Any carrier set is a type expression e If T is a type expression then T is a type expression e If S and T are type expressions then ST is a type expre
80. elected Implicative Goal Simplify For all Goal Simplify Use Equals Hypotheses Simplify Exists Hypotheses Simplify Find Contradictory Hypotheses Discharge Shrink Implicative Hypotheses Simplify Shrink Enumerated Set Simplify gt gt Implicative Hypotheses with Conjunctive RHS Simplify Implicative Hypotheses with Disjunctive LHS Simplify Conjunctive Goal Split Clarify Goal Mixed Functional Overriding in Goal Split Functional Overriding in Hypothesis Split One Point Rule in Hypotheses Split One Point Rule in Goal Split A ee A ee ee ee a a Cancel Finish Figure 3 43 Selecting a profile for the Auto Tactics Other Ideas timeout a post action of arity 1 with duration as input limits the time allocated for the tactic that it is applied to fails after time has gone out limitDepth a post action of arity 1 with depth as input limits the proof tree depth for the tactic that it is applied to prevents tree from growing beyond a given depth 3 2 Event B Modeling notation In Event B we have two types of components contexts and machines Here we describe briefly the different elements of a context or machine We do not use a specific syntax for describing the components because the syntax is dependent on the editor that is used The default editor requires a structure which contains the elements that are described here Proof obligations are generated to guarantee ce
81. en light any more Consider the following scenario 1 pedestrians get green light 2 the light turns red 3 a pedestrian presses the button again 4 this prevents the car lights from turning green Instead the pedestrians get a green light again and the cycle continues There are tactics to address all these issues However it is rarely possible to generate proof obligations for such scenarios without making the model much more complicated It can be useful to use model checkers 77 to validate the model s behaviour or even to use temporal logic to articulate properties of the model wy As an exercise try to improve the model to address these issues 2 9 Proving Goals The goal of this section is to get familiar with the Proving Perspective and to carry out a simple proof by hand 2 9 1 The Celebrity Problem In this section we will work on the model of the so called celebrity problem In the setting for this problem we have a knows relation This relation is defined so that e no one knows himself e the celebrity knows nobody e but everybody knows the celebrity The goal is to find the celebrity Make sure that you have no existing Project named Celebrity If you do then rename it To do so right click the project and select Rename Import the archive file Celebrity zip to you Event B Explorer To do this select File Import General Existing Projects into Workspace Then select the according
82. ence of all constants variables of the concrete machine and parameters of the concrete event 1 n are in wW This is the most general form of assignment all other assignments can be converted to this The before after predicate is Q c w u 1 4 100 CHAPTER 3 REFERENCE Types x a and E c w u Pa WD iaa LO CE Ud DA OLE WA sl n Feasibility Fita Da OE WU S rl OCW rl y n E non deterministic assignment of a set member Description x E c w u assigns to the variable x any value of the set E x is an identifier that refers to a variable of the concrete machine c w u represent the sequence of all constants variables of the concrete machine and parameters of the concrete event Definition The before after predicate is x E c w u The assignment is equivalent to x 2 E c w u Types x Q and E c w u Pa WD L 2 E c w u L E c w u Feasibility F x E c w u E c w u 4 3 3 6 ASCII Representations of the Mathematical Symbols CONTENT Pre 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 U
83. er the symbol in question 2 4 THE FIRST MACHINE A TRAFFIC LIGHT CONTROLLER 19 7 ITESO erg pP o HEEE y O EET t t Figure 2 7 Red highlighted elements indicate errors After saving you should see that the EVENTS section is highlighted in yellow as demonstrated in Fig ure 2 8 Again the Rodin Problems view gives us the reason Variable cars_go is not initialized Every variable must be initialized in a way that is consistent with the model EVENTS ero gt g amp INITIALISATION not extended ordinary Y e 5 2 END Figure 2 8 Yellow highlighted elements indicate warnings To fix this problem expand EVENTS and in turn the INITIALIZATION event Add two elements in the THEN block These are actions that also have labels In the action fields provide cars_go FALSE and peds_go FALSE State Transitions with Events Our traffic light controller cannot yet change its state To make this possible we provide events We start with the traffic light for the pedestrians and we will provide two events one to set it to go and one to set it to stop From now on we won t describe the individual steps in the editor any more Instead we will simply show the resulting model The two events will look as follows Event set_peds go begin acti peds go TRUE end Event set_peds stop begin acti peds_go FALSE end 20 CHAPTER 2 TUTORIAL Event parameters
84. ers wD If you specify two variables x and y with x Z and y N then both are of type integer Z N is not another type There is just the additional condition y gt 0 2 6 Introducing Contexts v Goals In this section we introduce contexts that apply to the theoretical concepts that were introduced in the previous section 2 5 We will create a very simple model consisting of just one context file In this tutorial we will create a model of the well known Agatha puzzle Here is a brief description of the puzzle Someone in Dreadsbury Mansion killed Aunt Agatha Agatha the butler and Charles live in Dreadsbury Mansion and are the only ones to live there A killer always hates and is no richer than his victim Charles hates no one that Agatha hates Agatha hates everybody except the butler The butler hates everyone not richer than Aunt Agatha The butler hates everyone whom Agatha hates No one hates everyone Who killed Agatha The objective of this Section is to get familiar with contexts by modeling the Agatha puzzle 2 6 1 Create a Context Create a new Event B Project File New Event B Project Give the project the name tutorial 05 Next create a new Event B Component Unlike in Section 2 4 use agatha as the component name and mark the Context option in order to create a Context file instead of a Machine 3 2 3 file Click on Finish Rodin should start the editor with the created Context file see figure 2
85. for machine files Three actions are available for machine files see figure 3 5 e Automatic Invariant Labelling this action will rename the invariants alphanumerically according to their order of appearance 56 CHAPTER 3 REFERENCE e Automatic Guard Labelling this action will rename the guards alphanumerically according to their order of appearance e Automatic Action Labelling this action will rename the actions alphanumerically according to their order of appearance MEF Event B ProB Window Help Automatic Axiom Labelling Customize prefixes geMe 3 Celebnity_cl 3 ANTEVT Calahkritiu 1 Figure 3 5 Automatic rename actions for context files Event B menu When opening a machine or context file some wizards for creating Event B model elements are available for the user The different wizards are described in section 3 1 4 Tool bar The tool bar provides short cuts for familiar commands like save print undo and redo The tool bar also provides short cuts to the wizards for creating elements like axioms constants enumerated sets etc which are described in section 3 1 4 Editor View The editor view contains the active Event B editor which is described in section 3 1 4 Outline View The outline view displays the outline of the active Event B editor and lists elements like axioms variables etc Rodin Problems View When the Static Checker discovers an error in a project a little x is
86. freeness proof yet so we will have to add them by ourself A model 48 CHAPTER 2 TUTORIAL is considered as deadlocked if the system reaches a state with no outgoing transitions The objective of this section is to develop proofs for deadlock freeness for the initial model and for the first refinement Consider the event pass from the initial model EVENTS Event pass any P l where grd11 p gt lE aut grd12 sit p H l then aon sip gt end END Since the initial model has only one event pass the system might deadlock when both guards of the event grd11 and grd12 are false In this case to prove that no deadlocks can occur requires proving that someone can always change room Clearly we want to avoid this happening We must therefore prove that the two guards are always true To do this add a new derived invariant to doors_0 called DLF click the theorem button to make it derived and change the predicate so that it is the conjunction of the two guards INVARIANTS DLF Jp l p gt le aut A sit p E I uy Refer to the ProB Plugin with the deadlock freeness function Save the machine We will see that the autoprover fails to prove the theorem DLF THM If you don t see the proof obligation DLF THM maybe you forgot to mark the invariant as a theorem by clicking on the theorem button Another reason that you don t see the proof obligation DLF THM could be that you forgot to rename the invariant
87. g invariant holds but this time under the assumption that the abstract machine s variables have not changed Therefore the new state of our newly introduced event corresponds to the same state of our abstract machine from before the event happened Witnesses Let s consider a situation where we have an abstract event with a parameter p and in a refining event that no longer needs that parameter We saw above that we have to prove that for each concrete event the abstract event may act accordingly With the parameter however we now have the situation that we must prove the existence of a value for p such that an abstract event exists Proofs with existential quantification are often hard to do so Event b uses the construct of a witness A witness is just a predicate of the abstract parameter with the name of the variable as label Often a witness has just the simple form p 2 8 Expanding the Traffic Light System Contexts and Refinement Goals We apply what we learned in the previous section by introducing a context with traffic light colors and a refinement to integrate them We will also introduce another refinement for the push buttons 2 8 1 Data Refinement We will continue the example from Section 2 4 where we built a simplified model of a traffic light controller The model was simplified because we abstracted the traffic lights to TRUE and FALSE and a number of features were still missing We will introduce data refineme
88. ge In this case one will have to choose the project for which the prefixes should be set up This is allowed via a specific project selection dialog After the project selection a dialog for prefix settings opens for the selected project A window see figure 3 40 appears where a page handling prefixes settings allows a user to customize prefixes for a chosen project On this page the user can toggle the button Enable project specific settings e If this button is enabled the prefixes used are those which are specified at this project level e If this button is not enabled the prefixes used are those which are defined at the workspace level Sequent Prover Auto Post Tactic Preferences for the selected auto and post tactic profile This section describes the Auto Post Tactic tab of the Auto Post Tactic preference page There are two scopes to set up preferences for the auto and post tactics the workspace level and the project level Note that if the automatic application of tactics is decided only at the workspace level this option will also be set for the project level To access these preferences open the Auto Post Tactic preference page that can be found after Window Preference Sequent Prover Figure 3 41 shows the Auto Post Tactic preference page 3 1 THE RODIN PLATFORM 19 E y e 7 lt Preferences changeMe amp DS m Prefix Settings MACHINE changeMe b General Customize Event B Pref
89. gluing cars cars go TRUE amp green cars_colors EVENTS Initialisation begin init5 cars_colors red 38 CHAPTER 2 TUTORIAL end END We also have to modify the guard on set_peds_green which is something that you should now be able to figure out yourself just replace cars_go FALSE with green cars_colors The interesting piece is the last event set_cars which we rename as set_cars_colors We change the parameter to new_value_colors and type it as a subset of COLORS The witness appears in the with section of the event The label must be new_value The value itself must describe the relationship between the abstract parameter new_value and the new parameter new_value_colors As we use the parameter as the new value for the variable cars_colors the witness is an adaptation of the gluing invariant we just replace cars_colors with new_value_colors O In most cases the witness is a slightly modified gluing invariant Here is the resulting event Event set_cars_colors refines set_cars any new _value_colors where grdi new_value_colors E COLORS grd2 green new_value_colors peds_colors red with new_value new_value TRUE gt green new_value_colors then acti cars_colors new_value_colors end Now you can get rid of the variable cars_go and its inisialisation clause and there will not be any errors or warnings But even though all proof obligations are now discharged we re not done yet
90. gly 4 3 11 How to create a Event B Component Please check the tutorial 2 4 1 to learn how to create a new Event B component 4 3 12 How to remove a Event B Component In order to remove a component press the right mouse button on the component In the context menu select Delete This component is removed from the Project Explorer CONTENT MIGRATED FROM WIKI CONTENT MIGRATED FROM WIKI 114 CHAPTER 4 FREQUENTLY ASKED QUESTIONS 4 3 13 How to save a Context or a Machine CONTENT MIGRATED FROM WIKI Once a machine or context is possibly partly only edited you can save it by using the save button as indicated in figure 4 3 File Edit Navigate Search 2 Prfsavefx 3 Obligat Figure 4 3 Save a context or a machine 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 3 1 6 This can take a certain time A Progress window can be opened at the bottom right of the screen to see which tools are working most of the time it is the auto prover 4 4 Proving 4 4 1 Help Proving is difficult Yes it is Check out Section 3 4 5 to get started with using the provers 4 4 2 How can I do a Proof by Induction This page about proof by induction will give you some starting tips 4 4 3 Labels of proof tree nodes explained ah means add hypothesis eh means rewrite with equality fr
91. green end Event set_peds_red refines set_peds_stop begin acti peds_colors red end Event set_cars refines set_cars any new _value where grdi new_value BOOL grd2 new_value TRUE peds_colors red then acti cars_go new _value end END 2 8 5 Witnesses The refinement of set_cars is more difficult since the event uses a parameter the new value for cars_go In order to refine it we need a witness 3 2 3 A witness is to an event s parameter what a gluing invariant is to a variable it is a mapping between the abstract parameter and the new parameter and allows the abstract parameter to disappear In this example the abstract parameter new_value is of type BOOL and we introduce a new parameter new_value_colors of type COLORS The naming of a witnesses label is mandatory and must be the name of the abstract parameter In our example the label must be new_value Let s get started We first provide the new variable gluing invariant typing invariant and initialization as we have done before at this point you can also rename the gluing invariant from the last section as gluing_peds in order to be able to determine between the two gluing invariants Note that the traffic light for the cars can show more than one color at a time Therefore the variable contains a set of colors instead of just one color as modelled for PEDS_COLORS a VARIABLES cars_colors INVARIANTS inv5 cars_colors C COLORS
92. gt 0j Np e ve Zan 1 a b n nE ZAa lt cnAn lt b Z P Z N P Z N P Z P Z with ae ZandbeZ Arithmetic operations E k mod mod Description Definition Types Addition Subtraction or unary minus Multiplication Integer division Modulo These are the usual arithmetic operations Addition subtraction and multiplication behave as expected The division is defined in a way that 1 2 0 and 1 2 Q a b max c cENAb c lt a foraeNandbEeN a b a b a b a b TODO Take the definition from Matthias paper TODO The same for modulo With a Z b Z and for each operator LJ of mod allbeZ a E Z 3 3 MATHEMATICAL NOTATION 99 WD a b L a A L b a b L a A L b Ab40 L a modb L a AL b Aa lt 0 AbF OD TODO Notation is actually implemented in Rodin Is D still interesting Or should we use something like the domain condition DOM because it s simpler for operators 3 3 5 Assignments In the previous sections we did not consider the scope of the expressions I e we did not say which constants or variables can be used in an expression or predicate because this depends completely on the context where the expression is used The following paragraphs are about assignments Depending on the type of assignment it may be im portant to specify which identifiers can be used Thus we us
93. h an apple and orange we can write apples N oranges Y This can be expressed shorter by saying that apples and oranges constitute a partition of the fruits partition FRUITS apples oranges In general we can use the partition operator to express that a set S is partitioned by the sets s S with partition S s1 Sn We use partitions in Section 2 6 2 Another typical usage for user defined data types are enumerated sets These are sets where we know all the elements already Let s take a system which can be either working or broken We model this by introducing a type STATUS in the SETS section and two constants working and broken We define that STATUS consists of exactly working and broken by STATUS working broken Additionally we have to say that working and broken are not the same by working broken If the enumerated sets gets larger we need to state for every two element of the set that they are distinct Thus for a set of 10 constants we ll need 10 10 2 45 predicates Again we can use the partition operator to express this in a more concise way partition STATUS working broken 2 5 5 Relations Relations are a powerful instrument when modeling systems From a mathematical point of view a relation is just a set of pairs Formally when we have to sets A and B we can specify that r is a relation between both by r P A x B ASCII r POW A B Because relations are so common we can write i
94. he view The Smiley The smiley can be one of three different colors 1 red indicates that the proof tree contains one or more undischarged sequents 2 blue indicates that all undischarged sequents of the proof tree have been reviewed 3 green indicates that all sequents of the proof tree are discharged The Editing Area The editing area allows the user to supply parameters for proof commands For example when the user attempts to add a new hypothesis by clicking on the ah button the new hypothesis should have been written by the user in the editing area ML PP and Hypotheses 3 1 THE RODIN PLATFORM 13 ML ML mono lemma prover appears in the drop down list under the button pp as MO M1 M2 M3 and ML The different configuration e g MO refer to the proof force of the ML prover All hypotheses are passed to ML PP PP predicate prover appears in the drop down list under the button pp as PO P1 PP e PO uses all selected hypotheses the ones in Selected Hypotheses window e Pl performs a lasoo operation on the selected hypotheses and the goal and uses the resulting hypotheses e PP uses all hypotheses 3 1 6 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 fi
95. help system The advantage of using dynamic help is that it allows to display the help page side by side with the other views and editors To start the dynamic help click Help Dynamic Help then click All Topics and select the page in the tree 4 3 MODELING 111 4 2 5 Rodin and eclipse doesn t take into account the MOZILLA _FIVE_HOME environment variable You have to add a properties by appending the following code to your eclipse eclipse ini or rodin rodin ini file Dorg eclipse swt browser XULRunnerPath usr 1ib xulrunner xulrunner xxx 4 2 6 No More Handles On Windows platforms it may happen that Rodin crashes complaining about no more handles This is an OS specific limitation described here and there A workaround is provided in this site 4 2 7 Software installation fails When installing softwares from update sites Help Install New Software it sometimes fails with an error saying something like No repository found containing osgi bundle org eclipse emf compare 1 0 1 v200909161031 No repository found containing osgi bundle org eclipse emf compare diff 1 0 1 v200909161031 This is an eclipse p2 bug referenced here The workaround is to e Go to Window Preferences Install Update Available Software Sites e Remove all sites then add them back again which can be achieved in the Available Software Sites preference page by e Select all update sites by highlighting them all those that are check
96. ion Simulation t d SIM t is the concrete event name d is SSO tne abetract action name Equality of a preserved Variable t v EQL t is the concrete event name v is This table shows the proof obligations concerned with the new events variant Well definedness of Variant wb Finiteness for a set Variant FINO Finally this table shows are the proof obligations concerned with witnesses Well definedness of Witness t p WWD t is the concrete event name p is parameter name or a primed variable name Feasibility of non det Witness t p WFIS t is the concrete event name p is parameter name or a primed variable name Remark At the moment the proof obligation generation for deadlock freeness is missing If you need it you can generate it yourself as a derived invariant by saying that the disjunction of the abstract guards imply the disjunction of the concrete guards 3 2 5 Visibility of identifiers This table shows which identifiers can be used in predicates or expressions Sets Sets that are defined in the context in case of an axiom or in a seen context If a context extends another context the sets of the extended context are treated as if they are defined in the extending context Constants Like the sets constants that are defined in the context in case of an axiom or in a seen context Concrete Variables Variables that are defined in the machine itself This does not include variables of
97. ion is usually located in the wiki 1 13 Feedback All online versions of the handbook contain a button or link for feedback Work on the handbook continues at least until January 2012 so your feedback will be read and will help to improve this handbook You can also submit feedback via email to rodin handbook formalmind com 1 2 Foreword It would be nice to recruit somebody for the foreword maybe Cliff and or Jean Raymond 1 3 Conventions We use the following conventions in this manual Checklists and Milestones are designated with tick Here we summarize what we want to learn or should have learned so far wy Useful information and tricks are designated by the information sign A Potential problems and warnings are designated by a warning sign A Examples and Code are designated by a pencil We use typewriter font for file names and directories We use sans serif font for GUI elements like menus and buttons Menu actions are depicted by a chain of elements separated by e g File New Event B Component 1 4 Acknowledgements The content of this handbook has grown over many years since the formation of the European Union IST Project RODIN in 2004 Giving credit to every contributor is almost impossible attempting to do so would almost certainly omit some people which is not in the spirit of this work It should suffice to say that we extend our gratitude to all contributors to the Rodin Wiki 1 1 2 In partic
98. ior must correspond to any machines that it refines Refinement and Abstract machines A machine can only refine one other machine We refer to the refined machine as the abstract machine and refer to the refinement as the concrete machine More generally a machine My can be refined by machine M M refined by M and so on The most concrete refinement would be Mn Basically a refinement consists of two aspects 1 The concrete machine s state is connected to the state of the abstract machine To do this an invariant is used to relate abstract and concrete variable This invariant is called a gluing invariant 2 Each abstract event can be refined by one or more concrete events The full invariant of the machine contists of both abstract and concrete invariants The invariants are accumulated during refinements wy How to use Refinement Refinement can be used to subsequently add complexity to the model this is called superposition refinement or horizontal refinement It can also be used to add detail to data structures this is called data refinement or vertical refinement We ve seen both types of refinement in the tutorial Chapter 2 Seeing a context If the machine sees a context the sets and constants declared in the context can be used in all predicates and expressions The conjunction of axioms A c can be used as hypotheses in the proofs Variables and invariants Variables can be declared by adding the
99. iption A Resource Path Lia W393 ss amp C GC mos ee A H te e OA CC e ll 44 nt 6 M NIN Pl n O items selected Event B Explorer Rodin Problems View Symbols View Figure 2 2 Rodin GUI 2 3 2 Install new plugins This sections shows how to install new plugins for Rodin by using the example of the Atelier B Provers plugin 3 4 4 It is highly recommended to install this plugin because without it we will not be able to prove anything Open the Install Manager Help Install New Software Click the downward arrow next to the field Work with to select the Atelier B Provers update site Mark the Atelier B Provers entry and click on the Next button compare with figure 2 3 Follow the installation instruction to install the plugin After installing the plugin you will be asked to restart Rodin in order to finalize the installation 2 4 The First Machine A Traffic Light Controller v Goals The objective of this section is to get acquainted with the modeling environment We will create a very simple model consisting of just one file to develop a feeling for Rodin and Event B In this tutorial we will create a model of a traffic light controller We will use this example repeatedly in subsequent sections Figure 2 4 depicts what we are trying to achieve In this section we will implement a simplified controller with the following characteristics e We model the signals with boolean values to indicated stop fa
100. ir unique name an identifier to the Variables section The invariants of the machine must make the type of the variable clear We denote the variables of the abstract machines Mi M 1 with a v and the variables of the concrete machine with a w An invariant is a statement that must hold at each state of the machine Each invariant 7 consists of a label and a predicate J c v w An invariant can refer to the constants as well as the variables of the concrete and all abstract machines We write I c v w to denote the conjunction of all invariants of the machine and all its abstract machines We call this the invariant of the machine An invariant lipm c v w can be marked as a theorem In this case the following proof obligation is generated An invariant as theorem Name label THM Goal A c A I c v w gt Lipm C V W 3 2 EVENT B MODELING NOTATION 87 where J denotes the conjunction of all invariants declared in abstract machines and all invariants declared in the concrete machine before the theorem in question Invariants that are marked as theorems derive their correctness from the preservation of other invariants see below for details so their preservation does not need to be proven If an invariant J contains a well definedness condition the following proof obligation is generated Well definedness of an invariant Name label WD Goal A c A c v w gt L 1 c v w Common variables between m
101. isation extended begin init_button button FALSE end Event push_button when grd peds_colors red then act button TRUE end END Now we need to integrate the push button with the traffic light logic e Upon pressing the button the pedestrians must eventually get a green light e At some point the button variable must be reset As we will see in the following discussion this be more tricky than it first appears For now we will introduce a guard preventing the car lights from turning green when button is true and we will reset the button when the pedestrian lights turn red Event set_peds_red extends set_peds_red begin act_button button FALSE end 2 9 PROVING 41 Event set_cars_colors extends set_cars_colors where grd_button cars_colors red A button TRUE end 2 8 9 Discussion There are a number of problems associated with the model in its current state Let s start with the resetting of the button The way we built our model so far set_peds_red can be triggered any time there is not a single guard which prevents this Therefore the button could be reset any time without the pedestrian light ever turning green This could be prevented with additional guards For instance the traffic ight events could require an actual change in the light s status This in turn could lead to deadlocks But even if we introduce such guards we could get stuck in a situation where cars would never get gre
102. ivalent to B C A P 4 ASCII POW1 A is the set of all non empty subsets of A 2 5 4 Introducing user defined types We can introduce our own new types simply by giving such types a name This is done by adding the name of the type to the SETS section of a context We will see how this is done in practice in the next section For instance if we want to model different kind of fruits in our model we might add FRUITS to our sets Then the identifier FRUITS denotes the set of all elements of this type Nothing more is known about FRUITS unless we add further axioms In particular we do not know the cardinality of the set or even if it is finite A Assume that we want to model apples and oranges which are sub sets of FRUITS We do not need not introduce them in the SETS section of a context just because they are sets Let s imagine such a scenario where apples and oranges are modeled as types of their own by declaring them in the SETS section And we have two variables or constants a and o with a apples and o oranges Then we cannot compare a and o with a o or a o That would raise a type error because and expect the same type for the left and right expression If we want to model sub sets apples and oranges as described above we can add them as constants and state apples C FRUITS and oranges C FRUITS If apples and oranges are all fruits we want to model we can assume apples U oranges FRUITS and if no fruit is bot
103. ixes b BMotion Studio Configure project specific settings gt REFINES v Event B Context prefixes b Appearance Event B Carrier Set set gt SEES Y Modelling UI Event B Constant cst gt VARIABLES cal Event B Axiom axm o Machine Editor sa a ae Proving UI Event B Action eri sgue Event B Event lt INVARIANTS Event B Invariant invariant ec b Install Update bwa b Q linvariantl L PES A S pm gt VARIANT Event B Variable variable Restore Defaults Apply TE Rodin Problems X E f gs i ce a 0 errors 0 warnings 0 infos Description Figure 3 39 Prefix Settings The buttons 1 and 2 are activating deactivating the automatic use of auto and post tactics Here you can also choose the profile that should be used for auto and post tactics Note that there is always a profile selected and this profile can be changed regardless of whether the tactics are automatically launched or not because there is always a way to manually launch auto and post tactics On the previously references figure the Default Auto Tactic Profile is used for the automatic tactic and the Default Post Tactic Profile is used for the post tactic Preferences for available profiles This section describes the Profile tab of the Auto Post Tactic preference page Figure 3 42 shows the contents of the profile tab There are two visible lists a list of profiles on the left and the tactics or provers that co
104. latform File Edit Navigate Search Project Run ProB Window Help Civ O Events Checksy Tew Ow How Event Paramel P set peds go P set_peds sto pi P set_cars x2 TRUE ar 2 mac giv to T Cars go peds go Formulas invariants 23 set peds go set_coars INITIALISATION uninitiolised state vs cars_go TRUE a peds go TRUE v cars go TRUE a peds go TRUE Y cars go TRUE cars go TRUE v peds go TRUE oT peds go TRUE guards P 13 CruiseControl e 13 Paper gt 12 Paper TL e 3 Sandbox e Traceability gt 5 Trafficlight Figure 2 10 An invariant violation found by ProB The simplest predicates are T ASCII true and L ASCII false We can also check whether arbitrary objects of the same type are equal with or ASCII Predicates can be combined with the usual logical operators symbol ASCII conjunction and amp disjunction or V or implication gt gt equivalence lt gt negation not z not We can use universal quantification to express a statement that should hold for all possible values a variable might have For example in order to show that any given number x greater than zero and multiplied with two is greater than one we can use the following expression Vex gt 0 gt 2x gt 1 ASCII ix x gt 0 gt 2 x gt 1 When a variable is introduced by a qu
105. lied from the top to the bottom The user can choose a tactic from the list on the left and hit the gt gt button to select it or unselect some tactics from the list of the right using the lt lt button The user can re order the priority of the selected tactic using the Up and Down button By clicking on Finish the profile will be saved and available for use in the auto and post tactics Project specific settings The user can select profiles locally for each project To do so select the Auto Post Tactic property page available via right click on a project and select the Properties item or click the Configure project specific settings link on the Auto Post Tactic preference page Figure 3 44 shows what this Auto Post Tactic tab looks like Note that the enablement of automatic use of post and auto tactics is decided at the workspace level Figure 3 45 shows the Profiles tab of the Auto Post Tactic page for a project specific setting At the project level there is a contextual menu available via right click from the list of defined profiles This contextual menu offers two options to the user e Import Workspace Profiles retrieve all the defined profiles in the workspace e Export to Workspace Profiles push a selected profile up in the list of workspace profiles Preferences for the automatic tactics Introduction The purpose of this section is to give a more detailed preferences to the user so he can b
106. lse and go true We do not model colors yet e We do not model the push button yet 16 CHAPTER 2 TUTORIAL Install Available Software Check the items that you wish to install Work with Atelier B Provers http bmethod com update_ site atelierb provers v Add Find more software by working with the Available Software Sites preferences type filter text Name Version Bu Atelier B Provers 42 Atelier B provers Select All Deselect All 1 item selected pte Atelier B Provers 1 0 0 7 757CcL5g6h Show only the latest versions of available software O Hide items that are already installed Y Group items by category What is already installed Y Contact all update sites during install to find required software lt Back Next gt Cancel Finish Figure 2 3 Eclipse Install Manager Figure 2 4 The traffic light controller 2 4 1 Project Setup Models typically consist of multiple files that are managed in a project Create a new Event B Project File New Event B Project Give the project the name tutorial 03 as shown in figure 2 5 2 4 THE FIRST MACHINE A TRAFFIC LIGHT CONTROLLER 17 New Event B Project This wizard creates a new empty Event B Project in the current Workspace Project name tutorial 03 O Add project to working sets Working set cancel Figure 2 5 New Event B Project Wizard Eclipse supports different types of projects The proj
107. lugins is maintained in the Rodin Wiki 1 1 2 2 2 6 Eclipse Rodin is based on the Eclipse Platform 3 1 1 a Java based platform for building software tools This matters for two reasons e If you have already used Eclipse based software then you will feel immediately comfortable with the handling of the Rodin application e Many extensions or plugins are available for Eclipse based software There are Rodin specific plugins as well as Rodin independent plugins that may be useful to you The Rodin Wiki 1 1 2 contains a list of plugins is maintained The GUI of an Eclipse application consists of Views Editors Toolbars Quickview Perspectives and many more elements If these terms are unfamiliar to you please consult Section 3 1 1 which contains references to Eclipse tutorials In Section 2 3 we present the Rodin specific GUI elements 2 3 Installation Goals The objective of this section is to guide you through downloading installing and starting Rodin In addition we explain the update mechanisms needed to install new plugins for Rodin Finally we name the Rodin specific GUI elements and describe their functions v You can skip this section if e you know how to install and update Rodin e you know how to install new plugins for Rodin Before installing Rodin you should ensure that your computer fulfills the system requirements The system requirements for the present release can be found in the Rodin Wiki
108. ment down by selecting it and then pressing one of the two arrows T or E It is also possible to add modelling elements by using wizards You can active the different wizard by using the buttons in the tool bar as shown in Figure 3 12 and in Figure 3 13 or via the Event B menu keeping in mind that the wizards depend on the active file machine or context The next sections explain how to use the wizards Event B Celebrity Celebrity c File Edit Navigate Search Project Run Rename Event B ProB Window Help Figure 3 12 Wizards for context specific elements located in the tool bar Event B Celebrity Celebrity 0 File Edit Navigate Search Project Run Rename Event B ProB Window Help ri meala E Event B Explorer 0 10 ctx Celebrity_cO eral ar A 7 Figure 3 13 Wizards for machine specific elements located in the tool bar 3 1 THE RODIN PLATFORM 61 New Carrier Sets Wizard ate To activate the New Carrier Sets Wizard press the gt button located in the tool bar Pressing the button bring up the window shown in figure 3 14 New Carrier Sets Identifier E53 Identifier Identifier woe coma ox Figure 3 14 New Carrier Sets Wizard You can enter as many carrier sets as you want by pressing the More button When you are finished press the OK button New Enumerated Set Wizard te To activate the New Enumerated Set Wizard press the button located in the tool bar Pressing the but
109. mpose these profiles Profile Details Here one can see the contents of the default Auto Tactic Profile There are 4 buttons available to the user e New to create a new profile from scratch e Edit to edit an existing editable profile e Remove to remove a profile definitively e Duplicate to duplicate a selected profile for further slight modification Default profiles can not be edited nor removed That is why they this option appears in gray on the previously referenced figure 80 CHAPTER 3 REFERENCE Properties for Celebrity X type filter text amp Prefix Settings Br ay w Resource E Enable project specific settings Auto Post Tactic Context prefixes Builders Event B Carrier Set set Prefix Setti ON e Project References Event B Axiom axm Refactoring History Run Debug Settings Machine prefixes Event B Action fact Event B Event evt Event B Invariant invariant Event B Guard grd Event B Witness wit Event B Event Parameter prm Event B Variable variable Restore Defaults Apply 2 ane oe Figure 3 40 Project specific prefix settings Figure 3 43 shows the dialog available to edit or create a profile For instance here we create a profile named MyFirstTacticProfile The list on the right represents the available and unselected tactics The list of the left displays the profile contents and shows the selected tactics that will be app
110. n the Event B mathematical language description Based on the domain conditions we associate with each term or formula E a well definedness condition D E respectively Well definedness conditions are formulae as follows x ranges over variables f over operators p over predicates t over sequences of terms of length t and over formulae All terms and formulae are well formed and well typed 3 2 EVENT B MODELING NOTATION 93 Ie D x S T D f t DOM F t ANA D ti Dz 0 Va D 9 D p t AL Dlt D T D L T Dad D d D GAW D S AD V D A gt V DW AW PVY D AD 6 V PIA A V D Y Av PCO gt 4 E DIE A PW V DIO A V D H Mb Dl 4 4 DO ADH D VI p Va D V Gxr D A D 3x p Va D V E22 D H A A constant c is an operator of arity zero and therefore has the well definedness condition DOM c which equals T for all currently supported constants Intuitively the well definedness condition of a term or formula is true if and only if the term or formula can be evaluated without applying an operator to an argument outside of its domain Well Definedness and Provability Recall that the set of provable sequents is the smallest set of sequents such that if all antecedents of some inference rule are provable then so is the consequent See Inference Rules and All Rewrite Rules for an incomplete list of rules that may be used to prove a sequent Here w
111. nally the Auto Tactic button This yields the window in figure 3 31 i gt Preferences alx ype filter text Auto Tactic or b General Preferences for the Automatic Tactic gt Event B Enable auto tactic for proving gt Help Tactics are run as auto tactics b Install Update True Goal Discharge B4free P1 Discharge b Run Debug Goal in Hypotheses Discharge B4free PP Discharge Y Sequent Prover Functional Goal Discharge Find Contradictory Hypotheses Simplify B4free ML Discharge PP restricted Discharge Post Tactic B4free PO Discharge PP after lasoo Discharge gt Team Use Equals Hypotheses Simplify Shrink Implicative Hypotheses Simplify Type Rewriter Simplify PP unrestricted Discharge Simplification Rewriter Simplify False Hypothesis Discharge Clarify Goal Mixed Restore Defaults Apply Figure 3 31 Auto Prover Preferences 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 The Search Hypotheses View ma By typing a string in the Proof Control view and pressing the Search Hypotheses 1 button a window is provided which contains all the hypotheses that have a character string in common with the one entered by the user in the e
112. ng Perspective is not visible as a tab on the top right hand corner of the main interface the user can switch to it via Window Open Perspective The Proving Perspective consists of a number of views the Proof Tree the Goal the Selected Hypotheses the Proof Control the Search Hypotheses the Cache Hypotheses and the Proof Information In the discussion that follows we look at each of these views individually Figure 3 25 shows an overview of the Proving Perspective 3 1 THE RODIN PLATFORM 67 Menu bar Tool bar Name of PO Selected Hyptotheses Event B mest ae Soe Celebrity Celebrity 1 bps Rodin Platform pes Be tos Help pr TS ta E E File Y Navigate Search P ES Proving ce v simplification rewrites em 0 ceQ y Jo cat ce v p Celebrity_1 O ot xeQ gt o Varifbles O ct yea b Invg gants Cl et 7x yek b Events Oct 7 xy Y Proof Obligations Selected Hypotheses G INITIALISATION inv G INITIALISATION inv Sool celebrity act1 SIM ct ced Y y G remove_1 inv1 INV Q remove Vinv2 1NV A Proof Control 23 5 Statistics 2 Rodin Pfoblems Y 5 VA Symbols EN 0 P po de ah ae y po pil m 2 oe Proof Tree Proof Control View Goal Symbols View Figure 3 25 Overview of the Proving Perspective Loading a Proof To work on an PO that has not yet been discharged it is necessary to load the proof into the Proving
113. nicode character i e mathematical symbol Atomic Symbols Unary Operators EE asc Saal Powe Assignment Operators 3 4 PROVING 101 Binary Operators sabe pease a O i CN o ES E MR IET EI i a SO E AA E A IN IES CEN Multiple Operators Quantifiers TY I Typing O O oftype 3 4 Proving In Section 3 2 4 we learned what proof obligations are generated by Rodin from an Event B model We validate the model by discharging proof obligations This is what we call proving v In this chapter we will e Explain proof rules 102 CHAPTER 3 REFERENCE Explain tactics e Explain and describe provers Explain reasoners Describe how to perform automatic and manual proving e Purge proofs for maintenance 3 4 1 Sequents A sequent stands for something we want to prove Sequents are of the following form HFG where H is the set of hypotheses predicates and G is the goal a predicate in the mathematical language The meaning of the above sequent is that Under the hypotheses H prove the goal G 3 4 2 Proof Rules In its pure mathematical form a proof rule is a tool to perform formal proof and is denoted by A C where A is a possibly empty list of sequents the antecedents of the proof rule and C is a sequent the consequent of the rule We interpret the above proof rule as follows The combination of the proofs of each sequent of A prove the sequen
114. not been defined 4 3 5 What are type expressions in Event B ee 4 3 6 How can I create a new Event B Project 0 00022 4 3 7 How to remove a Event B Project o o 4 3 8 How to export a Event B Project o o 4 3 9 How to import a Event B Project e o 4 3 10 How to change the name of a Event B Project 0000 4 3 11 How to create a Event B Component 2 e a a e e a e a a a 4 3 12 How to remove a Event B Component 4 3 13 How to save a Context or a Machine e ELIO casonas TN EES Oo ERR AAA AA Helpi Provine icicle e s s teessa SE KE SEH EKO pr EEE RES S 442 How can Ido a Proot by Induction lt lt sas 5 jee 448 pedias prani a 4 4 3 Labels of proof tree nodes explained a a a a USES Cees wn he ee RRR ER CEE RR RR GES we Oe ee ee Hd 4 5 1 Where did the GUI window go 2 e e 4 5 2 Where vs When What s going on 2 aa Plug n Questions ce ek hh ee wee era aaa 113 113 CONTENTS Chapter 1 Introduction The Rodin documentation needs improvement This has been established at the Deploy Exec Meeting in 2010 We ve been collecting background information and the requirements in the Rodin Wiki What you see here is a working draft of the documentation We are grateful for any feedback that you may have 1 1 3 1 1 Overview
115. nt in this section The objective is to create a mapping between the abstract traffic light values and actual colors Figure 2 13 depicts our mapping for the traffic light For simplicity the traffic light for pedestrians consists of only two lights red and green We break this problem into two steps 1 Create a context with the data structures for the colors 34 CHAPTER 2 TUTORIAL Abstract Events Concrete Events Figure 2 13 Mapping between Abstract and Concrete Events 2 Create a refinement of the existing model that sees the new context and refines the boolean states into colors 2 8 2 A Context with Colors Start by creating a context called ctx1 as described in Section 2 6 We model the colors as constants A CONSTANTS red yellow green These constants are part of a set N sets COLORS And last we need to provide typing We do this by creating a partition a AXIOMS type partition COLORS red yellow green Please note the curly braces around the colors It s very easy to forget these which will result in typing errors that are very hard to interpret for a novice This completes the context 2 8 3 The Actual Data Refinement The easiest way to create a refinement is by right clicking on the machine in the project browser and selecting Refine in this case we will be refining the machine mac from the project tutorial 3 This will create a stub consisting of all variables and
116. nual installation of plug ins is described in Installing external plug ins manually 4 2 3 The builder takes too long Generally the builder spends most of its time attempting to prove POs There are basically two ways to get it out of the way e the first one is to disable the automated prover in the Preferences panel e the second one is to mark some PO as reviewed when you don t want the auto prover to attempt them anymore Note that if you disable the automated prover you always can run it later on some files by using the contextual menu in the event B Explorer To disable the automated prover open Rodin Preferences menu Window Preferences In the tree in the left hand panel select Event B Sequent Prover Auto tactic Then in the right hand panel ensure that the checkbox labelled Enable auto tactic for proving is disabled To review a proof obligation just open it in the interactive prover then click on the review button this is a round blue button with a R in the proof control toolbar The proof obligation should now labelled with the same icon in the event B explorer 4 2 4 What are the ASCII shortcuts for mathematical operators The ASCII shortcuts that can be used for entering mathematical operators are described in the help of the Rodin keyboard plug in In the help system this page has the following path Rodin Keyboard User Guide Getting Started Special Combos This page is also available in the dynamic
117. odels The text based Camille Editor 2 4 2 is very popular Please visit the Rodin Wiki 1 1 2 for the latest information 2 4 2 Camille a text based editor Y Camille is a real text editor that provides the same feel as a typical Eclipse text editor including Pr copy and paste undo redo etc However please note that at this time not all Rodin plugins are compatible with Camille Also please consult the extensive documentation in the Rodin Wiki A Camille can be installed via its update site which is preconfigured in Rodin Once installed Camille is made the default editor The structural editor can still be used by selecting it from the context menu of a file in the project browser For more information please visit http wiki event b org index php Text_Editor This contribution requires the Camille plugin The content is maintained by the plugin contributors and may be out of date 2 4 3 Building the Model Back to the problem Our objective is to build a simplified traffic light controller as described in 2 4 We start with the model state Two traffic lights will be modelled and we will therefore create two variables called cars_go and peds_go Go to the Edit tab in the editor and expand the VARIABLES section Click on the green plus sign to create a new variable Creating Variables You will see two fields The left one is filled with the word vari Change this to cars_go The second field after the double sla
118. of obligation Choosing proofs to delete For the moment nothing has been erased The new window see figure 3 46 shows obsolete proofs and offers to choose among them which ones should be deleted One may wish to keep some of them knowing they might be useful in the future Once the selection has been decided clicking the Delete button will actually delete selected proofs from proof files Files becoming empty will be deleted as well Caution Proof purging shall not be performed on models that are not in a stable state For instance it should not be applied to a model that bears some errors or warnings issued by the type checker This is because in case of errors and warnings it can happen that not all proof obligations are generated Therefore some proofs could be considered wrongly as obsolete 108 CHAPTER 3 REFERENCE Proof Pureer Selection Select proofs to delete W plaf thmaTHM thma THM thm4 THM ths THM A plf thm THM F plouf E then LTH W thmaTHM ff then ay THM oF i PS F Cl Select All Deselect All Figure 3 46 Proof Purger Selection Window Chapter 4 Frequently Asked Questions 4 1 General Questions 4 1 1 What is Event B Event B is a formal method for system level modelling and analysis Key features of event B are the use of set theory as a modelling notation the use of refinement to represent systems at different abstraction levels and the use of m
119. olors red yellow gt new_value_colors green grd_g y cars_colors green gt new_value_colors yellow with new_value new_value TRUE gt green new_value_colors then 40 CHAPTER 2 TUTORIAL acti cars_colors new_value_colors end END 2 8 8 One more Refinement The Push Button We will demonstrate another application of refinement introducing new features into an existing model A typical traffic light system allows the pedestrians to request a light change by pressing a button We will introduce this feature in a new refinement We could have introduced the push button in the initial machine but introducing it later allows us to structure the model and makes it easier to understand and navigate We will realize this feature by introducing a new boolean variable for the push button We will introduce an event that notifies the model that a push button has been pressed Upon allowing the pedestrians to cross we will reset the push button As in the previous section we create a new refinement mac2 by right clicking on mac1 and selecting Refine A stub is generated that contains the events from the abstract machine We simply add a new variable for the push button including typing and an initialisation clause We also introduce an event that sets the button This event doesn t work while the pedestrians have a green light a VARIABLES button INVARIANTS type button button BOOL EVENTS Initial
120. om hypothesis from left to right he means rewrite with equality from hypothesis from right to left rv tells us that this goal has been manually reviewed sl ds means selection deselection PP means discharged by the predicate prover ML means discharged by the mono lemma prover 4 5 USAGE QUESTIONS 115 4 5 Usage Questions 4 5 1 Where did the GUI window go When you are looking for a particular view and the view does not appear or it appears in a different place than is usual try clicking on Window Reset Perspective This will reset the different views back to their default positions If you can t find menu buttons from one of the views try resizing the view in question to see if part of the menu has been hidden 4 5 2 Where vs When What s going on 4 6 Plug In Questions Index abstract machine 86 abstract machine notation 13 anticipated status 90 Atelier B provers 104 axiom 85 bijection 97 carrier set 85 Comment 18 Component 17 conjunction 96 constant 85 context 85 convergent status 90 disjunction 96 equivalence 96 event 87 Event B 13 false as predicate 1 96 feasibility of actions 89 of witnesses 88 function 97 gluing invariant 86 guard 88 implication 96 initialization 89 injection 97 invariant 86 machine 86 negation 96 ordinary status 90 parameter 87 Parameters 20 predicate logic 12 ProB 20 Project 16 project 53 proof rule
121. ook something up check the reference 3 and FAQ 4 of this handbook Online PDF and Eclipse Version of the Handbook There are three versions of this handbook You can access it directly through Rodin by using the built in help browser Help Help Contents The Eclipse Version is useful because it can be used offline Use the Rodin Wiki The Rodin Wiki 1 1 2 contains the latest news regarding Rodin and a wealth of information that is not in the scope of this handbook Be sure to check out it out Find useful Plugins There are many plugins available so be sure to check them out There is a good chance that they will make your life easier Subscribe to the mailing lists The wiki lists the existing mailing lists which include a list for users and for developers We strongly recommend subscribing to the announcement list Rodin in Industry If you are considering using Rodin in an industrial setting be sure to explore the testimonies from the Deploy 1 5 project in which industrial partners describe their experiences with Rodin We wish you success in your modeling projects Chapter 3 Reference 3 1 The Rodin Platform In this section we describe the details of the tool platform as it is presented to the user You will find a description of all GUI elements that you may encounter 3 1 1 Eclipse in General From the Eclipse Website Eclipse is an open source community whose projects are focused on building an open
122. orm in the Event B Explorer This is usually situated on the left hand side of the screen as shown in figure 3 3 The Event B Explorer contains a list of name of the current projects Next to each project name is a small triangle By pressing it one can expand a project and see the machines and contexts that it contains The icons respectively When expanding a machine or a context you can explore its elements Double clicking on a specific element i e a variable opens the Event B editor and marks the position of the variable in the machine or context as shown in figure 3 7 Furthermore proof obligations are displayed when clicking on the small triangle next to the label Proof Obligations for more information see section 3 1 5 or next to the components help identify whether they are a context or machine 3 1 3 Customizing a perspective suitable for RODIN So 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
123. ower set the set of all subsets of S Pairs If we have two terms we can construct a pair For example with 2 and TRUE we can construct the pair 2 TRUE ASCII 2 gt TRUE The type of that pair is Z x BOOL where x denotes the Cartesian product Set of pairs relations play an important role in modeling languages like Event B Please do not confuse predicates and Boolean values For example if you want to express the condition if the variable b is true x should be greater than 2 you cannot write b gt x gt 2 That would raise a syntax error Instead you can write b TRUE gt x gt 2 In the reference section TODO link to mathematical notation if the reference the types of each operator in Event B are described in detail 2 5 MATHEMATICAL NOTATION 25 2 5 3 Operations on Sets Let s assume that we have two sets A and B of the same type e g sets of integers Then we can check if an element e is in it by e A ASCII e A or on if it is not in A by e A ASCII e A Expressing that all elements of A are also elements of B i e A is a subset of B can be done by A C B ASCII A lt B The negated form is A Z B ASCII A lt B We can build the union AU B the intersection AN B and the set subtraction A B ASCII A B A B and A B The set subtraction contains all elements that are in A but not in B The power set P A ASCII POW A is the set of all subsets of A Thus B P A is equ
124. ox to indicate that the corresponding invariant should be a theorem New Event Wizard To activate the New Events Wizard press the E button located in the tool bar Pressing the button brings up the window shown in figure 3 20 You can then enter the events that 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 press the Add button Press the OK button when you re finished Note that an event with no guard is considered to the guard true Also an event with no action is considered to have the action skip 64 Label jet Guard label s gra1 gra2 grd3 Action label s fact1 fact2 fact3 CHAPTER 3 REFERENCE New Events Parameter identifier s Guard predicate s ees not theorem not theorem not theorem Action substitution s Add mMorepar mMoreGrd morea cancel ok Figure 3 20 New Event Wizard Dependencies Context By selecting the Dependencies tab at the bottom of the Event B editor you obtain the window as shown in figure 3 21 Sy O Celebrity o Abstract Contexts Select abstract contexts of this context Remove Dependencies Figure 3 21 Dependencies tab of the Event B editor 3 1 THE RODIN PLATFORM 65 The dependencies tab allows you to control what other contexts that the cu
125. 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 example 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 58 CHAPTER 3 REFERENCE Event B Celebrity Celebrity_0 bum Rodin Platform File Edit Navigate Search Project Run Rename Event B ProB Window Help b INITIALISATION b celebrity gt SEES inwl b Celebrity_cO Celebrity co gt Celebrity c1 gt VARIABLES EF gt Celebrity_0 ere v Variables o fr i er Pretty Print Synthesis Dependencies Dias El Rodin Problems 23 E Properties Tasks PD Y Symbols x b Events 0 errors 0 warnings 0 infos b Proof Obligations Pb
126. preservation includes the event as well as the invariant in question For instance in figure 3 33 the hyperlinks CreateToken and inv2 can be used to navigate to the containing machine 3 1 THE RODIN PLATFORM 19 1 Proof Information 3 E CreateToken inv INV e Event in M2 CreateToken ANY u r t WHERE grdl u e User 4 ranfutok grd2 r Room grd3 t e Token tok grd4 act ir authliu THEN actl tok tok u t act2 utok utok u teu act3 rtok rtok u iter END e Invariant in Me inv2 utok e tok gt User Figure 3 33 Proof Information View Rule Details View This view displays the information relating to a given proof tree node onto which a rule was applied A command is available when right clicking on a proof tree node in order to reveal the Rule Details view See figure 3 34 T goz Copy simpl aa 30 fd 6 Prune LO Show details y 0 sl ds Figure 3 34 Open Rule Details View By default this view is a fast view If the window does not appear seek the button identified by the view s icon at the bottom left of the workbench to make this view visible Figure 3 35 gives an overview of the Rule Details View A quick summary of the applied rule contents is provided In this figure we display the contents of the rule named Y hyp mp where an input has been used to instantiate an hypothesis One can quickly see the input that was used to instantiate the rule the line below Rul
127. r machine that extends or sees the contexts it makes no difference where a constant or axiom is declared Extending two contexts which declare a constant or set using the same identifier will result in an error Constants and axioms Constants can be declared by adding their unique name an identifier to the Constants section An axiom must also be in place from which the type of the constant can be inferred We denote the sequence of all constants with c An axiom is a statement that is assumed as true in the rest of the model Each axiom consists of a label and a predicate A c An axiom Aihm can be marked as a theorem In that case the following proof obligation is created Proof obligation of a theorem Name label THM Goal Asc gt Atnm c where A denotes the conjunction of all axioms declared in extended contexts and the axioms already declared in the current context before the theorem in question If an axiom A contains any condition that is well defined a proof obligation is generated 86 CHAPTER 3 REFERENCE Well definedness of an axiom Name label WD Goal Asc L A c 3 2 3 Machines A machine describes the dynamic behavior of a model by means of variables whose values are changed by events There are two basic things that must be proven for a machine 1 The machine must be consistent i e it should never reach a state which violates the invariant 2 The machine is a correct refinement i e its behav
128. ract event PASS of its predecessor To prove this we would have to prove that the guard of the abstract event implies that of the concrete event The issue is that this condition cannot be verified in general Moreover the failure to prove the above condition indicates that there are possibilities that certain people could stay permanently blocked in locations People are also more limited in the ways that they may move because they can only move between rooms that are connected Now we know that this model contains a problem ignored in the document requrements We must now find a sufficient solution wy Please note that post tactics should still be disabled before starting this part of the tutorial At the beginning of this section we need to come back to the Event B Perspective As described in section 2 10 1 open door_1 machine and add a derived invariant theorem called DLF as follows INVARIANTS DLF Jq m q gt m E aut A sit q gt m com Save the file Once again the prover fails to prove the deadlock freeness automatically Actually all we want to prove is that any person authorized to be in a location must also be authorized to go in another location which communicates with the first one This can be illustrated as demonstrated in figure 2 24 To begin with switch over to the proving perspective and double click on DLF THM to begin proving At the beginning of the proof there aren t any selected hypothesis
129. re 2 22 You see that it is automatically instantiated It leads to the selected hypothesis x P We can now instantiate p in the goal with x enter x in the yellow box corresponding to p in the Goal View and click on the existential quantifier as shown in Figure 2 23 Ml O O et 3x xeP Selected Hypotheses Figure 2 22 Click on the existential quantifier in order to Y Goal z a ed Y E p leaut A P x foutside p xl Figure 2 23 TODO Description A If the hypothesis does not appear immediately in the Selected Hypothesis view reclick on the Auto Prover button until it does Now needs to be instantiated In order to instantiate it we need a case distinction Type sit x 1 into the Proof Control View and click on Case Distinction button dc to look at the two cases sit x l and sitlx l Before starting with the cases the prover now wants you to prove that x dom sit This can be done with the p0 prover since sit is a total function In the first case x is situated in I so it cannot be in outside You can instantiate with outside type outside in the box corresponding to and click on the existential quantifier In order to prove that x is allowed outside you will need to select the hypothesis P x outside C aut if this hypothesis doesn t appear in the search hypothesis type outside in the proof control view click on the Search Hypothesis button and add it to the selected hypothesis using
130. re it comes from There are two kind of proof obligations generated in a context e Each theorem must be proven The proof obligation s name has the form label THM where label is the theorem s label e Some expressions are not obviously well defined E g the axiom x y gt 2 is only meaningful if y is different from 0 Thus Rodin generates the proof obligation y 0 A well defined proof obligation has the name label WD The order of the axioms and theorems matter because the proof of a theorem or the degree to which an expression is well definded may depend on the axioms and theorems that are already written This is necessary to avoid circular reasoning 2 7 2 Machines A machine describes the dynamic behavior of a model by means of variables whose values are are changed by events A central aspect of modeling a machine is to prove that the machine never reaches an invalid state i e the variables always have values that satisfy the invariant First we briefly summarize of which parts a machine consists Refines Optionally a machine can refine another one We ll see in 2 7 4 what that means Sees We can use the context s sets constants and axioms in a machine by declaring it in the Sees section The axioms can be used in every proof in the machine as hypothesis Variables The variables values are determined by an initialization and can be changed by events Together they constitute the state of the machine Each vari
131. reference is activated Auto tactic will then run after each proof step and post tactic will run after each step and rebuild Post tactics and auto tactics only need to be activated in order to run automatically see previous sections on how to activate auto and post tactic The user can separately define tactic profiles and assign them to post and auto tactics Therefore there are two tabs in the Auto Post Tactic preference page for each of these choices These tabs will be described in section 3 1 7 3 1 7 Preferences Rodin provides several options to set preferences the Event B editor You can access the preferences via Window Preferences Event B in the menu bar The following subsections describe the different preference option Appearance This section provides settings for the Event B editor appearance Colors and Fonts The color and fonts preference page allows you to set the text and comment color of the Event B editor Furthermore it allows to toggle on or off the borders of the different fields in the Event B editor Figure 3 38 shows the Colors and Fonts preference page Context and Machine Editor The context and machine editor preference pages allows you to customize the visible tabs of the context and machine editor Prefix Settings This page describes the mechanism used to set element prefixes and perform renaming using dedicated actions for both machines and contexts Note that prefixes are used for automatic ren
132. required hypotheses that have been missing Do some case splits Instantiate quantifiers Apply ae abstract expression to replace complicated expressions by fresh variables You can also apply one of the automatic provers They may be more successful than the auto tactic because they have a longer timeout Try New PP before PP or ML because New PP proofs can be better reused if the model changes The configurations that act on more than the selected hypotheses New PP after lasso and unre stricted P1 and PP ML become useless when the model grows When everything fails start to unfold the proof obligation manually by clicking on the red links 3 4 PROVING 107 You may discover that some assumption was missing You may complete the proof If you observe that a valid proof obligation cannot be proved manually please send a bug report Rodin Bug Tracker 3 4 6 Reasoners Reasoners apply on the sequent of a given proof tree node and is a way to contribute to the provers They are typically not of direct interest to the user but to the developer A reasoner is and has to be quite rough it shall take a given sequent and produce a proof rule that will if possible apply on this given sequent whereas a tactic could be smarter Indeed a tactic can involve several reasoners thus apply them in loops and combine them or even call other tactics 3 4 7 Purging Proofs Proofs
133. rrent context is extending To add the context that you want to extend select the name of the context from the drop down menu at the bottom of the window and then hit the Add button There is also another way to create a new context as an extension existing one Select the context in the project window and then press the right mouse key Then select Extend from the menu that opens up This should bring up the window as shown in figure 3 22 New EXTENDS Clause Please enter the name of the new context zz caca J Figure 3 22 New EXTENDS Clause window You can then enter the name of the new context which will automatically extend your chosen context Dependencies Machine The Dependencies tab for machines is very similar to the one for contexts that is described in the previous section The main difference is that there are two kinds of dependencies that can be established machines on which the current machine depends are listed in the upper part and contexts on which the current machine depends are listed in the lower part Synthesis Context Selecting the Synthesis tab brings up a global view of your context s elements carrier set constant axiom extended context as demonstrated in Figure 3 23 By pressing the set cst or axm buttons in the upper right corner you can filter out the carrier sets constants or axioms of your context respectively If you select an element you can change its priority by pressing the
134. rtain properties of the modeled system We will explain here which proof obligations are generated and we will list the goal and hypotheses that can be used when performing the proof for each one This is done in the form 84 CHAPTER 3 REFERENCE o Properties for NewProject Auto Post Tactic O Auto Post Tactic Customize Event B Tactics Enable project specific settings Auto Post Tactic Profiles Auto Tactics Tactic profile to be used for auto tactics Default Auto Tactic Profile w Post Tactics Tactic profile to be used for post tactics Default Post Tactic Profile x Restore Defaults r Apply f Cancel OK Figure 3 44 Auto Post Tactic Tab for project specific settings for Auto Post Tactic Properties For NewProject Auto Post Tactic Auto Post Tactic Auto Post Tactic Customize Event B Tactics Enable project specific settings Profiles Profile Details Default Auto Tactic Profile Default Post Tactic Profile MyFirstProjectSpecificProfile Atelier B ML Discharge Atelier B PO Discharge Atelier R P1 Discharge Edit Import Workspace Profiles New e Remove False Hypothesis Discharge Duplicate Restore Defaults Apply Cancel OK Figure 3 45 Profiles Tab for project specific settings for Auto Post Tactic Name Goal Hypotheses Description Label of the proof obligation label refers to the label of the
135. s using the check boxes and press the E button Adding these hypotheses to the selected hypotheses means that they will be visible to the prover They can then be used during the next interactive proof phase To remove hypotheses from the Search Hypotheses window use the o button This button also appears above the selected hypotheses and allows the user to remove any hypothesis from the Selected Hypotheses window The other button situated to the left each hypotheses is the et button Clicking on this will attempt a proof by contradiction The effect is the same as if the hypothesis were in the Selected Hypotheses window The Cache Hypotheses Window This window allows the user to keep track of recently manipulated i e used removed or selected hypotheses for any PO For example when the user applies a rewrite to a hypothesis a new hypothesis after the rewriting is selected and the original hypothesis is deselected and put in the Cache Hypotheses window Similar operations to that of the Selected Hypotheses and Search Hypotheses windows such as removing selecting and proof by contradiction ct are also available for the cached hypotheses Interactive proof steps e g rewriting can also be carried out from the Cache Hypotheses window Proof Information View This view displays information so that the user can relate a proof obligation to the model For example typical information for an event invariant
136. s methods and tools together with the necessary further research on methods and tools 1 6 Creative Commons Legal Code The work presented here is the result of an collaborative effort that took many years To ensure that access to this work stays free and to avoid any legal ambiguities we decided to formally lincense it under the Creative Commons Share Alike License This work is licensed under the Creative Commons Attribution ShareAlike 3 0 Unported License To view a copy of this license visit http creativecommons org licenses by sa 3 0 or send a letter to Creative Commons 444 Castro Street Suite 900 Mountain View California 94041 USA 3http www deploy project eu 10 CHAPTER 1 INTRODUCTION Chapter 2 Tutorial The objective is to get you to a stage where you can use Rodin and build Event B models We expect you to have a basic understanding of logic and an idea why doing formal modeling is a good idea You should be able to work through the tutorial with no or little outside help This tutorial covers installation and configuration of Rodin it brings you through step by step through building formal models and it provides the essential theory and provides pointers to more information We attempt to alternate between theory and practical application thereby keeping you motivated We encourage you not to download solutions to the examples but instead to actively build them up yourself as the tutorial progresses If
137. sh is a comment field in which you can write any necessary notes or explanations 1 Comments The comment field supports line breaks Note that it is not possible to comment out parts of the model as you would expect in any programming language You can use the comment field to park predicates and other strings temporarily Create the second variable peds_go in the same way Upon saving the variables will be highlighted in red indicating an error as shown in figure 2 7 The Rodin Problems view shows corresponding error messages In this case the error message is Variable cars_go does not have a type Types are provided by invariants Expand the INVARIANTS section and add two elements by following the same steps as above Invariants have labels Default labels are generated invi and inv2 The actual invariant is prepopulated with T which represents the logical value true Change the first invariant to cars_go BOOL and the second invariant to peds_go BOOL Event B provides the build in datatype BOOL amongst others Ly Mathematical Symbols Every mathematical symbol has an ASCII representation and the substitution occurs automatically To generate element of simply type a colon The editor will perform the substitution after a short delay The Symbols view shows all supported mathematical symbols The ASCII representation of a symbol can be found by hovering ov
138. small question mark For instance inv3 has all proof obligations as children while the event set_cars has one To prevent the invariant from being violated and therefore to allow all proof obligations to be discharged we need to strengthen the guards of the events A Before looking at the solution try to fix the model yourself Finding Invariant Violations with ProB Y A useful tool for understanding and debugging a model is a model checker like ProB You B can install ProB from the ProB Update Site directly from Rodin Just select Install New Software from the Help menu and select ProB from the dropdown You should see ProB for Rodin2 as an installation option which you can then install using the normal Eclipse mechanism We will continue the example at the point where we added the safety invariant REQ 1 but didn t add guards yet to prevent the invariants from being violated 2 4 THE FIRST MACHINE A TRAFFIC LIGHT CONTROLLER 21 We launch ProB by right clicking on the machine we d like to animate and select Start Animation Model Checking Rodin will switch to the ProB Perspective as shown in Figure 2 9 The top left pane shows the available events of the machines Upon starting only INITIALIZATION is enabled The middle pane shows the current state of the machine and the right pane shows a history On the bottom of the main pane we can see whether any errors occurred like invariant violations
139. so we need to select a few The old deadlock freeness invariant will be useful and axm7 of doors_ctx2 as well AXIOMS axm7 Jl l LA outside A outside l com A P x I C aut We will try to avoid using exit since we want to keep things as simple as possible Because sit and aut are inside the invariant we also are likely to need sit C aut A site Po L 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 Add this case as previously using the Case Distinction button dc To do this you first need to instantiate the value for p To do this use the hypothesis Jp l p gt l aut A sit p 1 and then click on the existential quantifier to create the expression p P see Figure 2 23 Initialize the value of q with the value of p type p into the yellow box next to q For m you will use the existential quantifier of axm7 of doors ctx2 to instantiate m add the axiom as a hypothesis and then click on the existential quantifier next to the 1 Once the variable has been initialised type it into the yellow box next to m For the other case we will need the notion of exit This function exit connects locations to locations and defines at every location except outside We can look at the axioms about exit 2 10 LOCATION ACCESS CONTROLLER 51 Outside Figure 2 24 TODO Description AXIOMS axm3 exit L o
140. something is unclear remember to check the Reference 3 for more information 2 1 Outline Background before getting started 2 2 We give a brief description of what Event B is and what it is being used for and what kind of background knowledge we expect Installation 2 3 We guide you through downloading installing and starting Rodin and point out platform differences We install the provers We name the visible views and describe what they are doing A Machine and nothing else 2 4 We introduce a first machine a traffic light with booleans for signals We introduce guards resulting in the proof obligations to be discharged automatically We explain how proof labels are read without changing to the proof perspective Mathematical notation 2 5 At this point we quickly go through the most important aspects of predicate calculus and provide pointers to the reference and to external literature We cover everything used by the traffic light system we introduce all data types and we introduce sets and relations but not in depth Difference between predicates and expressions for instance understand the difference between TRUE and T Introducing Contexts 2 6 We introduce Contexts to apply the theoretical concepts that were introduced in the previous section We use the Agatha Puzzle to step by step introduce more and more complex elements We point out partitions as a typical pitfall also add to FAQ We will cover Theorems
141. ss it is always the corresponding concrete parameter The initialisation event sometimes needs witnesses in this case do not forget to use the after value of variable x Initialization The initialization of a machine is given by a special event called INITIALISATION Unlike other events the initialization must not contain guards and parameters The actions must not make use of variable values before the initialization event occurs All variables must have a value assigned to them If there is no assignment for the variable x Rodin assumes a default assignment of the form x T Ensuring machine consistency The following proof obligations are generated for events The assignment a of each action with the label actionlabel of an event must be well defined Well definedness of actions Name eventlabel actionlabel WD Goal A c AI c v w AG c w u gt L L a If the event s guard is enabled every action must be feasible This is trivially true in the case of the deterministic assignments For a non deterministic assignment a the feasibility F a must be proven The feasibility operator F is defined in the reference section regarding non deterministic assignments Action feasibility Name eventlabel actionlabel FIS Goal A c A I c v w A G c w u gt F a For each invariant J with the label invlabel that contains a variable affected by the assignment it must be proven that the invariant still holds with the new values
142. ss just that checking well definedness is undecidable because it involves finding a proof As D E in the worst case grows exponentially in the size of E it is not computed directly in the Rodin platform Instead another syntactic transformation is defined and D E is approximated by E In the case of disjunction L pV y L d A L w which is equivalent to the first two disjuncts of D V w One may therefore view L E as an incomplete strategy for proving D E Approximating D by is sound because L E gt D E is always provable Nomenclature In this article the following nomenclature is used 1 1 2 isa formula 1 1 is a term is an operator is a predicate In other places but not in this wiki page 1 1 2 is called predicate and 1 1 expression edit D Well Definedness edit Definition We associate with each operator f a domain condition DOM f Informally the domain condition of an operator determines which terms the operator may be applied to Formally if f t is a term then DOM f t is a formula Intuitively if f t is a well typed term DOM f t is true if and only if t belongs to the intended domain of f For example DOM t u u 4 0 DOM app r xz x dom r Ar A B assuming that r is of type P A x B Here the operator app takes a function r and a value x and returns the result of applying r to x The various domain conditions can be found i
143. ssion 4 3 6 How can I create a new Event B Project CONTENT MIGRATED EROM WIKI Please check the tutorial 2 4 1 to learn how to create a new Event B project 4 3 7 How to remove a Event B Project CONTENT a ae In order to remove a project you first select it on the Project Explorer and then right click with the mouse The contextual menu will appear on the screen as indicated in figure 4 1 E Event B Explorer N b 2 Doo Ctrii c b T tut aia Ctri v Pb t tuto Figure 4 1 Removing a Event B Project You simply click on Delete and your project will be deleted confirmation is asked It is then removed from the Project Explorer 4 3 8 How to export a Event B Project CONTENT E 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 4 3 MODELING 113 E Event B Explorer 3 lal a s of lp e b ip Celebrity i b Door gt b tutori E e gt wtutori 3 Paste Ctri V X Delete Delete Move Rename F2 g Import 1 Export Refresh FS Pri A A A Figure 4 2 Export a Event B Project 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 click on File Export from the menubar as
144. sult of this process is a list of output sequents if the process is successful or none if not e The rule is applicable if the goal of the sequent is not exactly the same as the used goal or if any of the used hypotheses are not contained in the set of hypotheses of the input sequent e If the case is applicable the antecedent sequents are returned The goal of each antecedent sequent is the new goal The hypotheses of each antecedent sequent are the union of the old hypotheses and added hypotheses of the corresponding antecedent 1 The user interface for proving is explained in Section 3 1 5 The practical application of proof rules is explained in Section 2 9 3 3 4 3 Proof Tactics Tactics provide an easier way to construct and manage proof search and manipulation They provide calls to the underlying reasoners or other tactics to modify proofs oy A list of all proof tactics is maintained in the Rodin Wiki This list is really comprehensive be sure to check it out Tactics can be applied as follows Automatic Rodin can try a number of tactics after each manual proof step In the GUI Section Proof tree Pruning the proof tree is one drastic tactic that is applied from the proof tree through the context menu Other tactics may be available there In sequents Some sequents have elements that are highlighted in red clicking on those exposes a menu with all applicable tactics where they can be applied manually It can be
145. t C AN Example Consider the following proof rule Ej E V Es This says that if Ey holds then Ey V E2 holds as well Thus we can replace the sequent by the consequent Proof Rule Representation in Rodin In Rodin the representation for proof rules is more structured not only to reduce the space required to store the rule but more importantly to support proof reuse A proof rule in Rodin contains the following used goal A used goal predicate used hypotheses The set of used hypotheses antecedents A list of antecedents to be explain later reasoner The reasoner used to generate this proof rule see reasoners 3 4 6 reasoner input The input for the reasoner to generate this proof rule see reasoners 3 4 6 Each antecedent of the proof rule contains the following information new goal A new goal predicate added hypotheses The set of added hypotheses 3 4 PROVING 103 With this representation a proof rule in Rodin corresponding to a proof schema as follows H H Ha Ga H Hy Ha 1 Ga 1 H Hy F Gy Where e H is the set of used hypotheses Gau is the used goal H a is the set of added hypotheses corresponding to the ith antecedent Ga is the new goal corresponding to the ith antecedent H is the meta variable that can be instantiated Applying Proof Rules Given a proof rule of the form mentioned above the following describes how to apply this rule to an input sequent The re
146. t shorter r AO B ASCII r A lt gt B With a gt b r we can check if two elements a and b are related in respect to b 26 CHAPTER 2 TUTORIAL We use a small example to illustrate relations Let A a b c d and B 1 2 3 4 We define the relation r with r a gt 1 a gt 3 c gt 2 d gt 1 The domain of r are all elements occurring on the left side dom r a c and the range are all elements on the right ran r 1 2 3 To find out to which elements the objects of the set s b c d are related to we can use the relational image r s r b c d 1 2 Often we want to know to which object a single element b is related We just write it as a singleton set r a 1 3 Event B supports several operators to work with relations TODO link We will not go into more detail during the course of the tutorial An important special case of relations are functions TODO link Functions are relations where each element of the domain is uniquely related to one element of the range Event B directly supports operators to describe partial and total functions which can injective surjective or bijective 2 5 6 Arithmetic We have the usual operations on integers and ASCII x and They can be compared with the usual lt lt gt gt ASCII lt lt gt gt Z ASCII INT denotes the set of all integer numbers N and N ASCII NAT resp NAT1 are the subsets of natural numb
147. te where the invariant holds e Assuming that the machine is in a state where the invariant holds every enabled event leads to a state where the invariant holds Rodin generates proof obligations for every invariant that can be changed by an event i e the invariant contains variables changed by an event The name of the proof obligation is then event_name invariant_label INV The goal of such a proof is to assert that when all affected variables are replaced by new values from the actions the invariant still holds The hypotheses for such a proof obligation consist of e All invariants because we assume that all invariants hold before the event is triggered e All guards because events can only be triggered when the guards are valid In the special case of an initialization we cannot use the invariants because we do not make any assump tions about uninitialized machines 2 7 4 Refinement Refinement is a central concept in Event B Refinements are used to gradually introduce the details and complexity into a model If a machine B refines a machine A B is only allowed to behave in a way that corresponds to the behavior of A We now look into more detail of what corresponds here means In such a setting we call A the abstract and B the concrete machine Here we give just a brief overview over the concept of refinement Later in Section 2 8 we use refinement in an example The concrete machine has its own set of variables
148. ted hypothesis A user wishing to attempt an interactive proof has a number of proof rules available and these may either rewrite a hypothesis goal or infer something from it In the Goal and the Selected Hypotheses views various operators may appear in red coloured font The red font indicates that some interactive proof rule s are applicable and may be applied as a step in the proof attempt When the mouse hovers over such an operator a number of applicable rules may be displayed the user may choose to apply one of the rules by clicking on it Figure 3 28 shows an example Other proof rules can be applied when green buttons appear in the Goal and Selected Hypotheses views Examples are proof by contradiction et and conjunction introduction A l Y a Oe teToken tok SCT Vreres gt x E n act Hr auth tun Remove inclusion in hypothesis State Remove inclusion universal in hypothesis W Goal El eb iticdomiutokuit ur Figure 3 28 Applying a rule To instantiate a quantifier the user enters the desired expression in the box behind the quantifier and clicks on the quantifier the red 3 as demonstrated in figure 3 29 The Proof Control View The Proof Control view contains the buttons with which you can perform an interactive proof An overview of this proof can be seen in Figure 3 30 The following buttons are available in the Proof Control view 3 1 THE RODIN PLATFORM 71 Figure 3 29 Instantiating
149. this clear The expression x y makes only sense when y 0 In Rodin the operator TODO look up how this is called correctly and add a reference to the appro priate sources is implemented When applied to the above example integer division can be formatted as follows L x y S y 0 Well definedness conditions are usually used for the well definedness proof obligations In the following sections we state for each mathematical construct what the well definedness conditions are In many cases this is just the conjunction of the well definedness conditions for the different syntactical parts of a construct Structure of the reference The following reference sections follow the form math Symbol ASCII representation Name of the operator Description A short description of what the operator does Definition A more formal definition Types A description of the types of all arguments and if the operation is an expression the expression s type WD A description of the well definedness conditions using the operator Feasibility Non deterministic assignments may have feasability conditions These are used in the proof obligations of an event section 3 2 3 96 CHAPTER 3 REFERENCE 3 3 2 Predicates Logical primitives true True false False Description The predicates T and L are the predicates that are true and false respectively WD L M T PST Logical operators
150. ticipated event or a finite set expression which must be made strictly smaller by each convergent event or not made greater by each anticipated events 3 2 4 Generated proof obligations We give a brief overview about which POs are generated This should help the user to identify the why a PO generated when he can identify its label CONTENT E Proof obligations abbreviated as PO are generated by the proof obligation generator and have the form of sequents The following tables list the different PO and their associated name This table describes the names of context proof obligations Well defimedness of an Axiom Welk definedness of a Derived Axiom m THM This table shows the name of machine proof obligations 3 2 EVENT B MODELING NOTATION 91 Well definedness of an Invariant Well definedness of a Derived Invariant Well definedness of an event Guard t d WD t is the event name d is the ac e o SS Well definedness of an event Action t d WD t is the event name d is the ac D AA Feasibility of a non det event Action t d FIS t is the event name d is the ac tion name Derived Invariant m THM Invariant Establishment INIT v INV Invariant Preservation t v INV t is the event name v is the in variant name This table shows the proof obligations concerned with machine refinements Guard Strengthening t d GRD t is the concrete event name d is Guard Strengthening merge Act
151. ton bring up the window shown in figure 3 15 New Enumerated Set Identifier Element Element Element i More Element Cancel Figure 3 15 New Enumerated Set Wizard Enter the name of the new enumerated set as well as the names of its elements By pressing the More Elements button you can enter additional elements When you re finished press the OK button The benefit of using this wizard is that in addition to creating the set and its elements the wizard automatically creates the axiom that is necessary for the context to work For example when you add the new carrier set COLOR and the three constants red green and orange the wizard automatically creates the following axiom partition COLOR red green orange 62 CHAPTER 3 REFERENCE New Constants Wizard ate To activate the New Constants Wizard press the button located in the tool bar Pressing the button will bring up the window shown in figure 3 16 entiter p pom oad BE TAN tthe aa morenn comen 3 Figure 3 16 New Constants Wizard You can then enter the names of a constant and an axiom which can be used to define the constant s type By pressing More Axm button you can enter additional axioms To add more constants press the Add button When you have finished press the OK button New Axioms Wizard ate To activate the New Axioms Wizard press the button located in the tool bar Pressing the button brings up the windo
152. tors Toolbars Quickview Perspectives and many more elements We name the different Rodin GUI elements i e Views which are visible after starting Rodin for the first time and explain their functions Menu bar 3 1 2 The menu bar of Rodin provides for instance file and edit operations Tool bar The tool bar provides short cuts for familiar commands like save print undo and redo Event B Explorer 3 1 2 The Event B Explorer shows the projects tree structures It has projects as main entries and for each one its corresponding project files Outline View 3 1 2 A view used to view the outline of the active editor or file respectively Rodin Problems view The Rodin Problems View shows problems i e syntax errors in the active editor Symbols View 3 1 2 A view that shows a list of available mathematical symbols which can be used in conjunction with the mathematical notation 3 3 Editor View 3 1 2 The editor view contains the active editor 2 See Rodin Release Notes 2 4 THE FIRST MACHINE A TRAFFIC LIGHT CONTROLLER 15 Menu bar Tool bar Editor View Outline View Event B Rodin P atform cs cil 5 File Edit Navigate Search Project Run Window Help rt Ar 4a to H a vent B E Event B Ex E oO 8 5 Outl Es o de T An ou is not availa Jlo Rodin Problems amp gt Properties Tasks jp 0 4 Symbols E gt Progress o O errors 0 warnings 0 infos ee unes gp ESS Descr
153. tutorial 05 Y Goal E gt Goal is not available 2 Proof Control aN O Statistics Rodin Proble Symbols N Proof Control is not available gt a Gy B Celebrity Figure 2 18 Rodin Proving Perspective The Proving Perspective contains three new important views 2 9 PROVING 45 Proof Tree View 3 1 5 Here we see a tree of the proof that we have done so far and the current position in it By clicking in the tree we can navigate inside the proof Currently we have not started with the proof so there is no new place to move to Proof Control View 3 1 5 This is where we perform interactive proofs Goal View This window shows what needs to be proved at the current position inside the proof tree Expand the Celebrity_1 machine in the Event B Explorer Then expand the Proof Obligations section We can see that the auto prover 3 1 6 did quite a good job Only three proofs have not been completed completed a completed proof is indicated by a green check Let s start with the proof remove_1 inv2 INV of Celebrity_1 To do this double click on the proof obligation remove_1 inv2 INV We should now see the window as shown in Figure 2 19 Pow ine Celebrity celebrity bps Rodin Platform File Edit Navigate Search Project Run ProB Window Help ris A mE E Proving s b Pro 3 A QCelebrity 1230 Alt EventBE 7a 7 remove Vinv2 INV geo T
154. uild his own automated tactics More precisely the user should have a way to specify which parameters have to be passed to the reasoners and have a way to construct complex proof strategies 3 1 THE RODIN PLATFORM Sl Preferences H Auto Post Tactic v Pb General Y Event B Customize Event B Tactics Configure project specific settings Pb Appearance Auto Post Tactic Profiles P Modelling UI Proving Ul Auto Tactics Sequent Prover Enable auto tactic for proving cotos Tactic profile to be used for auto tactics Default Auto Tactic Profile P Help gt Install Update Post Tactics P Run Debug l Enable post tactic for proving E Tactic profile to be used for post tactics Default Post Tactic Profile Restore Defaults Apply F 2 Cancel OK Figure 3 41 The Auto Post Tactic preference page User Documentation Here is the documentation about the current implementation of automatic tactics preferences Auto tactic dz Post tactic Tactic Combinators Tactic combinators can be used to construct complex proof strategies Historically one combinator has existed since the beginning of auto tactic preferences the loop on all pending It takes one or more tactics and loops them over every pending child until all tactic fail Until Rodin 2 3 was released it was the only combinator in Rodin It is used on the configurable list of auto and post tactics Rodin 2 3 is easier to configure because there ar
155. ular we would like to thank Systerel for their significant contributions to the handbook as they have been the main driver behind the tool and its documentation We would also like to thank Cliff Jones who never gave up the quest for improved Rodin documentation The icons that you find throughout this handbook were created by Pixel Mixer who provides them freely Thanks http www systerel fr 2http pixel mixer com 1 5 DEPLOY 9 15 DEPLOY This work has been sponsored by the DEPLOY project DEPLOY is an European Commission Information and Communication Technologies FP7 project The overall aim of the EC Information and Communication Technologies FP7 DEPLOY Project is to make major advances in engineering methods for dependable systems through the deployment of formal engineering methods Formal engineering methods enable greater mastery of complexity than found in traditional software engineering processes It is the central role played by mechanically analysed formal models throughout the system development flow that enables mastery of complexity As well as leading to big improvements in system dependability greater mastery of complexity also leads to greater productivity by reducing the expensive test debug rework cycle and by facilitating increased reuse of software The work of the project is driven by the tasks of achieving and evaluating industrial take up initially by DEPLOY s industrial partners of DEPLOY
156. urce El ava Galois D cowhd CEE ceicte Y Galois o Selected Hypotheses a Sm el fen N mF el ten gt N a al tot h T a t fet Bs a T gt ONE e fgs A ata gt f ES al ko def o xl o xet el x1eN a ADN take I Goal El en 7 xl weet Proof Control 22 Problems peo O E y Tres Oo Tactic applied successfully Figure 3 8 Our self made Quick perspective BE CONTEXT Cex SS gt EXTENDS gt SETS gt CONSTANTS gt AXIOMS END Pretty Print Edit Synthesis Dependencies Figure 3 9 The Event B editor keyword you can see the different modelling elements and also add remove or move them Figure 3 10 shows what the section looks like after pressing the triangle next to the keyword AXIOMS By pressing the button you can add a new modelling element For instance clicking on the button next in the AXIOMS section will add a new axiom element You can now enter a new axiom and a comment in the corresponding boxes as indicated in Figure 3 11 To remove a modelling element press the o button You can also move an modelling element up or 60 CHAPTER 3 REFERENCE gt CONSTANTS poon ept END Pretty Print Edit Synthesis Figure 3 10 By pressing the triangle you can collapse expand context sections lt 7 AXIOMS et o not theorem i b is a constant booking et END Pretty Print Edit Synthesis Dependencies Figure 3 11 Adding a new modelling ele
157. useful to consider the following categorization of tactics Shttp wiki event b org index php Rodin_Proof_Tactics 104 CHAPTER 3 REFERENCE Basic Tactics They are those tactics that make change to the proof tree only at the point of application e Prune direct application of the pruning facility providing by the proof tree The tactic is successful if the input node are non pending e Rule Application Tactics of this class provide a wrapper around a proof rule See Proof Rules The tactic is successful if the proof rule is successful applied to the input node e Reasoner Application Tactics of this class provide a wrapper around a reasoner See Reasoner The tactic is successful if the reasoner is successful applied to the input node Tactical Tactics They are those tactics that are constructed from existing tactics They indicate different strategic or heuristic decisions e Apply on All Pending Apply a specific sub tactic to all pending nodes of the point of application The tactic is successful if the sub tactic is successful on one of the pending nodes e Repeating Repeating a specific sub tactic to the point of application until it fails The tactic is successful if the sub tactic is successful at least once e Composing Sequential compose a list of sub tactics to apply to the point of application The tactic is successful if one of the sub tactic is successful More complex proof strategy can be constructed by composing
158. utside gt L axm4 exit C com axm5 Vs s C erit t s gt s axm6 aut amp outside C aut exit The axioms state that e axm3 Every room except the outside has exactly one exit axm4 An exit must be a room that communicates with the current one axm5 A chain of exits leads to the outside without any cycles or infinite paths axm6 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 axmb is useless so we add all hypotheses containing exit except for axm5 Now we have to instantiate q and m correctly and to conclude that the proof should not be too hard Once again 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 wD Try translating this into set theory But do not worry if you get it wrong You can still go back in the proof by right clicking at the desired point in the proof tree and choose Prune in order to retry 52 CHAPTER 2 TUTORIAL 2 11 Outlook Congratulations if you made it this far you should have a good foundation for getting some real work done with Rodin In the following we d like to provide you with a few pointers that will help you to make your work as efficient as possible Use the Reference Section and FAQ If you have a specific issue or if you quickly need to l
159. very sequence x of variables of appropriate length and type Property 3 ensures that D E is provable if and only if F D E is provable In the future Property 3 may be replaced by a weaker version edit Important Properties of D and L edit L is stronger than D L E gt D E is provable for each term or formula E edit Monotonicity We define the order E on terms and formulae by tEuffD t gt t u is provable and p E pif fD d gt 6S Y isprovable Then D has the following monotonicity properties TODO add citation u v are terms x is a variable are formulae E is a term or a formula and p is a position in E If uE v thenElzx u E Elx v If y Cx then Epl E Elx Here Ep denotes the term or formula obtained by replacing the subformula at position p in E by We assume that bound variables of E do not appear free in or which can be achieved by consistent renaming of variables The above monotonicity properties are crucial for the soundness of several rewrite rules such as t 0 0 It is possible to prove similar monotonicity properties for but monotonicity of is not necessary for soundness of any inference rule edit Strictness We have decided to make operators strict i e if some element in the list of terms t is ill defined then so is f t where f is an operator Predicates are also strict The strictness property can be dropped without making any inference rule unsound as long as the monotonicity
160. w shown in figure 3 17 Label s Predicate s Theorem a fas A fama a more cancel ok Figure 3 17 New Axioms Wizard You can then enter the axioms you want If more axioms are needed press the More button When you are finished press the OK button Check the Theorem checkbox to indicate that the corresponding axiom should be a theorem New Variable Wizard To activate the New Variable Wizard press the ye button located in the tool bar Pressing the button brings up the window shown in figure 3 18 You can then enter the names of the variable what its state at initialization should be and an invariant which defines 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 1 THE RODIN PLATFORM 63 New Variable x identifier a varl initialisation fact2 var Invariant inv2 var e not theorem Add More Inv Cancel Figure 3 18 New Variable Wizard New Invariants Wizard To activate the New Invariants Wizard press the button located in the tool bar Pressing the button bring up the window shown in figure 3 19 New Invariants Label s Predicate s Theorem fina TO fins o fina SO woe cme C Figure 3 19 New Invariants Wizard You can then enter the invariants you want If more invariants are needed press the More button Check the Theorem checkb
161. w to Use the Provers Effectively 106 CONTENTS JAO MSO cesos tee eee aser Ot FURS Prodo ong dwn ht oe he eee wR REEDS RSE EER wR BREE GOH 4 Frequently Asked Questions 4 1 4 2 4 3 4 4 4 5 4 6 Index G neral Questions s s gt orita DEG oo OE HEE GS ALI Whatis EventeB cocos aceras 4 1 2 What is the difference between Event B and the B method 4 1 5 How to contribute and develop o a a General Tool Usage ooon oa a a a 4 2 1 DoTI lose my proofs when I clean a project 4 2 2 How do I install external plug ins without using Eclipse Update Manager 4 2 3 The builder takes too long Kana iama a 4 2 4 What are the ASCII shortcuts for mathematical operators 4 2 5 Rodin and eclipse doesn t take into account the MOZILLA _FTIVE_HOME environ ment variable ooo sardina A e a 426 No More Handles s a coc ered a na PRE A RRR we EE RE RE a a2 polare lnstallati n tae c8tiwe detar sordos aserrada WEIS corran ada AAA AAA 4 3 1 Witness for Xyz missing Default witness generated 0 0008 0G 4 3 2 Identifier Xyz should not occur free in a witness 2 2 2 eee ee 4 3 3 In INITIALISATION I get Witness Xyz must be a disappearing abstract variable or CIIU rra AAA 4 3 4 I ve added a witness for Xyz but it keeps saying Identifier Xyz has

User Manual for Rodin v.2.3 - Rodin Handbook - Event

Contents

Download Pdf Manuals

Related Search

Related Contents