Difference between pages "Index Query" and "The Use of Theories in Code Generation"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Laurent
m
 
imported>Andy
 
Line 1: Line 1:
−
==Purpose==
+
= 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>
  
−
The purpose of the Rodin index manager is to store in a uniform way the entities that are declared in the database together with their occurrences. This central repository of declarations and occurrences allows for fast implementations of various refactoring mechanisms (such as renaming) and support for searching models or browsing them.
+
Figure 1 shows the interface, and some translations rules of the mapping to Ada.
  
−
==Performing queries==
+
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.
  
−
The indexer contents are not directly accessible to other plug-ins. Queries are sent through a {{class|IIndexQuery}} object provided by the RodinCore plug-in.
+
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.
  
−
===What to query ?===
+
== Type Rules for Code Generation ==
  
−
Two types of information can be queried:
+
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.
−
* declarations ({{class|IDeclaration}})
 
−
* occurrences ({{class|IOccurrence}})
 
  
−
A declaration is the unique identifier of an entity in the index repository.
+
= Adding New (implementation-level) Types =
−
It consists in a handle of the declared element itself plus its user-defined name.
+
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.
−
Every occurrence refers to one single declaration.
 
  
−
Several query types can be performed, depending on the starting point:
+
== An Array Type Definition ==
−
* getting the declaration of a given element (as {{class|IInternalElement}})
+
<div id="fig:Extension with an Array Type">
−
* getting the declarations of elements that match a given user-defined name (as {{class|String}}) in a given file
+
<br/>
−
* getting the declarations of elements that occur, or could occur, in a given file
+
[[Image:ArrayDef.png|center||caption text]]
−
* getting occurrences of a given declaration (this declaration having been retrieved from a previous query)
+
<center>'''Figure 2''': Array Definition</center>
−
* getting occurrences of a given declaration using propagation (see [[#Propagation|Propagation]] hereafter )
+
<br/>
 +
</div>
  
−
Thus, a declaration is the key to retrieve occurrences.
+
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.
  
−
As the result might be too coarse, queries can be filtered out using various criterias (see {{class|IIndexQuery}} interface for more details).
+
== Translation Rules ==
  
−
===Occurrences===
+
<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>
  
−
An occurrence ({{class|IOccurrence}}) describes a location ({{class|IRodinLocation}}) and a kind of occurrence ({{class|IOccurrenceKind}}) of an element (referred to through its {{class|IDeclaration}}).
+
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.
−
For example, in Event-B, an occurrence could be:
 
−
 
 
−
; location: in {{class|IAxiom}} 'a' (handle), in the PREDICATE_ATTRIBUTE, between characters 7 and 12
 
−
; kind: REFERENCE
 
−
; declaration: the {{class|ICarrierSet}} 's' (handle), named "set1"
 
−
 
 
−
Occurrence kinds are contributed by indexers, no kinds are defined at the indexing system level.
 
−
See more in [[Event-B Indexers]].
 
−
 
 
−
===Propagation===
 
−
 
 
−
Propagation is a way to get occurrences of several declarations, starting from one single declaration. In particular, it addresses cases where various declarations represent the same entity. The problem is that each declaration has separate occurrences. The propagation mechanism allows to get all occurrences of the entity, whatever the underlying declaration.
 
−
 
 
−
For example, in Event-B, a variable can be redeclared in a refining machine. In the index repository, each variable has a separate declaration and separate occurrences. However, it might be interesting in some cases to consider occurrences of the concrete variable as a subset of occurrences of the abstract one. The concept here is to 'propagate' the query about the abstract variable to occurrences of the concrete one. This is achievable in this case thanks to event-B propagators.
 
−
 
 
−
See more in [[Event-B Indexers#Propagation|Event-B Indexers Propagation]].
 
−
 
 
−
===Getting a valid result===
 
−
 
 
−
The indexing system data is constantly evolving, as long as files get modified. Furthermore, as indexing is performed as a background operation, one cannot guess whether the indexing has completed or not. The system may also be updating its data, making it temporarily incoherent. Thus, the problem arises to ensure that the data is valid and up-to-date.
 
−
 
 
−
To that end, a method is provided by the {{class|IIndexQuery}}, that blocks the current thread until all planned files are indexed. Requests performed after that will thus return a valid result and benefit from the most up-to-date version of the data.
 
−
 
 
−
==Query Examples==
 
−
 
 
−
Here are a few examples of index queries. They are all implicitly preceded by the following code
 
−
 
 
−
  final IIndexQuery query = RodinCore.makeIndexQuery();
 
−
  query.waitUpToDate();
 
−
 
 
−
that creates the query object and waits until the index becomes up-to-date.
 
−
 
 
−
===Occurrences of an element===
 
−
 
 
−
Input Data:
 
−
* a handle 'var' of an IVariable
 
−
 
 
−
To get its declaration
 
−
 
 
−
final IDeclaration declVar = query.getDeclaration(var);
 
−
 
 
−
Remember to check for a null return value.
 
−
 
 
−
From that declaration, the user-defined name of the variable can be retrieved
 
−
 
 
−
final String userDefinedName = declVar.getName();
 
−
 
 
−
To get the occurrences of 'var'
 
−
 
 
−
final Set<IOccurrence> occurrences = query.getOccurrences(declVar);
 
−
 
 
−
===Homonyms in a file===
 
−
 
 
−
Input Data:
 
−
* a handle 'file' of an {{class|IRodinFile}}
 
−
* a name "foo"
 
−
 
 
−
Goal:
 
−
getting declarations of all elements named "foo" that occur in 'file'
 
−
 
 
−
First, all declarations of all indexed elements that occur in 'file' are retrieved.
 
−
Then a query filter on the name is used.
 
−
 
 
−
final Set<IDeclaration> declarations = query.getDeclarations(file);
 
−
query.filterName(declarations, "foo");
 
−
 
 
−
At the end, 'declarations' contains the declarations of all elements named "foo" occurring in 'file'.
 
−
 
 
−
===Parameters of an event===
 
−
 
 
−
Input Data:
 
−
* a handle 'file' of an {{class|IRodinFile}}
 
−
* a handle 'evt1' of an {{class|IEvent}}
 
−
 
 
−
Goal:
 
−
getting the declarations of all parameters of 'evt1'
 
−
 
 
−
<pre>
 
−
final Set<IDeclaration> declarations = query.getDeclarations(file);
 
−
query.filterType(declarations, IParameter.ELEMENT_TYPE);
 
−
 
 
−
final Set<IOccurrence> occurrences = query.getOccurrences(declarations);
 
−
query.filterKind(occurrences, EventBPlugin.DECLARATION);
 
−
 
 
−
final IInternalLocation evt1Location = RodinCore.getInternalLocation(evt1);
 
−
query.filterLocation(occurrences, evt1Location);
 
−
 
 
−
final Set<IDeclaration> paramsOfEvt1 = query.getDeclarations(occurrences);
 
−
</pre>
 
−
 
 
−
We first get all declarations of elements that occur in 'file', and we filter them so as to keep only declarations of parameters.
 
−
 
 
−
We then get all occurrences of those parameters. We want parameters that have a DECLARATION occurrence in 'evt1'. To that aim, two filters are successively applied to the occurrences.
 
−
 
 
−
Finally we get the declarations ({{class|IDeclaration}}) associated with the filtered occurrences.
 
−
 
 
−
===Query with propagation===
 
−
 
 
−
Input Data:
 
−
* a handle 'var' to a {{class|IVariable}}
 
−
 
 
−
Goal:
 
−
getting all occurrences of 'var' including occurrences in machines that redeclare 'var'.
 
−
 
 
−
<pre>
 
−
final IDeclaration declaration = query.getDeclaration(var);
 
−
if (declaration != null) {
 
−
  final Set<IOccurrence> propagatedOccs = query.getOccurrences(declaration,
 
−
        EventBPlugin.getIdentifierPropagator());
 
−
  ...
 
−
}
 
−
</pre>
 
−
 
 
−
Here, we start from the 'var' handle but of course, we could also have obtained its declaration by any other way (see other examples).
 
−
 
 
−
Returned occurrences can then be filtered, as usual.
 
−
 
 
−
[[Category:Design]]
 

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=Index_Query&oldid=10253’