RODIN is an Eclipse-based platform for the formal specification of systems in Event-B. Unfortunately, I have to use it (although, not too much). It is, however, the worst piece of software I have seen for a long time. As such I have decided to share my frustration also with you…

Event-B has a main language structure the Event. An Event has a status (not important for now), local variables (which have a type), guards (which define when the event can be triggered) and actions (which specify how to change the state variables.

I decided to create a local variable rr, but unfortunately I managed to put a space after the name “rr”… so it read “rr ” [look out for the space]. Immediately, RODIN refuses the variable definition and highlights all the occurrences of rr throughout the body of the event as undefined variable. WOW!

I leave you with a screenshot: