imported>Im06r |
imported>Andy |
| Line 1: |
Line 1: |
| − | === Overview === | + | = Defining Translations Using The Theory Plug-in = |
| | + | The theory plug-in is used to add mathematical extensions to Rodin. The theories are created, and deployed, and can then be used in any models in the workspace. When dealing with implementation level models, such as in Tasking Event-B, we need to consider how to translate newly added types and operators into code. We have augmented the theory interface with a Translation Rules section. This enables a user to define translation rules that map Event-B formulas to code. |
| | + | == Translation Rules== |
| | + | <div id="fig:Translation Rules"> |
| | + | <br/> |
| | + | [[Image:TheoryCGRules.png|center||caption text]] |
| | + | <center>'''Figure 1''': Translation Rules</center> |
| | + | <br/> |
| | + | </div> |
| | | | |
| − | Mathematical extensions have been co-developed by Systerel (for the Core Rodin Platform) and Southampton (for the Theory plug-in). The main purpose of this new feature was to provide the Rodin user with a way to extend the standard Event-B mathematical language by supporting user-defined operators, basic predicates and algebraic types. Along with these additional notations, the user can also define new proof rules (prover extensions).
| + | Figure 1 shows the interface, and some translations rules of the mapping to Ada. |
| | | | |
| − | A theory is a file that can be used to define new algebraic types, new operators/predicates and new proof rules. Theories are developed in the Rodin workspace, and proof obligations are generated to validate prover and mathematical extensions. When a theory is completed and (optionally) validated, the user can make it available for use in models (this action is called the deployment of a theory). Theories are deployed to the current workspace (i.e., Workspace Scope), and the user can use any defined extensions in any project within the workspace.
| + | The theory is given a name, and may import some other theories. Type parameters can be added, and we use them here to type the meta-variables. The meta-variable ''a'' is restricted to be an integer type, but meta-variable ''c'' can be any type. Meta-variables are used in the translator rules for pattern matching. |
| | | | |
| − | Records Plug-in has been developed by University of Southampton before the mathematical extensions as a new feature to provide structured types in Event-B. The plug-in extends Rodin standard context editor with a new modelling construct to provide support for structured types, which can be defined in terms of two new clauses: record declarations and record extensions. Both enable users to define their custom reusable types, that are treated underline by Rodin as Event-B constant sets and relations, supported by additional axioms, which the plug-in generates to simplify the proofs.
| + | Translator rules are templates, which are used in pattern matching. Event-B formulas are defined on the left hand side of the rule, and the code to be output (as text) appears on the right hand side of the matching rule. During translation an abstract syntax tree (AST) representation of the formula is used. The theory plug-in attempts to match the formulas in the rules with each syntactic element of the AST. As it does so it builds the textual output as a string, until the whole AST has been successfully matched. When a complete tree is matched, the target code is returned. If the AST is not matched, a warning is issued, and a string representation of the original formula is returned. |
| | | | |
| − | === Motivations === | + | == Type Rules for Code Generation == |
| | | | |
| − | Main reasons for implementing mathematical extensions are:
| + | The type rules section, shown in Figure 1, is where the relationship is defined, between Event-B types and the type system of the implementation. |
| − | * increased readability (<math>a \; \operatorname{OR} \; b</math> rather than <math>\operatorname{bool}(a=TRUE \or b=TRUE)</math>)
| |
| − | * polymorphism (<math>l \in List(S \cprod T)</math>)
| |
| − | * decreased proving effort, thanks to extension specific proof rules instead of general purpose ones
| |
| | | | |
| − | The Theory plug-in superseded the Rule-based Prover v0.3 plug-in, and is the placeholder for mathematical and prover extensions. It provides a high-level interface to the Rodin Core capabilities with regards to mathematical extensions. The Rule-based Prover was originally devised to provide an usable mechanism for user-defined rewrite rules through theories. Theories were, then, deemed a natural choice for defining mathematical extensions as well as proof rules to reason about such extensions. In essence, the Theory plug-in provides a systematic platform for defining and validating extensions through a familiar technique: proof obligations.
| + | = Adding New (implementation-level) Types = |
| | + | When we are working at abstraction levels close to the implementation level, we may make an implementation decision which requires the introduction of a new type to the development. We give an example of our approach, where we add a new array type, shown in Figure 2, and then define its translation to code. |
| | | | |
| − | The motivation for development of Records plug-in was to fill the gap in Event-B language - a missing support of a syntax for the direct definition of structured types. Some of the industrial partners expressed a desire to have this missing feature in Event-B, that would allow them to define their own structured types such as records or classes. Theoretically these structures could be modelled with existing Event-B capabilities via projection functions. Backed up by a refined theoretical proposal Records plug-in was developed to extend the standard Event-B notation with requested capability.
| + | == An Array Type Definition == |
| | + | <div id="fig:Extension with an Array Type"> |
| | + | <br/> |
| | + | [[Image:ArrayDef.png|center||caption text]] |
| | + | <center>'''Figure 2''': Array Definition</center> |
| | + | <br/> |
| | + | </div> |
| | | | |
| − | === Choices / Decisions ===
| + | The array operator notation is defined in the expression array(s: P(T)); and the semantics is defined in the direct definition. arrayN constrains the arrays to be of fixed length. Array lookup, update, and constructor operators are subsequently defined. In the next step we need to define any translations required to implement the array in code. |
| | | | |
| − | On the Core Rodin Platform side, implementing mathematical extensions required to make some parts of the code extensible, that were not designed to be so, namely the lexer and the parser. We were using tools that automatically generated them from a fixed grammar description, so we had to change to other technologies. A [http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser study] has been made on available technologies. The Pratt algorithm was selected for its adequation with the purpose and it did not have the drawbacks of other technologies:
| + | == Translation Rules == |
| − | * foreign language integration
| |
| − | * overhead due to over generality
| |
| | | | |
| − | After a mocking up phase to verify feasibility, the Pratt algorithm has been confirmed as the chosen option and implemented in the Rodin Platform.
| + | <div id="Translation Rules for the Array Type"> |
| | + | <br/> |
| | + | [[Image:ArrayTrans.png|center||caption text]] |
| | + | <center>'''Figure 3''': Translation Rules for the Array Type</center> |
| | + | <br/> |
| | + | </div> |
| | | | |
| − | Besides, we wanted to set up a way to publish and share theories for Rodin users, in order to constitute a database of pre-built theories for everyone to use and contribute. This has been realised by adding a new tracker on SourceForge site ([http://sourceforge.net/tracker/?group_id=108850&atid=1558661]).
| + | Figure 3 shows the Ada translation; beginning with the meta-variable definitions that are used for pattern matching in the translation rules. Each of the operators; ''newArray'', and ''update'', and an expression using the ''lookup'' operator, are mapped to their implementations on the right hand side of the rule. The ''Type Rules'' section describes the implementation's description of the ''arrayN'' type. |
| − | | |
| − | The Theory plug-in contributes a theory construct to the Rodin database. Theories were used in the Rule-based Prover (before it was discontinued) as a placeholder for rewrite rules. Given the usability advantages of the theory component, it was decided to use it to define mathematical extensions (new operators and new datatypes). Another advantage of using the theory construct is the possibility of using proof obligations to ensure that the soundness of the formalism is not compromised. Proof obligations are generated to validate any properties of new operators (e.g., associativity). With regards to prover extensions, it was decided that the Theory plug-in inherits the capabilities to define and validate rewrite rules from the Rule-based Prover. Furthermore, support for a simple yet powerful subset of inference rules is added, and polymorphic theorems can be defined within the same setting. Proof obligations are, again, used as a filter against potentially unsound proof rules.
| |
| − | | |
| − | Records plug-in required the extension of the Rodin database with the new constructs to support structured types. On the other hand the Event-B language itself did not support extension at that time. For that reason the decision was made to address extensibility problem at the lowest level possible, which was Rodin database, but to model structured types using standard Event-B notation at the level below. The translation from extended to standard syntax has been entrusted to the static checker, that was also extended for this purpose. Thus the plug-in provides the users with notation for record declarations and extensions in unchecked models, but the checked versions operate with standard Event-B constructs.
| |
| − | | |
| − | === Available Documentation ===
| |
| − |
| |
| − | * Pre-studies (states of the art, proposals, discussions).
| |
| − | ** [http://deploy-eprints.ecs.soton.ac.uk/216/ ''Proposals for Mathematical Extensions for Event-B'']
| |
| − | ** [http://deploy-eprints.ecs.soton.ac.uk/251/ ''Mathematical Extension in Event-B through the Rodin Theory Component'']
| |
| − | ** [http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser#Design_Alternatives]
| |
| − | ** [http://wiki.event-b.org/index.php/Structured_Types ''Theoretical Description of Structured Types'']
| |
| − | * Technical details (specifications).
| |
| − | ** [http://wiki.event-b.org/index.php/Mathematical_Extensions]
| |
| − | ** [http://wiki.event-b.org/index.php/Constrained_Dynamic_Lexer]
| |
| − | ** [http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser]
| |
| − | ** [http://wiki.event-b.org/index.php/Theory_Plug-in]
| |
| − | ** [http://wiki.event-b.org/index.php/Records_Extension ''Records Extension Documentation'']
| |
| − | * Teaching materials (tutorials).
| |
| − | * User's guides.
| |
| − | ** [http://wiki.event-b.org/images/Theory_UM.pdf]
| |
| − | | |
| − | === Planning ===
| |
| − | This paragraph shall give a timeline and current status (as of 28 Jan 2011).
| |
| − | | |
| − | {{TODO|What will remain to do after Rodin 2.1 ?}}
| |
| − | | |
| − | [[Category:D32 Deliverable]]
| |
Defining Translations Using The Theory Plug-in
The theory plug-in is used to add mathematical extensions to Rodin. The theories are created, and deployed, and can then be used in any models in the workspace. When dealing with implementation level models, such as in Tasking Event-B, we need to consider how to translate newly added types and operators into code. We have augmented the theory interface with a Translation Rules section. This enables a user to define translation rules that map Event-B formulas to code.
Translation Rules
Figure 1: Translation Rules
Figure 1 shows the interface, and some translations rules of the mapping to Ada.
The theory is given a name, and may import some other theories. Type parameters can be added, and we use them here to type the meta-variables. The meta-variable a is restricted to be an integer type, but meta-variable c can be any type. Meta-variables are used in the translator rules for pattern matching.
Translator rules are templates, which are used in pattern matching. Event-B formulas are defined on the left hand side of the rule, and the code to be output (as text) appears on the right hand side of the matching rule. During translation an abstract syntax tree (AST) representation of the formula is used. The theory plug-in attempts to match the formulas in the rules with each syntactic element of the AST. As it does so it builds the textual output as a string, until the whole AST has been successfully matched. When a complete tree is matched, the target code is returned. If the AST is not matched, a warning is issued, and a string representation of the original formula is returned.
Type Rules for Code Generation
The type rules section, shown in Figure 1, is where the relationship is defined, between Event-B types and the type system of the implementation.
Adding New (implementation-level) Types
When we are working at abstraction levels close to the implementation level, we may make an implementation decision which requires the introduction of a new type to the development. We give an example of our approach, where we add a new array type, shown in Figure 2, and then define its translation to code.
An Array Type Definition
Figure 2: Array Definition
The array operator notation is defined in the expression array(s: P(T)); and the semantics is defined in the direct definition. arrayN constrains the arrays to be of fixed length. Array lookup, update, and constructor operators are subsequently defined. In the next step we need to define any translations required to implement the array in code.
Translation Rules
Figure 3: Translation Rules for the Array Type
Figure 3 shows the Ada translation; beginning with the meta-variable definitions that are used for pattern matching in the translation rules. Each of the operators; newArray, and update, and an expression using the lookup operator, are mapped to their implementations on the right hand side of the rule. The Type Rules section describes the implementation's description of the arrayN type.
