Theory Plug-in User Manual - Event
Contents
1. Associativity not applicable Y Commutativity not commutative v Gv arguments ego a a P A e L lt v well definedness condition eri vdirect definition e7d 9 Formulan f nena teina T e t v recursive definition ere e t Figure 6 Sequence Operator Definition Note the numbering in figure 6 The following explains each part of the definition 1 Syntax Symbol this specifies the syntax token that will be reserved for the new operator sequence in our example It should not clash with any previously defined symbol in the mathematical language available to the theory 2 Syntactic Class this specifies whether the new operator is an expression operator or a predicate operator For example the cardinality operator card is an expression operator of integer type and the finiteness operator finite is a predicate operator In our case the sequence operator is an expression operator The button can be toggled off if a predicate operator is required instead 3 Notation this specifies whether the symbols is a prefix or an infix opera tor In the existing mathematical language is an infix operator whereas partition is a prefix predicate operator In our example the sequence op erator is specified as prefix 4 Associativity this specifies whether the operator is associative Note that this has semantic implications and as such a proof obligation is generated to check the associativi2. In the Event B mathematical language predicates known as formulae in most literature and expressions known as terms are two separate syntactic categories Expressions have a type Predicate do not 3 Quick Start In this section we step through a simple tutorial on how to define and use a simple theory Click on the links above to navigate through this tutorial 3 1 Install Theory Plug in Considering figure 1 the installation or update for the Theory plug in is avail able under the main Rodin Update site http rodin b sharp sourceforge net updates under the category Modelling Extensions Like always af ter the installation restarting Rodin is recommended For more details see Install Available Software Check the items that you wish to install Work with Rodin http rodin b sharp sourceforge net updates Find more software by working with the Available Software Sites preferences Name Version b C 000 Composition and Decomposition gt _ 000 Edition gt C 000 Event B EMF Framework v 100 Modelling Extensions _ EventB Statemachines 0 1 4 201105221556 Event B Theory Feature O 4 Records O amp UML B Modelling Environment gt C 000 Prover Extensions gt _ 000 Select All Deselect All 1 item selected Details The Event B Theory Feature provides a mechanism by which user can specify and validate mathematical and prover extensions It also provides a
3. THEOREMS eid 7 PROOF RULES ea i END HTML Edit Figure 4 The Theory Editor The theory editor has two pages an Edit page and an HTML i e pretty print page The edit page corresponds to the structured editor The HTML page is a pretty print view of the theory 3 3 Adda Type Parameter Type parameters in a theory specify the types on which new definitions and rules may be polymorphic For instance a theory of sequences can be polymorphic on one type and that is the type of elements it may hold Type parameters are similar in nature to carrier sets in contexts To create a new type parameter click on button under the Type Parameters section of the structured editor and specify the name of the type parameter see figure 5 A Type parameters are expected to be a legal Event B identifier For example 27dent is not a legal identifier lt TYPE PARAMETERS ett e B A i eot Figure 5 Type Parameters v As a convention type parameters are specified as upper case strings same as context s carrier sets 3 4 Create an Operator Definition Event B mathematical language has many useful operators Examples include cardinality operator card the finiteness predicate operator finite and the func tion application Other useful operators can be defined using the Theory plug in Figure 6 shows a definition of a sequence operator v OPERATORS ed 2 3 4 5 vo seq expression PREFIX
4. Rodin v2 0 the mathematical language used in Event B was fixed As such it was not possible to define reusable polymorphic operators A workaround was to define any required operators as set constructs in contexts Originally contexts were supposed to provide a parametrization of machines The aforementioned limitations of the Event B language lead to users to use contexts for purposes for which they were not intentionally devised Examples of operators that can be useful to users include the sequence operator which was present in classical B mathematical language and the bag operator In Rodin v2 0 a dynamic parser has been implemented for the Event B AST The Theory plug in was a natural candidate for defining and using mathematical extensions To provide a comprehensive platform cover for a wider range of proof rules was also needed ML is a rule based prover as opposed to the semi decision procedure PP 2 Capabilities The Theory plug in has the following capabilities 1 Theory Definition a Definition of operators operators can be defined as predicate or expression operators An expression operator is an operator that returns an expression an example existing operator is card A predicate operator is one that returns a predicate an example ex isting predicate operator is finite Definition of datatypes datatypes are defined by supplying the types on which they are polymorphic a set of constructors one
5. Theory Plug in User Manual Issam Maamria Asieh Salehi Fathabadi University of Southampton June 20 2013 The Theory plug in is a contribution to the Rodin platform that facilitates the specification validation deployment and use of language and proof extensions for the Event B methodology Language extensions are additions to the Event B mathematical language in the form of 1 datatypes 2 operators and 3 axiomatic definitions Proof extensions are additions to the Event B proving infrastructure in the form of rewrite rules inference rules and polymor phic theorems The specification of extensions is achieved by means of theories The validation of extensions is achieved by means of proof obligations when ever appropriate This user manual provides a comprehensive overview of the plug in s functionality and capabilities For a quick start guide the user can skip to Section 3 The Event B mathematical language refers to the language used to write axioms invariants guards etc in Event B models Event B theories are Rodin file just like contexts and machines 1 Motivation Work on the Theory plug in started as an effort to create a Rule based Prover for Event B much like the ML prover in Atelier B The Rule based Prover as it was known then supported the definition validation and use of rewrite rules The Theory plug in is the successor of the Rule based Prover and offers much more functionality Prior to
6. ation generated if the operator is tagged as commutative 3 Op ASSOC the associativity proof obligation generated if the operator is tagged as associative 3 5 Specify a Polymorphic Theorem A polymorphic theorem is no different in principle from theorems defined in contexts and machines The Theory plug in however provides facilities to instantiate and use these theorems in proofs See the example in figure 12 q THEOREMS Name Theorem D seqsIsFinite Ws a acAas e segla gt finite s Figure 12 Sequence Finiteness Theorem The previous theorem articulates the fact the sequences as specified in our example are finite As with theorems in contexts and machines you have to prove validity and well definedness of the theorem The proof obligations asso ciated with a theorem are the following 1 S THM the validity proof obligation 2 WD THM the well definedness proof obligation Figure 13 shows other theorems that can be defined in relation to our theory of sequences so far THEOREMS seqsIisFinite Ws a acAas seq a finite s seqsMonotone Vs a b aC As E segq a aat b s seq b tailSeqIsS5Seq Ys a aCA a s seq a a seqlsEmpty s seqTail s seq a seqgPrependIsSeq Ys a e aCA as seq a seqPrepend s e eseq aU e segAppendIsSeq Ys a e aCA as seq a seqAppend s e E seqlau e Figure 13 Sequence Theorems v A theorem can be instantiate
7. d e g in the previous example the type parameter A can be substituted with a type expression that is acceptable in the context of the sequent under consideration We will later show how this is achieved 12 3 6 Specify an Inference Rule Inference rules are proof rules that can be used to 1 infer new hypotheses in a proof or 2 split the goal into sub goals or 3 discharge a proof obligation The general structure of an inference rule is as follows Given GO Gn Infer I where each of GO Gn and J is an Event B predicate The above inference rule can be read in the following two ways given conditions GO Gn one can infer J and one can prove J if one can prove each of GO Gn Inference rules can be defined as part of a block of Proof Rules Each proof rules block may contain a number of metavariables rewrite rules and in ference rules see figure 14 To create a rules block under the heading PROOF RULES in the structured editor press e lt v E Sequences Rules gt Metavariables Rewrite Rules Inference Rules eri Figure 14 Proof Rules Block Metavariables define the variables used to specify proof rules Considering figure 15 each metavariable has a name and a type For our example we need one metavariable s v Metavariables ered s Typ Z A Figure 15 Defining a Metavariable The example in figure shows an
8. e The argument type can be a type or a set expression If the argument type is a set expression then the type of the argument is inferred Fur thermore the additional restriction i e that the argument belongs to a set expression is added as a well definedness condition for the operator v e As a convention names of operators should be lower case e As a convention names of operator arguments should be lower case The operator in figure 7 defines size for sequences vD seqSize expression PREFIX Associativity not applicable Y Commutativity not commutative v size of sequences v arguments erg expression erg wv well definedness condition erg vdirect definition erg ae a a ae Note that this expression is only defined when the set s is finite rormula EIS erg lt v recursive definition eri Note that the argument belongs to a set expression rather than a type Figure 7 Sequence Size Operator Definition This definition asserts that the operator seqSize takes one argument of type Z A This definition also triggers a proof obligation to prove the strength of the well definedness condition provided Namely one has to prove that Vs s seq A gt finite s We leave this as an exercise to the reader Figure 8 is a definition of a predicate operator The definition of segisEmpty does not trigger any proof obligation for well definedness strength This is due
9. en from the HTML view of our theory seq seq a P A EXPRESSION PREFIX The sequence operator direct definition a P A fn neNa fe 1 n alf a set of finite total functions seqSize seqSize s seq A EXPRESSION PREFIX size of sequences direct definition seqSize s seq A card s seqisEmpty seqilsEmpty s seq A PREDICATE PREFIX direct definition seqisEmpty s seq A seqSize s 0 eseqHead seqHead s seq A EXPRESSION PREFIX oj a non empty sequence well definedness condition seqisEmpty s direct definition seqHead s seq A s 1 seqlail seqTail s seq A EXPRESSION PREFIX the tail of a non empty sequence well definedness condition seqisEmpty s direct definition seqTail s seq A Ai ie1 seqSize s 1 s i 1 seqPrepend seqPrepend s seq A e A EXPRESSION PREFIX direct definition pend s seq A 1lre U Ai iE 2 seqSize s 1 s i 1 seqAppend seqAppend s seq A e A EXPRESSION PREFIX appends an element to a sequence direct definition segqAppend s seq A e A sU seqSize s 1 re predicate operator that checks whether a given sequence is empty Figure 11 Various Sequence Operators 11 The proof obligations associated with an operator definition are the follow ing 1 Op WD operator well definedness strength if a well definedness condi tion is explicitly specified 2 Op COMMUT the commutativity proof oblig
10. inference rule concerning finiteness of sequences 13 lt Inference Rules ei i vO seqsIsFiniteInt Applicability interactive Description sequences are finite v Given eti js e seq a ept v Infer etb ffinite s r i Figure 16 Sequence Finiteness Inference Rule The applicability of a proof rule indicates whether the rule should be applied automatically or interactively The description provides a human readable view of the rule The description provided will be the tool tip for the rule in the proof UI The inference rule in figure is an automatic rule that states that the tail of a non empty sequence is a sequence vO tallSeqIsSegInf Applicability automatic i Description Describe Me lt Given eri s e seq a seqIsEmpty s eri v Infer L seqTail s eseq a eri Figure 17 Sequence Tail Inference Rule 14 4 Scoping and Using of Theories A theorypath is a means to introduce the deployed theories in a project scope In order to use a math extension defined in a theory in a project scope 1 Deploy the theory by clicking the button figure 18 t Event B Explore ei E a aes ef G Figure 18 Deploy Theory Button in Event B Explorer Alternatively a theory can be deployed by a pop up menu by right clicking on the thoery 2 Import the deployed theory in a theorypath which is defined in the project scope By c
11. licking the button 2 a wizard that enables the creation of a new theorypath is initiated See figure 19 t Event B Explore 2 E z EEA G Figure 19 New Theorypath Button in Event B Explorer A e A machine contex accesses local global theories imported directly or indirectly by a theorypath within the same project as the machine contex e A theory path can imports deployed local global theories e A theory can import deployed local global theories Uw 15 e A local theory in a project scope is a theory defined inside a project Whereas a global theory is a theory defined in a separated project e As illustrated in figure if theory T1 imports theory T2 and theory T1 is imported in a theorypath created in the project Prj Then T1 is directly and T2 is indirectly accessible in the Prj scope E Event B Explorer 3 Off X TheoryPath 32 a 5 EE ge 7 amp THEory T1 F THEORYPATH TheoryPath O 4 W NewProject 12 lt IMPORTS THEORY PROJECTS lt THEORY PROJECTS a Py ere eres TB TheoryPath T T1 lt E NewProject v 7H 0 Pij v v7 THEORIES v THEORIES e7 eg ere ToT v o it v ere e7 es e7e ere END gt TYPE PARAMETERS gt DATATYPES gt OPERATORS D AXIOMATIC DEFINITIONS gt THEOREMS gt PROOF RULES END lt gt lt gt HTML Edit HTML Edit Figure 20 Accessibility of Theories 16
12. mechanism to use defined extensions Figure 1 Install Theory Plug in Once the Theory plug in is successfully installed menu entries will be added in certain places see figure 2 In particular the Event B Explorer will have an additional button that initiates the wizard to create new theory files Figure 2 New Theory Button in Event B Explorer 3 2 Create A New Theory An additional button red circled in figure 2 should appear in the Event B Explorer By clicking the button t a wizard that enables the creation of a new theory is initiated Figure 3 shows the wizard in action New EventB Theory This wizard creates a new theory file with but extension Project MathExtensions Browse Figure 3 New Theory File Wizard In the wizard specify the parent project of the theory and a theory name The project can be selected using the button on the right hand side of project name text field akin to selecting a project when creating a new Event B com ponent Click the Finish button to create the theory If there are no name clashes between the name of the new theory and any existing resources you should get a theory editor opened up as depicted in figure 4 T Theory 3 E H THEORY Theory New Empty Theory lt IMPORTS THEORY PROJECTS evi lt TYPE PARAMETERS eri lt DATATYPES eri lt OPERATORS eid lt AXIOMATIC DEFINITIONS eid
13. of which has to be a base constructor Each constructor may or may not have destructors Definition of axiomatic definitions axiomatic definitions are de fined by supplying the types a set of operators and a set of axioms Definition of rewrite rules rewrite rules are one directional equal ities that can be applied from left to right The Theory plug in can be used to define rewrite rules Definition of inference rules inference rules can be used to infer new hypotheses split a goal into sub goals or discharge sequents Definition of polymorphic theorems theorems can be defined and validated once and can then be imported into sequents of proof obligations if a suitable type instantiation is available Validation of extensions where appropriate proof obligations are generated to ensure soundness of extensions This includes proof obligations for validity of inference and rewrite rules as well as proof obligations to validate operator properties such as associativity and commutativity 2 Theory Deployment this step signifies that a theory is ready for use Theories can be deployed after they have been optionally validated by the user It is strongly advisable to discharge all proof obligations before deployment Once a theory has been deployed to its designated project all its extensions mathematical and proof extensions can be used in models In later sections we show the two different scopes of theory availability
14. to the fact that the corresponding condition is a trivial predicate namely Vs s E seq A gt s E seq A The head operator on sequences can be defined as in figure 9 vD seqIsEmpty PREFIX Associativity not applicable wa Commutativity not commutative v po eiea palm Bant y v7 arguments e L s seq A e L vwell definedness condition L vdirect definition erg Formula e t lt v recursive definition erd Figure 8 A Predicate Operator Definition vD seqHead expression PREFIX Associativity not applicable Y Commutativity not commutative v the head of a non empty sequence v7 arguments ety The argument of this operator has to be sequence oes evs vwell definedness condition eve The argument of this operator must not be an empty sequence seqIsEmpty s T L v direct definition Formula e e The definition is defined iff 1 is in the domain of s erg wv recursive definition eri Figure 9 Sequence Head Operator Definition Figure 10 shows the well definedness strength proof obligation corresponding to the previous definition of seqHead 10 seqHead Op WD pom sa O ct seseq A O oe seqIsEmpty s Selected Hypotheses 4 Goal 22 ledom s A 5seZ A Figure 10 Sequence Head WD Strength PO As asummary have a look at figure 11 which is tak
15. ty property 5 Commutativity this specifies whether the operator is commutative Note that this has semantic implications and as such a proof obligation is generated to check the commutativity property 6 Operator Arguments an operator may have a number of arguments all of which may be expressions 7 Argument Identifier this specifies the name of the argument of the operator It has to be a legal Event B identifier similar to carrier sets constant variables etc 8 Argument Type this specifies the type of the argument In our case the sequence operator takes a set of type A Since A is a type parameter the sequence is polymorphic 9 Direct Definition this provides the direct definition of the operator In our case see the red boxed field it asserts that sequences are total functions from a contiguous integer range starting at 1 to the set a the argument of the operator seq Lr e Only operators that take two arguments of the same type can be tagged as commutative Of course then one has to prove the mathematical property e An operator can be tagged as being associative if it satisfies the three conditions 1 it is an expression operator 2 it takes two or more arguments of the same type 3 the type of the operator is the same as that of its arguments Of course then one has to prove the mathematical property e Operators that are tagged associative have to be tagged as infix as well
Download Pdf Manuals
Related Search