Difference between pages "Extending the Static Checker (How to extend Rodin Tutorial)" and "Rodin Developer Support"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
m
 
imported>Colin
 
Line 1: Line 1:
−
{{Navigation|Previous= [[Providing_help_for_your_plug-in_(How_to_extend_Rodin_Tutorial) | Providing help]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]] | Next= [[Extending_the_Proof_Obligation_Generator(How_to_extend_Rodin_Tutorial) | Generating the proof obligations]]}}
+
The Developer Support provides resources for developing plug-ins for the Rodin Platform.
  
−
=== In this part ===
 
  
−
We will see how to add rules to statically check the machines after our extension. The Static Checker (SC) is one dedicated part of the Proof Obligation (PO) generation process. Indeed, the POs are generated from the statically checked version of the model taken into account. Hence, we have to ensure before creating POs, that the model is correctly expressed (i.e. POs are generated for a model which "''could'' have some sense"). This means that we have to verify some additional properties on the newly added elements. <br>
+
== Rodin Developer FAQ ==
−
The question addressed here is: " '''Under which conditions (about the model well-formedness) the PO generation means something?''' ".<br>
 
−
Additional information is available [http://wiki.event-b.org/index.php/Extending_the_Static_Checker here].
 
  
−
=== Principles ===
+
see [[Developer FAQ]].
  
−
1. To extend the static checker in order to verify some conditions, one has to '''define a static checker module''' using the extension point <tt>org.eventb.core.scModuleTypes</tt>.<br>
+
== Architecture of the Rodin Platform ==
−
There are two types of modules: <tt>processorType</tt> and <tt>filterType</tt>. We will detail the way to define such modules later.<br>
 
−
2. Then, one has to '''set up a configuration''' involving these modules and giving them a hierarchy. In fact, verifying the correctness conditions about added elements can be separated in several processor and filter modules; the configuration is then used to organise them.<br>
 
−
3. Finally, it is needed to add a reference (e.g. include) to this created configuration to the default one (the SC and POG configuration used by rodin), so our static checkings can be performed.<br>
 
  
−
=== Step 1: Extending the database to introduce the static checked version of the element ''Bound'' (a.k.a. SCBound) ===
+
=== Rodin Platform Core ===
  
−
The aim of static checking is to produce a static checked version of the model upon consideration. Hence, every element ("unchecked") shall have its statically checked counterpart. We will then add the counterpart of the element <tt>Bound</tt>, following the same steps as when we added our element <tt>Bound</tt> in the database (See step 4 [[Extend_Rodin_database_(How_to_extend_Rodin_Tutorial)|here]]).
+
* [[Database]]
  
−
To do so, create a new extension <tt>internalElementType</tt> from <tt>org.rodinp.core.internalElementTypes</tt> with:<br>
+
* [[Builder]]
−
- id: <tt>scBound</tt>,<br>
 
−
- a name such as "Event-B Static Checked Bound Element",<br>
 
−
- a class for this element that extends <tt>SCExpressionElement</tt> and implements a freshly created interface <tt>ISCBound</tt> defined as follows:
 
  
−
public interface ISCBound extends ISCExpressionElement, ITraceableElement {
+
* [[Rodin Index Design]]
−
 
−
IInternalElementType<ISCBound> ELEMENT_TYPE =
 
−
RodinCore.getInternalElementType(QualProbPlugin.PLUGIN_ID + ".scBound");
 
−
}
 
  
−
=== Step 2: Adding modules===
+
* [[Indexing System]]
  
−
==== Generalities ====
+
* [[Undo Redo]]
−
In our case of probabilistic reasoning, the following '''well-formedness conditions should be held''' for a model ''containing probabilistic events'':
 
−
# The variant V (declared as usual) shall be either of type integer or some set.
 
−
# There is exactly one bound for a model where the probabilistic convergence is proved. The Bound element B shall be of the same type as the declared variant.
 
−
# Every probabilistic event shall be refined by a probabilistic event.
 
−
# The result of merging a probabilistic event and a convergent event is a probabilistic event.
 
  
−
We can face two types of situations during the static checking:
+
* [[File Root Separation]]
−
# We encounter a problem which doesn't affect the PO generation: it leads to a '''warning''' (fixed by a default assumption or not).
 
−
# We encounter a problem which affects the PO generation: it leads to an '''error''' (The element, added with our extension and under consideration, is not added in the statically checked model).
 
  
−
We have previously said that there is two types of modules. We first define a <tt>processorModule</tt>. Processor modules literally process the elements, storing them once validated in the statically checked file.
+
=== Event-B User Interface ===
−
In parallel, a <tt>filterModule</tt>s performs only some verifications (i.e. a <tt>filtermodule</tt> cannot do anything with the statically checked file). Furthermore, the filters are called (in group) from processors, and as soon as one filter rejects one element (i.e. "does not accept the element"), the other filters will not be evaluated for this element.
 
  
−
In a <tt>processorModule</tt>, if the static check fails for the considered element, the module '''must not add such element''' to the statically checked file that it holds, and which is used for PO generation. Processors are also responsible of running sub-processors, and filters, as well as adding states to the repository if required.<br>
+
The Event-B User Interface of the Roding Platform has two major components that are concerned with either [[Modelling User Interface|modelling]] in Event-B or [[Proving User Interface|proving]] properties of models.
−
The developer is responsible of its module configuration lifecycle. He has to be aware, at any time, of his module's hierarchy, and has to call sub-modules explicitly when meaningful. Furthermore, a system of state sharing (via a state repository) is available so that a processor can provide informations about its checking results to its sub-modules. See <tt>org.eventb.core.sc.state.ISCStateRepository</tt> and <tt>org.eventb.core.sc.state.ISCState</tt>. Remember that it is only allowed to share informations within a module/sub-module hierarchy and that a policy should be established so that concurrent access to these states is taken into account, and that informations stored in the state repository are still coherent through sub-processors and filters computations.<br>
 
  
−
Three methods can be used (e.g. overridden) in a <tt>processorModule</tt>:
+
* [[Modelling User Interface]]
−
* <tt>void initModule(IRodinElement element, ISCStateRepository repository, IProgressMonitor monitor) throws CoreException</tt>, which by default does nothing, but should be used in order to initialise the state (e.g. information) sharing.
 
−
* <tt>void process(IRodinElement element, IInternalElement target, ISCStateRepository repository, IProgressMonitor monitor) throws CoreException</tt>, which MUST be implemented to perform static checking.
 
−
* <tt>void endModule(IRodinElement element, ISCStateRepository repository, IProgressMonitor monitor) throws CoreException</tt>, which by default does nothing, but should be used if <tt>initModule()</tt> was used, to release the states locally created.<br>
 
  
−
==== Adding a processor module ====
+
* [[Proving User Interface]]
−
The processor that we will create will perform checks, and eventually add the statically checked version of the Bound element to the statically checked machine. As we don't really need to share information to our sub-modules, only the <tt>process()</tt> method will be overridden.
 
  
−
For the extension point <tt>org.eventb.core.scModuleTypes</tt> create an extension <tt>processorType</tt>.<br>
+
Apart from these are more minor components.
−
1. Enter a unique ID (like here <tt>machineBoundModule</tt>).<br>
 
−
2. Enter a human readable name such as "Machine SC Bound Module" as we will start to check bound elements.<br>
 
−
3. Enter the parent ID of the module we want to extend. Here as we want to make checks on bounds, variants and events, we will take <tt>org.eventb.core.machineModule</tt> as parent.<br>
 
−
4. Create the module class that <tt>extends SCProcessorModule</tt> (we called it "MachineBoundModule" and we used the "new class wizard").
 
  
−
The module class we created has to be implemented.<br>
+
* [[Proof Purger Design|Proof Purger]] allows to delete unused proofs.  
−
Two methods inherited from the interface <tt>ISCProcessorModule</tt> have to be defined (e.g. <tt>@Override</tt>):
 
  
−
''A . <tt>public IModuleType<?> getModuleType()</tt>''
+
* [[Proof Skeleton Design]] is a view that displays skeletons of existing proofs
  
−
This method shall return the type of our module, built from its extension's ID. In order to do that, we use the static method in <tt>org.eventb.core.sc.SCCore.getModuleType()</tt> with the complete identifier of our module extension: <tt>QualProbPlugin.PLUGIN_ID + ".machineBoundModule"</tt>.<br>
+
* [[Auto-Completion Design]] proposes a list of names to the user editing a model
−
Thus, let's use the constant below in our code:
 
  
−
public static final IModuleType<MachineBoundModule> MODULE_TYPE = SCCore.getModuleType(QualProbPlugin.PLUGIN_ID + ".machineBoundModule");
+
=== Event-B Component Library ===
  
−
So we can write:
+
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 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|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|proof obligation generator]] uses those parts of constructs that are well-formed and generates proof obligations from them. Finally, the [[Proof Manager|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|proving user interface]]).
  
−
@Override
+
* [[Abstract Syntax Tree]]
−
public IModuleType<?> getModuleType() {
 
−
return MODULE_TYPE;
 
−
}
 
  
−
''B . <tt>public void process(IRodinElement element, IInternalElement target, ISCStateRepository repository, IProgressMonitor monitor) throws CoreException</tt>''
+
* [[Static Checker]]
  
−
This method is the place where checks are performed. Thus, it is where we will code all the conditions to check and finally produce a statically checked Bound element if all the conditions are respected.
+
* [[Proof Obligation Generator]]
−
The implementation is "huge" and pure Java, and it is not relevant in this tutorial to detail the full code. We will rather explain which are the main operations performed by the <tt>process</tt> method and give some hints about how to use the Rodin API to retrieve the information required in our checks. Full implementation is let to the reader as an exercise.
 
  
−
Here are some explanations about the <tt>process()</tt> method arguments:
+
* [[Proof Manager]]
  
−
The <tt>element</tt> passed as argument here is the element propagated by the parent of this module. It may be useful in case of systematic element checking, to retrieve the elements to check in a parent processor module, and then manage each element one by one, calling sub-processor modules.<br>
+
* [[Proof Simplification]]
−
The <tt>IInternalElement</tt> target is the statically checked file where our elements, after successful well-formedness verification, will be stored. This file will be used as an input for the PO generation.<br>
 
−
The parameter <tt>ISCStateRepository</tt> repository is the global repository used by the module to get shared information. (//FIXME complete the static checker page, to add infos about states and link it here).<br>
 
−
Finally, <tt>IProgressMonitor</tt> monitor is the progress monitor used while performing the static checks. Sub-tasks can be created for it.
 
  
−
In our case, we have to refine the well-formedness conditions into a verification algorithm. We choose to retrieve the bound and variant values from the machine root directly using the following code in the <tt>process</tt> method:
+
== Extending Rodin ==
  
−
final IRodinFile machineFile = (IRodinFile) element;
+
* [[Developer Documentation]]
−
final IMachineRoot machineRoot = (IMachineRoot) machineFile.getRoot();
 
−
final IBound[] bounds = machineRoot.getChildrenOfType(IBound.ELEMENT_TYPE);
 
−
final IVariant[] variants = machineRoot.getVariants();
 
  
−
Warnings and errors will be created using the method <tt>createProblemMarker</tt> (see <tt>org.eventb.core.sc.SCModule</tt>).
+
* [[Plug-in Tutorial]]
  
−
==== Exercise 1 - Implement the proposed algorithm (among others) ====
+
* [[Extending the Rodin Database]]
  
−
If the machine does not contain a probabilistic event, but there is a bound,
+
* [[Extending the project explorer]]
−
then we add a warning informing that the bound is ignored.
 
−
 
−
If the machine contains at least a probabilistic event (i.e. "the model is probabilistic"), but there are more than one bound,
 
−
then we create an error telling that there are too many bounds, nothing is created an we return immediately.
 
−
 
−
// We are now sure that there a single bound
 
−
If the model is probabilistic
 
−
   
 
−
    If the variant is not a set or a constant, we create an error and return.
 
−
      The following code may serve as a basis:
 
−
 
−
      private boolean assertIsASetOrConstant(IExpressionElement element)
 
−
throws RodinDBException {
 
−
              final String formula = element.getExpressionString();
 
−
              final IParseResult result = factory.parseExpression(formula, LanguageVersion.V2, element);
 
−
              final Expression boundExpression = result.getParsedExpression();
 
−
              return isASetOrConstant(boundExpression.getType());
 
−
 
−
          with
 
−
 
−
              private boolean isASetOrConstant(Type type) {
 
−
if (type.equals(factory.makeIntegerType())) {
 
−
return true;
 
−
}
 
−
final Type baseType = type.getBaseType();
 
−
if (baseType != null) {
 
−
return type.equals(factory.makePowerSetType(baseType));
 
−
}
 
−
return false;
 
−
}
 
−
   
 
−
    If there is no bound, we create an error, and return.
 
−
 
−
    If the bound is not a set or a constant, we create an error, and return.
 
−
 
−
    If the bound is not of the same type as the variant, we create an error and return.
 
−
      One may check it as follows:
 
−
                        if (!getType(bound).equals(getType(variant))) {
 
−
createProblemMarker(bound,
 
−
EventBAttributes.EXPRESSION_ATTRIBUTE,
 
−
ProbabilisticGraphProblem.VariantBoundTypeError);
 
−
return;
 
−
}
 
−
    [...]
 
  
−
// After all checks, we add the bound to the statically checked file.
+
* [[Extending the Structure Editor]]
−
final ISCBound scBound = target.getInternalElement(ISCBound.ELEMENT_TYPE, BOUND_NAME_PREFIX);
 
−
scBound.create(null, monitor);
 
−
scBound.setExpression(getExpression(bound), null);
 
  
−
In the processor module, one may use the filters to drop a part of the processing with the invocation <tt>filterModules(element, repository, monitor)</tt> which will return a boolean telling if the element has successfully passed all the filtering criteria or not.
+
* [[Extending the Pretty Print Page]]
−
One may also process an element using the child processor modules with the following invocation:<br>
 
−
<tt>protected final void processModules(IRodinElement element, IInternalElement target, ISCStateRepository repository, IProgressMonitor monitor) throws CoreException</tt>
 
  
−
==== Exercise 2 ====
+
* [[Extending the Proof Manager]]
−
We use here a filter <tt>machineBoundFreeIdentsModule</tt> to check that the expression of the ''Bound'' element parses, and that no additional free identifier was introduced.
 
−
Implement such a filter using the fact that the repository holds a type environment which contains all the usable free identifiers. To use this, we have to add a ''prereq'' clause to our filter pointing the ID <tt>org.eventb.core.machineVariantModule</tt> of the variant module.
 
−
Here is an extract of the filter's <tt>accept()</tt> method:
 
  
−
final ITypeEnvironment typeEnv = repository.getTypeEnvironment();
+
* [[Extending the Index Manager]]
−
final Expression parsedExpression = parseResult.getParsedExpression();
 
−
 
−
final FreeIdentifier[] freeIdentifiers = parsedExpression
 
−
.getFreeIdentifiers();
 
−
 
−
boolean ok = true;
 
−
for (FreeIdentifier ident : freeIdentifiers) {
 
−
if (!typeEnv.contains(ident.getName()))
 
−
createProblemMarker(bound,
 
−
EventBAttributes.EXPRESSION_ATTRIBUTE,
 
−
ProbabilisticGraphProblem.BoundFreeIdentifierError,
 
−
ident);
 
−
ok = false;
 
−
}
 
−
return ok;
 
  
−
=== Step 3: Setting up the configuration ===
+
* [[Extending the Static Checker]]
  
−
In order to register our checks, and because these verifications may be separated in several modules, we need to encapsulate them into a configuration.<br>
+
* [[Index Query]]
−
The extension point <tt>org.eventb.core.configurations</tt> allows to do that.<br>
 
−
To organise our modules:<br>
 
−
1. Create an extension <tt>configuration</tt> from the above mentioned extension point.
 
−
:Give it an ID (for example "qpConfig").
 
−
:Give it a human readable name (for example, "Qualitative Probabilistic Reasoning Plug-in Configuration").
 
  
−
2. Add the modules (full id) previously defined to the configuration. In our example, we implemented two modules:<br>
+
== Useful Hints ==
−
- <tt>fr.systerel.rodinextension.sample.machineBoundModule</tt><br>
 
−
- <tt>fr.systerel.rodinextension.sample.machineBoundFreeIdentsModule</tt><br>
 
  
−
That's all for configuration creation. Now, we need to add references to machine file configuration elements (e.g. kind of "include") so it can run when our plug-in is installed.
+
=== Version Control ===
  
−
=== Step 4: Adding the configuration ===
+
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  https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp].
  
−
The best way to add our configuration is to register a utility class that will add our configuration to the machine files when our plug-in is active, and if their configuration doesn't contain ours.
+
=== Building against a version of Rodin ===
−
To do so, create the following class that implements <tt>org.rodinp.core.IElementChangedListener</tt>:
 
  
−
/**
+
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 [http://wiki.event-b.org/index.php/FAQ#Installing_the_sources_from_Subversion_in_Eclipse Installing the sources from Subversion in Eclipse] for further instructions.
−
  * Class that updates the configuration of files, to add the static checker
 
−
  * modules for our qualitative probabilistic reasoning plug-in.
 
−
  */
 
−
public class ConfSettor implements IElementChangedListener {
 
−
 
−
private static final String QUAL_PROB_CONFIG = QualProbPlugin.PLUGIN_ID
 
−
+ ".qpConfig";
 
−
 
−
public void elementChanged(ElementChangedEvent event) {
 
−
 
−
final IRodinElementDelta d = event.getDelta();
 
−
try {
 
−
processDelta(d);
 
−
} catch (final RodinDBException e) {
 
−
// TODO add exception log
 
−
}
 
−
}
 
−
 
−
private void processDelta(final IRodinElementDelta d)
 
−
throws RodinDBException {
 
−
final IRodinElement e = d.getElement();
 
−
 
−
final IElementType<? extends IRodinElement> elementType = e
 
−
.getElementType();
 
−
if (elementType.equals(IRodinDB.ELEMENT_TYPE)
 
−
|| elementType.equals(IRodinProject.ELEMENT_TYPE)) {
 
−
for (final IRodinElementDelta de : d.getAffectedChildren()) {
 
−
processDelta(de);
 
−
}
 
−
} else if (elementType.equals(IRodinFile.ELEMENT_TYPE)) {
 
−
final IInternalElement root = ((IRodinFile) e).getRoot();
 
−
 
−
if (root.getElementType().equals(IMachineRoot.ELEMENT_TYPE)) {
 
−
final IMachineRoot mch = (IMachineRoot) root;
 
−
final String conf = mch.getConfiguration();
 
−
if (!conf.contains(QUAL_PROB_CONFIG)) {
 
−
mch.setConfiguration(conf + ";" + QUAL_PROB_CONFIG, null);
 
−
}
 
−
}
 
−
}
 
−
}
 
−
}
 
  
−
Where the string constant ''QUAL_PROB_CONFIG'' refers to our configuration in the machine files. We check that each manipulated machine file contains our configuration.
+
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).
−
Now we need to launch this class at plug-in start-up.
 
  
−
To do so:<br>
+
=== Testing ===
−
1. Open the activator of our plug-in.<br>
 
−
2. Add a method <tt>setProbConfig()</tt> to the <tt>start(BundleContext context)</tt> method of the activator.<br>
 
−
3. Implement this method:<br>
 
−
        /**
 
−
* Registers a file configuration setter for our plugin.
 
−
*/
 
−
public static void setProbConfig() {
 
−
RodinCore.addElementChangedListener(new ConfSettor());
 
−
}
 
  
−
{{Navigation|Previous= [[Providing_help_for_your_plug-in_(How_to_extend_Rodin_Tutorial) | Providing help]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]] | Next= [[Extending_the_Proof_Obligation_Generator(How_to_extend_Rodin_Tutorial) | Generating the proof obligations]]}}
+
=== Debugging ===
  
−
[[Category:Developer documentation|*Index]]
+
=== Publishing ===
−
[[Category:Rodin Platform|*Index]]
+
 
−
[[Category:Tutorial|*Index]]
+
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).
 +
 
 +
Create a new release folder in the FRS (On Sourceforge Rodin project website - Admin-file releases) noting the naming conventions (e.g. Plugin_<mypluginName>). Now you can upload your jar files using the controls on the releases webpage). Note that you should include a zip of the complete source projects to comply with Sourceforge rules.
 +
You should not repeat files that have not changed. 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.
 +
# From the sourceforge SVN repository, check out the project org.rodinp.updateSite.
 +
# Edit the  file site.xml to add your feature and plug-in archive paths
 +
# Test the changes by performing the install into a Rodin installation, via the local update site in your workspace.
 +
# Commit the changes back into SVN
 +
# Upload the new version of the update site onto the Rodin webspace. (Currently this is done by Colin Snook on request - see Rodin developers page for contact details).
 +
 
 +
[[Details for Maintaining Main Rodin Update Site]]
 +
 
 +
 
 +
[[Category:Developer documentation]]
 +
[[Category:Rodin Platform]]

Revision as of 10:07, 3 February 2011

The Developer Support provides resources for developing plug-ins for the Rodin Platform.


Rodin Developer FAQ

see Developer FAQ.

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.

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

Create a new release folder in the FRS (On Sourceforge Rodin project website - Admin-file releases) noting the naming conventions (e.g. Plugin_<mypluginName>). Now you can upload your jar files using the controls on the releases webpage). Note that you should include a zip of the complete source projects to comply with Sourceforge rules. You should not repeat files that have not changed. 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.

  1. From the sourceforge SVN repository, check out the project org.rodinp.updateSite.
  2. Edit the file site.xml to add your feature and plug-in archive paths
  3. Test the changes by performing the install into a Rodin installation, via the local update site in your workspace.
  4. Commit the changes back into SVN
  5. Upload the new version of the update site onto the Rodin webspace. (Currently this is done by Colin Snook on request - see Rodin developers page for contact details).

Details for Maintaining Main Rodin Update Site

Retrieved from ‘https://wiki.event-b.org/index.php?title=Extending_the_Static_Checker_(How_to_extend_Rodin_Tutorial)&oldid=7068’