Rodin Platform 1.1 Release Notes

From Event-B
Jump to navigationJump to search

What's New in Rodin 1.1?

A new extensible plug-in for the Event-B Keyboard is included. The former one, namely org.eventb.eventBKeyboard, translated hard-coded key combos into hard-coded unicode mathematical symbols. There is now one main plug-in, org.rodinp.keyboard, that defines a mere extension point org.rodinp.keyboard.symbols to define associations between an ASCII sequence and a symbol. It avoids hard-coding anything.
There are currently two extensions of this point:
  1. One in the plug-in org.eventb.keyboard, for standard Event-B notation translation.
  2. One in the plug-in ch.ethz.eventb.keyboard.latex, for LaTeX notation translation.
The reasoners are now tagged with a version, which will evolve along with their behavior.
  1. Arithmetic rules (e.g. the form A+B+C-B \defi A+C and a few others)
  2. DEF_IN_UPTO: x \in a \upto b \defi a \leq x \land x \leq b
  3. One point rule
  4. Goals of the form \exists n \qdot \forall x \qdot x \in S \limp x \leq n when you have a hypothesis that states finite(S)
  5. SIMP_SPECIAL_OVERL
  6. SIMP_FUNIMAGE_LAMBDA
A new tactic provider extension API is proposed. It allows tactic providers to give several possible tactic applications, even at the same position in a predicate. This new mechanism is also intended to fit with rule-based provers needs.
  • Proof obligations
The POG does not not generate any longer THM POs for guards when the conditions have already been proved for the abstract event.
The generated event-B files are tagged. These files cannot be modified.
A symbol table view is provided. It contains the mathematical symbols. When clicking on a symbol, it is included at the current position in the text of the Rodin Context/Machine editor.
  • PO Icons
Changed color of 'pending' icon for undischarged POs from red to orange/brown.
Used 'pending_pale' icons for unattempted POs in explorer.
  • Modulo
Reinforced the WD condition for the modulo operator. We now have exactly the same condition as in classical B: x \bmod b~ is well-defined iff 0 \leq x \land 0 < y.

Requirements

TODO: Inform here of some specific system requirements (version of Java, etc).

  • It is recommended to run the Rodin platform with a Java 1.5 Runtime Environment.
  • Only a 32-bit version of the Rodin platform is provided. Some optional libraries dedicated to 32-bit support may be required in order to run it on a 64-bit OS. Moreover, you will have to install a 32-bit Java Virtual Machine (JVM), and then to set the -vm option to make sure that Rodin is run with the correct JVM.
eg. /usr/local/rodin/rodin -vm /usr/lib/jvm/ia32-java-1.5.0-sun/bin/java (You have to adjust paths to your system.)

External plug-ins

TODO: Describe here the available plug-ins, and the supported versions for this release.

Downloading

TODO: Add here a link to download the platform.

Fixed Bugs

TODO: Add here a list of the fixed bugs.

Known Issues

  • XULRunner 1.9.1 may cause an SWT exception that prevents from opening an editor (as well as any browser-based ui component). To fix it, it is possible to specify XULRunner path to point to 1.9.0: edit "rodin.ini" and add the following line:
-Dorg.eclipse.swt.browser.XULRunnerPath=/usr/lib/xulrunner-1.9.0.14

where "/usr/lib/xulrunner-1.9.0.14" must be replaced with your actual XULRunner 1.9.0 install directory.

TODO: Add here a link to the SourceForge Bugs page, after filtering bugs (Assignee Any, Status Open, Category Any, Group 1.1).