Introduction (How to extend Rodin Tutorial)

>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).

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 presented in details in //FIXME ajouter ref ici.

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.
We will, in a first time, focus on one concrete example of step-by-step plug-in 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)
//FIXME Include link to the paper here
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.

First part : extending Rodin with a plug-in for Qualitative Probabilistic Reasoning

1. Creating our plug-in
2. Adding elements to the database (Extending the database)
3. Adding elements in the Rodin structured editor (Extending the structured editor)
4. Adding elements to the Event-B explorer (Extending the navigator)
5. //extend the ui
6. //extend the static checker
7. //extend the proof obligation generator
8. Documenting your plug-in (Providing Eclipse Help contents)

Second part : extending Rodin (other extension abilities not mentioned above)

>next: Creating our plug-in

^up: How to extend Rodin Tutorial (Index)