Difference between revisions of "Rodin Platform 1.1 Release Notes"

From Event-B
Jump to navigationJump to search
imported>Pascal
imported>Pascal
Line 3: Line 3:
 
== What's New in Rodin 1.1? ==
 
== What's New in Rodin 1.1? ==
 
{{TODO | List here the new features and improvements.}}
 
{{TODO | List here the new features and improvements.}}
 +
 +
* [[Rodin_Keyboard | Rodin Keyboard]]
 +
A new extensible plug-in for the Event-B Keyboard is included. The former one, namely <tt>org.eventb.eventBKeyboard</tt>, translated hard-coded key combos into hard-coded unicode mathematical symbols. There is now one main plug-in, <tt>org.rodinp.keyboard</tt>, that defines a mere extension point <tt>org.rodinp.keyboard.symbols</tt> to define associations between an ASCII sequence and a symbol. It avoids hard-coding anything.
 +
There are currently two extensions of this point:
 +
# One in the plug-in <tt>org.eventb.keyboard</tt>, for standard Event-B notation translation.
 +
# One in the plug-in <tt>ch.ethz.eventb.keyboard.latex</tt>, for LaTeX notation translation.
 +
 +
* [[Versioned Reasoners | Versioned Reasoners]]
 +
The reasoners are now tagged with a version, which will evolve along with their behavior.
 +
 +
* New [[All_Rewrite_Rules | Rewriting rules]] and on prover rules are included:
 +
# Arithmetic rules (''e.g.'' the form <math>A+B+C-B \defi A+C</math> and a few others)
 +
# DEF_IN_UPTO: <math>x \in a \upto b \defi a \leq x \land x \leq b</math>
 +
# One point rule
 +
# Goals of the form <math>\exists n \qdot \forall x \qdot x \in S \limp x \leq n</math> when you have a hypothesis that states <math>finite(S)</math>
 +
# SIMP_SPECIAL_OVERL
 +
# SIMP_FUNIMAGE_LAMBDA
  
 
== Requirements ==
 
== Requirements ==

Revision as of 14:50, 26 August 2009

What's New in Rodin 1.1?

TODO: List here the new features and improvements.

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

Requirements

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

Optional plug-ins

TODO: Describe here the available plug-ins, and the supported versions for the 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).

Retrieved from ‘https://wiki.event-b.org/index.php?title=Rodin_Platform_1.1_Release_Notes&oldid=7309’