Rodin Developer Support
The Developer Support provides resources for developing plug-ins for the Rodin Platform.
Rodin Platform Overview
Architecture of the Rodin Platform
Rodin Platform Core
Event-B User Interface
The Event-B User Interface of the Roding Platform has two major components that are concerned with either modelling in Event-B or proving properties of models.
Apart from these are more minor components.
- Proof Purger allows to delete unused proofs.
- Proof Skeleton Design is a view that displays skeletons of existing proofs
- Auto-Completion Design proposes a list of names to the user editing a model
Event-B Component Library
Event-B models and all proof-related information are stored in the Rodin database. The syntax of the mathematical notation, that is, expressions, predicates, and assignments, are maintained in an abstract syntax tree. Abstract syntax trees are manipulated by means of a class library that can be used independently of Eclipse. They are saved in the database in human-readable form as Unicode character strings. Event-B constructs, such as contexts and machines, are not represented as abstract syntax trees. They are stored and retrieved directly from the database (by contrast, mathematical formulas need additional parsing). Well-formedness of Event-B constructs is verified by a static checker. The static checker has two main purposes: (1) it generates error messages for ill-formed constructs, and (2) it filters well-formed parts of components to be subjected to proof obligation generation. The proof obligation generator uses those parts of constructs that are well-formed and generates proof obligations from them. Finally, the proof manager attempts to prove proof obligations and maintains existing proofs associated with proof obligations. The proof manager works automatically and interactively. When new proof obligations have been generated it attempts to discharge them automatically. If it does not succeed, it permits interactive proof (by means of the proving user interface).
Extending Rodin
Useful Hints
Version Control
All sources of the core Rodin platform (and of some plug-ins) are managed under version control in SourceForge. The repository currently used is Subversion and can be accessed using URL https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp.
Building against a version of Rodin
To develop extensions to the Rodin platform your code build needs access to a consistent (version-wise) set of Rodin platform plug-ins. (Don't just check out the latest versions from 'Head' because it may be under development and in an inconsistent state). An easy way to set up your workspace is to import the Rodin platform source code from SVN into your workspace using the 'Releng' plug-in. See Installing the sources from Subversion in Eclipse for further instructions.
Alternatively, you can set your plugin development target platform to any Rodin installation you have installed (Eclipse-Preferences-Plug-in Development-Target Platform). This is useful as a final test that everything will work once installed into Rodin but because it uses a 'built' platform, you don't get access to the Rodin source code (e.g. for de-bugging).
Testing
Debugging
Publishing
A Plug-in developed for the Rodin Platform will normally consist of a collection of eclipse 'plugin' projects and a single eclipse 'feature' project. The feature project contains branding information such as logo's icons and licensing details. It is also used to identify your Plug-in so that users can install it. To build your Plug-in use an eclipse 'site' project. This will build the jar files for your plugin projects and a jar for your feature. See eclipse documentation for more details.
Now you need to make your Plug-in available for users to install via the Main Rodin Update site (which comes built-in to the Rodin platform).
First upload your jar files onto the Sourceforge uploads area and then create a new release in the FRS (Admin-file releases). Note that you should include a zip of the complete source projects to comply with Sourceforge rules. You must not repeat files that have not changed. Sourceforge does not allow you to upload multiple copies of the same jar file. The Feature jar will take care of unchanged plugin jars and use the existing links. Only new jars should be included in a particular release. See here for details:- http://alexandria.wiki.sourceforge.net/File+Release+System+-+Offering+Files+for+Download
Finally, the update site must be updated to redirect the update requests to the files on the FRS. (Currently this is done by Colin Snook on request - see Rodin developers page for contact details).
Details for Maintaining Main Rodin Update Site
Rodin Developer FAQ
see FAQ.
