Difference between pages "D32 Teamwork" and "The Use of Theories in Code Generation"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Vitaly
 
imported>Andy
 
Line 1: Line 1:
−
=== Overview ===
+
= Defining Translations Using The Theory Plug-in =
−
Teamwork consists of
+
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.
−
* SVN enabling teamwork plug-in
+
== Translation Rules==
−
* Decomposition methods
+
<div id="fig:Translation Rules">
 +
<br/>
 +
[[Image:TheoryCGRules.png|center||caption text]]
 +
<center>'''Figure 1''': Translation Rules</center>
 +
<br/>
 +
</div>
  
 +
Figure 1 shows the interface, and some translations rules of the mapping to Ada.
  
−
* Team-working Plug-in is a new feature developed by University of Southampton in request to industrial partners who required support of Rodin project management and team development using Subversion system. Having this support would bring the benefit of centralised model storage and versioning, as well as parallel development. Despite a few functional limitations, derived by specific nature of the Rodin projects, the implemented plug-in gives support for Subversion-based project sharing and collaborative development.
+
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.
  
−
* Decomposition plug-in was developed by Renato Silva (University of Southampton), Carine Pascal (Systerel) based on the initial prototype developed by T.S. Hoang (ETH Zurich). This plug-in was developed as an answer to models that became to big to be handled with a large number of events, a large number of variables and consequently a large number of proof obligations over several levels of refinements. There are two kinds of decomposition available: ''shared event'' (studied initially by Michael Butler) and ''shared variable'' (studied initially by Jean-Raymond Abrial). Both decomposition styles allow the partition of the original model into (smaller) sub-models. The sub-models are expected to be easier to handle, with less variables and less events and less proof obligations. This partition is done in a way that the sub-models (also referred as sub-components) are independent of each other and therefore can be refined individually. As a consequence, each sub-model can be further developed by different people allowing teamwork development.
+
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 teamwork are:
 
−
* SVN Teamwork
 
−
: The reason to support compatibility of Rodin projects with Subversion was to allow Rodin users to share their projects and work on them together, as well as have the benefits of versioning and revision control, provided by the SVN system. It was difficult to work on models in parallel and manage changes made by different parties, especially for big and complex models. Other users expressed a concern on safety aspect of collaborative development, thus pointing out the benefits of centralised repository storage of the models under development on SVN.
 
  
−
=== Choices / Decisions ===
+
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.
−
* SVN Teamwork
 
−
: The desired objective of a plug-in that would bring support for Subversion in Rodin was to make a Rodin project compatible with standard SVN interface. Due to nature of the Rodin resource management, in particular the use of Rodin database and non-XMI serialisation, it turned out a hard task. A solution to this difficulty was to provide an alternative serialisation method, that would be compatible with Subversion interface. XMI serialisation has been chosen in the final plug-in, which together with Event-B EMF framework provides a shareable copy of the resources of a Rodin project and takes care of synchronisation between two.
 
  
−
=== Available Documentation ===
+
= Adding New (implementation-level) Types =
−
* SVN Team-based development documentation<ref>http://wiki.event-b.org/index.php/Team-based_development</ref>
+
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.
  
−
=== Planning ===
+
== An Array Type Definition ==
−
This paragraph shall give a timeline and current status (as of 28 Jan 2011).
+
<div id="fig:Extension with an Array Type">
 +
<br/>
 +
[[Image:ArrayDef.png|center||caption text]]
 +
<center>'''Figure 2''': Array Definition</center>
 +
<br/>
 +
</div>
  
−
=References=
+
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.
−
<references/>
 
  
−
[[Category:D32 Deliverable]]
+
== Translation Rules ==
 +
 
 +
<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>
 +
 
 +
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.

Revision as of 15:51, 15 May 2012

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


caption text
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


caption text
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


caption text
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.

Retrieved from ‘https://wiki.event-b.org/index.php?title=D32_Teamwork&oldid=10253’