Difference between revisions of "Introduction (How to extend Rodin Tutorial)"

From Event-B
Jump to navigationJump to search
imported>Pascal
imported>Tommy
 
(20 intermediate revisions by 2 users not shown)
Line 1: Line 1:
−
{{Navigation|Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]] | Next= [[Creating_a_new_plugin_using_eclipse_(How_to_extend_Rodin_Tutorial)|Creating our plugin]]}}
+
{{Navigation|Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]] | Next= [[Creating_a_new_plugin_using_eclipse_(How_to_extend_Rodin_Tutorial)|Creating our plug-in]]}}
  
−
In this tutorial, we will focus on the extension of the Rodin platform by adding plugins. This mechanism inherits from Eclipse extension mechanism (see paragraph about Extension points and Extensions below).
+
In this tutorial, we will focus on the extension of the Rodin platform by adding plug-ins. This mechanism inherits from Eclipse extension mechanism (see paragraph about Extension points and Extensions below).
 
As we will discuss here about the provided Rodin extensibility possibilities, reading this tutorial implies that you have basic knowledge in Event-B, and are familiar with Java programming language.<br>
 
As we will discuss here about the provided Rodin extensibility possibilities, reading this tutorial implies that you have basic knowledge in Event-B, and are familiar with Java programming language.<br>
  
 
== Extension Points and Extensions ==
 
== Extension Points and Extensions ==
 
Rodin uses Eclipse extensibility mechanism. This mechanism is based on the notions of "'''extension points'''" and "'''extensions'''".<br>
 
Rodin uses Eclipse extensibility mechanism. This mechanism is based on the notions of "'''extension points'''" and "'''extensions'''".<br>
−
A plugin that wants to offer functionnalities (e.g. extension services) defines an extension point. An extension point is a sort of contract given to other plugins, to use (e.g. extend) those provided extension services. This contract is expressed in XML. A concrete example of extension service is offered by the plugin <tt>org.rodinp.core</tt> to register new elements in Rodin database.
+
A plug-in that wants to offer functionalities (e.g. extension services) defines an extension point. An extension point is a sort of contract given to other plug-ins, to use (e.g. extend) those provided extension services. This contract is expressed in XML. A concrete example of extension service is offered by the plug-in <tt>org.rodinp.core</tt> to register new elements in Rodin database.
−
Moreover, a plugin defining an extension point will manage all contributions (that we call extensions), through its lifecycle. In the case of Rodin Database, all extensions of the database (added elements, added attributes, etc.) are managed by the plugin <tt>org.rodinp.core</tt>.  
+
Moreover, a plug-in defining an extension point will manage all contributions (that we call extensions), through its lifecycle. In the case of Rodin Database, all extensions of the database (added elements, added attributes, etc.) are managed by the plug-in <tt>org.rodinp.core</tt>.  
  
−
To extend Rodin, we are in the situation where plugins (callers) want to use the extension services offered by one plugin (e.g. the callee that defines an extension point).
+
To extend Rodin, we are in the situation where plug-ins (callers) want to use the extension services offered by one plug-in (e.g. the callee that defines an extension point).
 
[[Image:Extend_Rodin_Tuto_Extension.png|center|300px]]
 
[[Image:Extend_Rodin_Tuto_Extension.png|center|300px]]
  
−
Thus, we will define a caller (a new plugin) that accepts one or more contracts with the Rodin platform. To accept such contract, a caller has to specify its dependency to the callee, and define one (resp. many) extensions, which conforms to an (resp. corresponding) imported extension point. The terms of the contract are often given through required interfaces, which defines a protocol to use the provided extension services. In other words, the results of the computation performed in caller's code need to conform to an interface defined by the callee (the extension service provider). Sometimes, the callee defines additional interfaces to give the callers a view on the managed contributions.<br>
+
Thus, we will define a caller (a new plug-in) that accepts one or more contracts with the Rodin platform. To accept such contract, a caller has to specify its dependency to the callee, and define one (resp. many) extensions, which conforms to an (resp. corresponding) imported extension point. The terms of the contract are often given through required interfaces, which defines a protocol to use the provided extension services. In other words, the results of the computation performed in caller's code need to conform to an interface defined by the callee (the extension service provider). Sometimes, the callee defines additional interfaces to give the callers a view on the managed contributions.<br>
 
In this tutorial, we will define new callers and use the contracts offered by the Rodin platform.
 
In this tutorial, we will define new callers and use the contracts offered by the Rodin platform.
  
−
For more information about extension points, please refer to this article : [[http://www.eclipse.org/resources/resource.php?id=383]].
+
For more information about extension points, please refer to this article: [http://www.eclipse.org/resources/resource.php?id=383 Getting started with Eclipse plug-ins: understanding extension points]. Reading this tutorial implies that you have basic knowledge about eclipse extension mechanism, and programming in Java.
  
−
== Explanations and Outline ==
+
== Extension Points provided by Eclipse ==
−
This tutorial is '''problem solving oriented'''. Hence, all contributions to the platform via plugin additions will address needs implied by the issues we aim to solve, or functionnalities we want to add.<br>
+
Eclipse defines extension points that allow plug-ins to contribute behaviours to existing views and editors or to provide implementations for new views and editors (See [http://help.eclipse.org/help33/index.jsp?topic=/org.eclipse.platform.doc.isv/reference/extension-points/org_eclipse_ui_actionSets.html Basic workbench extension points using actions]):
−
We will, in a first time, focus on one concrete example of step-by-step plugin development . This first example will add Probabilistic Termination and Qualitative Reasoning in Rodin. For more informations about the Probabilistic Termination and Qualitative Reasoning, please refer to the paper of ''Emre Yilmaz and Thai Son Hoang : Development of Rabin's Choice Coordination Algorithm in Event-B in Proceedings of the 10th International Workshop on Automated Verification of Critical Systems (AVoCS 2010)''<br>
+
* <tt>org.eclipse.ui.views</tt>
−
'''//FIXME''' Include link to the paper here
+
* <tt>org.eclipse.ui.viewActions</tt>
−
<br>
+
* <tt>org.eclipse.ui.editors</tt>
−
In a second time, we will use small examples, to review all extensions abilities that didn't appear in the first part of this tutorial.
+
* <tt>org.eclipse.ui.editorActions</tt>
 +
* <tt>org.eclipse.ui.popupMenus</tt>
 +
* <tt>org.eclipse.ui.actionSets</tt>
  
−
'''First part''' : extending Rodin with a plugin for Qualitative Probabilistic Reasoning
+
Some other extension points are useful to contribute to the GUI:
−
# [[Creating_a_new_plugin_using_eclipse_(How_to_extend_Rodin_Tutorial)|Creating our plugin]]
+
* <tt>org.eclipse.ui.preferencePages</tt>, which allows to define preference pages (See [http://www.eclipse.org/articles/Article-Preferences/preferences.htm Preferences in the Eclipse Workbench UI]).
−
# [[Extend_Rodin_database_(How_to_extend_Rodin_Tutorial)|Adding elements to the database (Extend the database)]]
+
* <tt>org.eclipse.ui.navigator.navigatorContent</tt> and <tt>org.eclipse.ui.navigator.viewer</tt>, which allows to get a basic navigator to appear with custom content. This extension point will be used in details in the section "[[Extending the Rodin Event-B Explorer (How to extend Rodin Tutorial) | Extending the Rodin Event-B Explorer]]" of this tutorial.
−
# //extend the ui
 
−
# //extend the static checker
 
−
# //extend the proof obligation generator
 
−
'''Second part''' : extending Rodin (other extension abilities not mentioned above)
 
−
#
 
−
#
 
−
#
 
−
#
 
  
 +
Finally, a plug-in may contribute help files by using the <tt>org.eclipse.help.toc</tt> extension point. These files may be written by hand or automatically generated from Wiki pages, as explained [[Providing_help_for_your_plug-in_(How_to_extend_Rodin_Tutorial) | here]].
  
−
==Requirements==
+
== Explanations and Outline ==
 +
This tutorial is '''problem solving oriented'''. Hence, all contributions to the platform via plug-in additions will address needs implied by the issues we aim to solve, or functionalities we want to add.
  
−
Reading this tutorial implies that you have basic knowledge about eclipse extension mechanism, and programming in Java.<br>
+
It is mainly based on one concrete example of step-by-step plug-in development. This example will add Probabilistic Termination and Qualitative Reasoning in Rodin. For more informations about the Probabilistic Termination and Qualitative Reasoning, please refer to the paper of ''Emre Yilmaz and Thai Son Hoang : Development of Rabin's Choice Coordination Algorithm in Event-B in Proceedings of the 10th International Workshop on Automated Verification of Critical Systems (AVoCS 2010)''<br>
−
For informations about extension points, please refer to this article : [[http://www.eclipse.org/resources/resource.php?id=383]].
+
See the corresponding paper here : http://e-collection.ethbib.ethz.ch/eserv/eth:1677/eth-1677-01.pdf
  
−
Moreover, a development environment is required to develop the plugin code described in this tutorial.<br>
+
Other small examples are used in parallel to review all extensions abilities.
−
'''//FIXME''' Document more about the needed environment to develop plugins for Rodin
 
  
−
{{Navigation|Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]] | Next= [[Creating_a_new_plugin_using_eclipse_(How_to_extend_Rodin_Tutorial)|Creating our plugin]]}}
+
{{Navigation|Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]] | Next= [[Creating_a_new_plugin_using_eclipse_(How_to_extend_Rodin_Tutorial)|Creating our plug-in]]}}
  
 
[[Category:Developer documentation|*Index]]
 
[[Category:Developer documentation|*Index]]
 
[[Category:Rodin Platform|*Index]]
 
[[Category:Rodin Platform|*Index]]
 
[[Category:Tutorial|*Index]]
 
[[Category:Tutorial|*Index]]

Latest revision as of 17:03, 16 October 2010

>next: Creating our plug-in ^up: How to extend Rodin Tutorial (Index)

In this tutorial, we will focus on the extension of the Rodin platform by adding plug-ins. This mechanism inherits from Eclipse extension mechanism (see paragraph about Extension points and Extensions below). As we will discuss here about the provided Rodin extensibility possibilities, reading this tutorial implies that you have basic knowledge in Event-B, and are familiar with Java programming language.

Extension Points and Extensions

Rodin uses Eclipse extensibility mechanism. This mechanism is based on the notions of "extension points" and "extensions".
A plug-in that wants to offer functionalities (e.g. extension services) defines an extension point. An extension point is a sort of contract given to other plug-ins, to use (e.g. extend) those provided extension services. This contract is expressed in XML. A concrete example of extension service is offered by the plug-in org.rodinp.core to register new elements in Rodin database. Moreover, a plug-in defining an extension point will manage all contributions (that we call extensions), through its lifecycle. In the case of Rodin Database, all extensions of the database (added elements, added attributes, etc.) are managed by the plug-in org.rodinp.core.

To extend Rodin, we are in the situation where plug-ins (callers) want to use the extension services offered by one plug-in (e.g. the callee that defines an extension point).

Extend Rodin Tuto Extension.png

Thus, we will define a caller (a new plug-in) that accepts one or more contracts with the Rodin platform. To accept such contract, a caller has to specify its dependency to the callee, and define one (resp. many) extensions, which conforms to an (resp. corresponding) imported extension point. The terms of the contract are often given through required interfaces, which defines a protocol to use the provided extension services. In other words, the results of the computation performed in caller's code need to conform to an interface defined by the callee (the extension service provider). Sometimes, the callee defines additional interfaces to give the callers a view on the managed contributions.
In this tutorial, we will define new callers and use the contracts offered by the Rodin platform.

For more information about extension points, please refer to this article: Getting started with Eclipse plug-ins: understanding extension points. Reading this tutorial implies that you have basic knowledge about eclipse extension mechanism, and programming in Java.

Extension Points provided by Eclipse

Eclipse defines extension points that allow plug-ins to contribute behaviours to existing views and editors or to provide implementations for new views and editors (See Basic workbench extension points using actions):

  • org.eclipse.ui.views
  • org.eclipse.ui.viewActions
  • org.eclipse.ui.editors
  • org.eclipse.ui.editorActions
  • org.eclipse.ui.popupMenus
  • org.eclipse.ui.actionSets

Some other extension points are useful to contribute to the GUI:

  • org.eclipse.ui.preferencePages, which allows to define preference pages (See Preferences in the Eclipse Workbench UI).
  • org.eclipse.ui.navigator.navigatorContent and org.eclipse.ui.navigator.viewer, which allows to get a basic navigator to appear with custom content. This extension point will be used in details in the section " Extending the Rodin Event-B Explorer" of this tutorial.

Finally, a plug-in may contribute help files by using the org.eclipse.help.toc extension point. These files may be written by hand or automatically generated from Wiki pages, as explained here.

Explanations and Outline

This tutorial is problem solving oriented. Hence, all contributions to the platform via plug-in additions will address needs implied by the issues we aim to solve, or functionalities we want to add.

It is mainly based on one concrete example of step-by-step plug-in development. This example will add Probabilistic Termination and Qualitative Reasoning in Rodin. For more informations about the Probabilistic Termination and Qualitative Reasoning, please refer to the paper of Emre Yilmaz and Thai Son Hoang : Development of Rabin's Choice Coordination Algorithm in Event-B in Proceedings of the 10th International Workshop on Automated Verification of Critical Systems (AVoCS 2010)
See the corresponding paper here : http://e-collection.ethbib.ethz.ch/eserv/eth:1677/eth-1677-01.pdf

Other small examples are used in parallel to review all extensions abilities.


>next: Creating our plug-in ^up: How to extend Rodin Tutorial (Index)
Retrieved from ‘https://wiki.event-b.org/index.php?title=Introduction_(How_to_extend_Rodin_Tutorial)&oldid=5813’