Difference between pages "The Use of Theories in Code Generation" and "User:Nicolas/Collections/ADVANCE D3.4 General Platform Maintenance"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Andy
 
imported>Nicolas
 
Line 1: Line 1:
−
= Defining Translations Using The Theory Plug-in =
+
This part describes the general maintenance performed on the Rodin toolset within the last year of the ADVANCE project. As the maintenance is a task that concerns the whole toolset, and to ease the reading of this part of the deliverable, the maintenance section has been decomposed in a list of subsections corresponding to scopes of the toolset. All these subsections maintain the template previously defined in the introduction.
−
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==
 
−
Code generation rules are specified in a theory file, which is created using the Theory plug-in. Figure 1 shows a pretty print of some of the translations rules that have been specified for the Ada code generator. In the figure we can see that 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. For instance, the meta-variable ''a'' is restricted to be an integer type, but meta-variable ''c'' can be any unspecified type, ''Q''. Meta-variables are used in the translator rules for pattern matching.
 
  
−
<div id="fig:Translation Rules">
+
== Core Rodin platform ==
−
<br/>
 
−
[[Image:TheoryCGRules.png|center||caption text]]
 
−
<center>'''Figure 1''': Translation Rules</center>
 
−
<br/>
 
−
</div>
 
  
−
Translator rules are templates. They are used in a pattern matching algorithm, in the Theory plug-in, invoked by the code generator. 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.
+
=== Overview ===
 +
During the last period of the ADVANCE project, the following versions of the Rodin platform have been released:
 +
* 3.0.0 (2014-03-20)
 +
* 3.0.1 (2014-06-11)
 +
* 3.1.0 (2014-11-??)
  
−
== Type Rules for Code Generation ==
+
The main part of the work was targeting improvements of
 +
* stability of the platform,
 +
* prover capabilities,
 +
* theory support
  
−
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.
+
Other running tasks consisted in answering questions on mailing lists, and processing bug tickets and feature requests.
  
−
= Adding New (implementation-level) Types =
+
=== Motivations / Decisions ===
−
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 ==
+
The core API has been improved.
−
<div id="fig:Extension with an Array Type">
+
The HMI has been upgraded to recent Eclipse.
−
<br/>
+
Bug fixes, increased stability.
−
[[Image:ArrayDef.png|center||caption text]]
+
Rodin Editor stability.
−
<center>'''Figure 2''': Array Definition</center>
+
Proof rules (SIMP_EMPTY_PARTITION and SIMP_SINGLE_PARTITION)
−
<br/>
+
Port to Java7.
−
</div>
+
Developer-friendly archive (Rodin as a target platform).
 +
Tactic Profile Dropdown from Proof Control.
 +
Better support for theories.
  
−
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.
+
{{TODO}}
  
−
== Translation Rules ==
+
=== Available Documentation ===
 +
The release notes, that appear and are maintained on the wiki, and that accompany each release, give useful information about the changes introduced by each. Moreover, two web trackers list and detail the known bugs and open feature requests:
 +
* a sourceforge bug tracker,<ref>http://sourceforge.net/p/rodin-b-sharp/bugs/</ref>
 +
* a sourceforge feature requests tracker.<ref>http://sourceforge.net/p/rodin-b-sharp/feature-requests/</ref>
  
−
<div id="Translation Rules for the Array Type">
+
{{TODO}}
−
<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.
+
=== Conclusion ===
 +
 
 +
{{TODO}}
 +
 
 +
== UML-B Improvements ==
 +
 
 +
=== Overview ===
 +
{{TODO}}
 +
 
 +
=== Motivations / Decisions ===
 +
{{TODO}}
 +
 
 +
=== Available Documentation ===
 +
{{TODO}}
 +
 
 +
=== Conclusion ===
 +
{{TODO}}
 +
 
 +
== ProR/Rodin Integration Plugin ==
 +
 
 +
=== Overview ===
 +
 
 +
ProR is a tool for working with requirements in natural language. It is part of the Eclipse Requirements Modeling Framework (RMF).<ref>http://www.eclipse.org/rmf/</ref> The goal of the ProR/Rodin integration plugin is to bring two complimentary fields of research, requirements engineering and formal modelling, closer together. The ProR/Rodin integration plugin supports the user by maintaining a traceability between natural language requirements and Event-B models.
 +
 
 +
A requirements Meta-Model for the WP-1 and WP-2 industrial case studies has been developed during the last period of the ADVANCE project.
 +
Beside this, general improvements, such as usability improvements have been made on the ProR/Rodin integration plugin during the last period of the ADVANCE project.
 +
 
 +
=== Motivations / Decisions ===
 +
 
 +
The ProR/Rodin integration plugin provides a default Meta-Model for requirements documents. However, this Meta-Model does not support all specific needs and characteristics of the industrial case studies.
 +
As a consequence, we decided to create a new requirements Meta-Model that supports the specific needs of both industrial case studies.
 +
 
 +
=== Available Documentation ===
 +
 
 +
* ''A Method and Tool for Tracing Requirements into Specifications''.<ref name="req1ref">http://www.stups.uni-duesseldorf.de/mediawiki/images/e/ec/Pub-HalJasLad2013.pdf</ref> Accepted for Science of Computer Programming.
 +
* ''Requirements Traceability between Textual Requirements and Formal Models Using ProR''<ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/LadenbergerJastram_iFMABZ2012</ref>. The paper has been accepted for iFM'2012 & ABZ'2012.
 +
 
 +
* A Tutorial for the Rodin/ProR integration<ref>http://wiki.event-b.org/index.php/ProR</ref> can be found on the Event-B wiki.
 +
* The User Guide<ref>http://wiki.eclipse.org/RMF/User_Guide</ref> contains additional tutorials for ProR.
 +
 
 +
=== Conclusion ===
 +
 
 +
The customized Meta-Models facilitated the requirements maintenance process of both industrial case studies. Moreover, the new Meta-Model is expandable so that new features can be easily added later in the project.
 +
 
 +
== Camille ==
 +
 
 +
=== Overview ===
 +
The Camille plug-in provides a textual editor for Rodin. This editor provides the same look and feel as a typical Eclipse text editor, including features most text editors provide, such as copy, paste, syntax highlighting and code completion.
 +
 
 +
During the last period of the ADVANCE project, three new versions of Camille have been released:
 +
* 3.0.0 - Initial release for version 3 of the Core Rodin platform. This release has been based on Camille 2.1.4.
 +
* 3.0.1 - Port of the changes done in Camille 2.2.0 to version 3. This includes theorems in guards as well as other bugfixes. See D3.3 for details.
 +
* 3.0.2 - Camille's structure parser has been moved to ProB's parser library. A fully automatic build process featuring continuous integration has been set up. This is the first release build by it.
 +
 
 +
One of the main goals of the last period was the support of Rodin's extensibility in Camille.
 +
 
 +
=== Motivations / Decisions ===
 +
'''Move to Git / GitHub'''
 +
 
 +
The source files for Camille have been moved from the old Rodin SVN repository to their own repository at GitHub.
 +
The old source files have been marked deprecated.
 +
Furthermore, the move to GitHub allows us to use GitHub's infrastructure for bug tracking and feature requests.
 +
We moved old feature requests from the wiki pages to the bug / feature tracking systems at GitHub.
 +
 
 +
'''Build Process'''
 +
 
 +
Before version 3.0.2 was released, the Camille build was mostly done by hand.
 +
This turned out to be slowing down development during the last period of the ADVANCE project.
 +
Starting with release 3.0.2 we completely revamped the build process.
 +
Camille is now build automatically on each commit using a Jenkins continuous integration server <ref>http://www.jenkins-ci.org</ref>.
 +
This facilitates the build as well as the release process for Camille.
 +
Furthermore, it should ease collaborative development.
 +
 
 +
'''Move Structure Parser to ProB's Parser Library'''
 +
 
 +
Camille's internal parser for the structure of Event-B machines and contexts has been split off of Camille and moved to ProB's general parsers library.
 +
This effectively renders the parser and external dependency for Camille and further decouples core, ui and parsers.
 +
Externalising the parser is the first step to making Camille more modular in oder to be able to replace the parser by the upcoming block parser.
 +
In addition, externalising the parser makes it available for other projects as well.
 +
 
 +
=== Available Documentation ===
 +
 
 +
* ''Architectures for an Extensible Text Editor for Rodin''.<ref name="Architectures_for_an_Extensible_Text_Editor_for_Rodin">http://www.stups.uni-duesseldorf.de/mediawiki/images/0/0a/Pub-Weigelt2012.pdf</ref> Bachelor thesis analysing the problem and discussing possible solutions.
 +
* An earlier version of the thesis has been published as a technical report<ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/Weigelt2012></ref> that has been discussed on the Roding Developers Mailing List and the ADVANCE Progress Meeting in May 2012 in Paris.
 +
* ''Camille GitHub Repository and Bugtracker'': https://github.com/hhu-stups/camille
 +
* ''Camille Wiki'': http://wiki.event-b.org/index.php/Camille_Editor
 +
 
 +
=== Conclusion ===
 +
Sadly, Camille still has the drawback of not supporting extensibility. It only supports the core Event-B language and plug-in-specific additions are simply ignored. Consequently, users have to switch back to Rodin's native Editor to edit plug-in-specific modelling extensions. The changes and improvements to the development process performed in the last period should finally allow for a new and completely overhauled version of Camille to be implemented.
 +
 
 +
== References ==
 +
<references/>

Revision as of 13:29, 3 November 2014

This part describes the general maintenance performed on the Rodin toolset within the last year of the ADVANCE project. As the maintenance is a task that concerns the whole toolset, and to ease the reading of this part of the deliverable, the maintenance section has been decomposed in a list of subsections corresponding to scopes of the toolset. All these subsections maintain the template previously defined in the introduction.

Core Rodin platform

Overview

During the last period of the ADVANCE project, the following versions of the Rodin platform have been released:

  • 3.0.0 (2014-03-20)
  • 3.0.1 (2014-06-11)
  • 3.1.0 (2014-11-??)

The main part of the work was targeting improvements of

  • stability of the platform,
  • prover capabilities,
  • theory support

Other running tasks consisted in answering questions on mailing lists, and processing bug tickets and feature requests.

Motivations / Decisions

The core API has been improved. The HMI has been upgraded to recent Eclipse. Bug fixes, increased stability. Rodin Editor stability. Proof rules (SIMP_EMPTY_PARTITION and SIMP_SINGLE_PARTITION) Port to Java7. Developer-friendly archive (Rodin as a target platform). Tactic Profile Dropdown from Proof Control. Better support for theories.

TODO

Available Documentation

The release notes, that appear and are maintained on the wiki, and that accompany each release, give useful information about the changes introduced by each. Moreover, two web trackers list and detail the known bugs and open feature requests:

  • a sourceforge bug tracker,[1]
  • a sourceforge feature requests tracker.[2]

TODO

Conclusion

TODO

UML-B Improvements

Overview

TODO

Motivations / Decisions

TODO

Available Documentation

TODO

Conclusion

TODO

ProR/Rodin Integration Plugin

Overview

ProR is a tool for working with requirements in natural language. It is part of the Eclipse Requirements Modeling Framework (RMF).[3] The goal of the ProR/Rodin integration plugin is to bring two complimentary fields of research, requirements engineering and formal modelling, closer together. The ProR/Rodin integration plugin supports the user by maintaining a traceability between natural language requirements and Event-B models.

A requirements Meta-Model for the WP-1 and WP-2 industrial case studies has been developed during the last period of the ADVANCE project. Beside this, general improvements, such as usability improvements have been made on the ProR/Rodin integration plugin during the last period of the ADVANCE project.

Motivations / Decisions

The ProR/Rodin integration plugin provides a default Meta-Model for requirements documents. However, this Meta-Model does not support all specific needs and characteristics of the industrial case studies. As a consequence, we decided to create a new requirements Meta-Model that supports the specific needs of both industrial case studies.

Available Documentation

  • A Method and Tool for Tracing Requirements into Specifications.[4] Accepted for Science of Computer Programming.
  • Requirements Traceability between Textual Requirements and Formal Models Using ProR[5]. The paper has been accepted for iFM'2012 & ABZ'2012.
  • A Tutorial for the Rodin/ProR integration[6] can be found on the Event-B wiki.
  • The User Guide[7] contains additional tutorials for ProR.

Conclusion

The customized Meta-Models facilitated the requirements maintenance process of both industrial case studies. Moreover, the new Meta-Model is expandable so that new features can be easily added later in the project.

Camille

Overview

The Camille plug-in provides a textual editor for Rodin. This editor provides the same look and feel as a typical Eclipse text editor, including features most text editors provide, such as copy, paste, syntax highlighting and code completion.

During the last period of the ADVANCE project, three new versions of Camille have been released:

  • 3.0.0 - Initial release for version 3 of the Core Rodin platform. This release has been based on Camille 2.1.4.
  • 3.0.1 - Port of the changes done in Camille 2.2.0 to version 3. This includes theorems in guards as well as other bugfixes. See D3.3 for details.
  • 3.0.2 - Camille's structure parser has been moved to ProB's parser library. A fully automatic build process featuring continuous integration has been set up. This is the first release build by it.

One of the main goals of the last period was the support of Rodin's extensibility in Camille.

Motivations / Decisions

Move to Git / GitHub

The source files for Camille have been moved from the old Rodin SVN repository to their own repository at GitHub. The old source files have been marked deprecated. Furthermore, the move to GitHub allows us to use GitHub's infrastructure for bug tracking and feature requests. We moved old feature requests from the wiki pages to the bug / feature tracking systems at GitHub.

Build Process

Before version 3.0.2 was released, the Camille build was mostly done by hand. This turned out to be slowing down development during the last period of the ADVANCE project. Starting with release 3.0.2 we completely revamped the build process. Camille is now build automatically on each commit using a Jenkins continuous integration server [8]. This facilitates the build as well as the release process for Camille. Furthermore, it should ease collaborative development.

Move Structure Parser to ProB's Parser Library

Camille's internal parser for the structure of Event-B machines and contexts has been split off of Camille and moved to ProB's general parsers library. This effectively renders the parser and external dependency for Camille and further decouples core, ui and parsers. Externalising the parser is the first step to making Camille more modular in oder to be able to replace the parser by the upcoming block parser. In addition, externalising the parser makes it available for other projects as well.

Available Documentation

  • Architectures for an Extensible Text Editor for Rodin.[9] Bachelor thesis analysing the problem and discussing possible solutions.
  • An earlier version of the thesis has been published as a technical report[10] that has been discussed on the Roding Developers Mailing List and the ADVANCE Progress Meeting in May 2012 in Paris.
  • Camille GitHub Repository and Bugtracker: https://github.com/hhu-stups/camille
  • Camille Wiki: http://wiki.event-b.org/index.php/Camille_Editor

Conclusion

Sadly, Camille still has the drawback of not supporting extensibility. It only supports the core Event-B language and plug-in-specific additions are simply ignored. Consequently, users have to switch back to Rodin's native Editor to edit plug-in-specific modelling extensions. The changes and improvements to the development process performed in the last period should finally allow for a new and completely overhauled version of Camille to be implemented.

References

  1. ↑ http://sourceforge.net/p/rodin-b-sharp/bugs/
  2. ↑ http://sourceforge.net/p/rodin-b-sharp/feature-requests/
  3. ↑ http://www.eclipse.org/rmf/
  4. ↑ http://www.stups.uni-duesseldorf.de/mediawiki/images/e/ec/Pub-HalJasLad2013.pdf
  5. ↑ http://www.stups.uni-duesseldorf.de/w/Special:Publication/LadenbergerJastram_iFMABZ2012
  6. ↑ http://wiki.event-b.org/index.php/ProR
  7. ↑ http://wiki.eclipse.org/RMF/User_Guide
  8. ↑ http://www.jenkins-ci.org
  9. ↑ http://www.stups.uni-duesseldorf.de/mediawiki/images/0/0a/Pub-Weigelt2012.pdf
  10. ↑ http://www.stups.uni-duesseldorf.de/w/Special:Publication/Weigelt2012>
Retrieved from ‘https://wiki.event-b.org/index.php?title=The_Use_of_Theories_in_Code_Generation&oldid=10850’