Rodin Platform 1.1 Release Notes

What's New in Rodin 1.1?

TODO: List here the new features and improvements.

• Rodin Keyboard

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.

• Versioned Reasoners

The reasoners are now tagged with a version, which will evolve along with their behavior.

• New Rewriting rules and on prover rules are included:

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

• Multi-tactics

• Generated Model Elements

The generated event-B files are tagged. These files cannot be modified.

• Symbol Table

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.

Requirements

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

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.

Known Issues

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