From Event-B
Revision as of 08:48, 6 September 2011 by imported>Nicolas (→‎General Tool Usage)
Jump to navigationJump to search


What is event-B?

Event-B is a formal method for system-level modelling and analysis. Key features of event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. More details are available in http://www.event-b.org/

What is the difference between event-B and the B method?

Event-B is derived from the B method. Both notations have the same inventor, and share many common concepts (set-theory, refinement, proof obligations, ...) However, they are used for quite different purpose. The B method is devoted to the development of correct by construction software, while the purpose of event-B is to model full systems (including hardware, software and environment of operation).

Both notations use a mathematical language which are quite close but do not match exactly (in particular, operator precedences are different).

What is Rodin?

The Rodin Platform is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof. The platform is open source, contributes to the Eclipse framework and is further extendable with plugins.

Where does the Rodin name come from?

The Rodin platform was initially developed within the European Commission funded Rodin project (IST-511599 ), where Rodin is an acronym for "Rigorous Open Development Environment for Complex Systems” . Rodin is also the name of a famous French sculptor, one of his most famous work being the Thinker.

General Tool Usage

Rodin does not launch on my 64 bit OS

You are probably running a 64 bit Windows or 64 bit Linux: for these OSes, Rodin is provided in a 32 bit version (Rodin for Mac is 64 bit). So you need to have a 32 bit JRE installed to run Rodin.

Then, you have to tell Rodin where to find it; edit the file "rodin.ini" in your Rodin install directory, then add a "-vm" option, as explained at http://wiki.eclipse.org/Eclipse.ini.

As Rodin is an Eclipse product, rodin.ini file is very much the same as eclipse.ini file.

Do I lose my proofs when I clean a project ?

No ! This is a common misunderstanding of what a project clean does. A project contains two kinds of files:

  • those you can edit: contexts, machines, proofs
  • those generated by a project build: proof obligations, proof statuses (roughly speaking, for each proof obligation, discharged or not discharged)

The cleaner just undoes what the builder does, i.e. it removes proof obligations and statuses, but it never modifies any proof.

A status may change from discharged to not discharged when the proof is no more compatible with the corresponding proof obligation (because hypotheses changed for instance), but the proof itself is still there ! You can try to replay it.

A confusion might arise from the possibility to launch automatic provers upon build. The cleaner does not undo these automatic proofs (why would it ?!!). Once a proof is made, the platform does not modify or delete it by itself. Even obsolete proofs are preserved !

How do I install external plug-ins without using Eclipse Update Manager?

Although it is preferred to install additional plug-ins into the Rodin platform using the Update Manager of Eclipse, this might not always be practical. In this case, a manner to install these plug-ins is to emulate either manually or using ad-hoc scripts the operations normally performed by the Update Manager.

This manual installation of plug-ins is described in Installing external plug-ins manually.

The builder takes too long

Generally, the builder spends most of its time attempting to prove POs. There are basically two ways to get it out of the way:

  • the first one is to disable the automated prover in the Preferences panel.
  • the second one is to mark some PO as reviewed when you don't want the auto-prover to attempt them anymore.

Note that if you disable the automated prover, you always can run it later on some files by using the contextual menu in the event-B Explorer.

To disable the automated prover, open Rodin Preferences (menu Window > Preferences...). In the tree in the left-hand panel, select Event-B > Sequent Prover > Auto-tactic. Then, in the right-hand panel ensure that the checkbox labelled Enable auto-tactic for proving is disabled.

To review a proof obligation, just open it in the interactive prover, then click on the review button (this is a round blue button with a R in the proof control toolbar). The proof obligation should now labelled with the same icon in the event-B explorer.

What are the ASCII shortcuts for mathematical operators

The ASCII shortcuts that can be used for entering mathematical operators are described in the help of the Rodin keyboard plug-in. In the help system, this page has the following path Rodin Keyboard User Guide > Getting Started > Special Combos.

This page is also available in the dynamic help system. The advantage of using dynamic help is that it allows to display the help page side-by-side with the other views and editors. To start the dynamic help, click Help > Dynamic Help, then click All Topics and select the page in the tree.

Rodin (and eclipse) doesn't take into account the MOZILLA_FIVE_HOME environment variable

You have to add a properties by appending the following code to your






No More Handles

On Windows platforms, it may happen that Rodin crashes, complaining about "no more handles". This is an OS specific limitation, described here and there. A workaround is provided in this site.

Software installation fails

When installing softwares from update sites (Help > Install New Software...) it sometimes fails with an error saying something like:

No repository found containing: osgi.bundle,org.eclipse.emf.compare,1.0.1.v200909161031
No repository found containing: osgi.bundle,org.eclipse.emf.compare.diff,1.0.1.v200909161031

This is an eclipse/p2 bug, referenced here.

The workaround is to:

  • go to Window > Preferences > Install/Update > Available Software Sites
  • sites then add them back again, which can be achieved in the "Available Software Sites" preference page by:
  • select all update sites (by highlighting them all those that are checked)
  • Export them
  • Remove them
  • restart Rodin
  • go back to the preference page and import update sites back (from the previously exported file)


Witness for
missing. Default witness generated

A parameter as disappeared during a refinement. If this is intentional, you have to add a witness telling how the abstract parameter is refined.

should not occur free in a witness

You refer to


in a witness predicate where


is a disappearing abstract variable or parameter which is not set as the witness label.

, I get Witness
must be a disappearing abstract variable or parameter

The witness is for the after value of the abstract variable, hence you should use the primed variable. The witness label should be


, and the predicate should refer to



I've added a witness for
but it keeps saying "Identifier
has not been defined"

As specified in the modelling language manual, the witness must be labelled by the name


of the concrete variable being concerned.

What are type expressions in Event-B?

The type expressions are defined recursively as follows:

  • Built-in types: ℤ, BOOL (Note that ℕ is NOT a type expressions).
  • Any carrier set is a type expression.
  • If T is a type expression then Failed to parse (lexing error): ℙ(T) is a type expression.
  • If S and T are type expressions then Failed to parse (lexing error): S × T is a type expression.


How can I do a Proof by Induction?

This page about proof by induction will give you some starting tips.

Labels of proof tree nodes explained

  • ah
    means add hypothesis,
  • eh
    means rewrite with equality from hypothesis from left to right,
  • he
    means rewrite with equality from hypothesis from right to left,
  • rv
    tell us that this goal as been manually reviewed,
  • sl/ds
    means selection/deselection,
  • PP
    means discharged by the predicate prover
  • ML
    means discharged by the mono lemma prover

How to contribute and develop ?

See the Developer FAQ page.