4.2.11 Where vs. When: What’s going on?

You may have noticed that both in this tutorial, as well as in the tool, events sometimes use the keyword “when” and sometimes “where”. The idea of this was to make the formal statements more intuitive. Unfortunately, this created more confusion than anything else.

The short answer is: “when” and “where” in events have exactly the same meaning, for all practical purposes.

The long answer is: In some contexts (but not all), the tool changes the keywords to make the meaning of the event more apparent. The distinguishing factor is the parameter: an event without a parameter uses the keyword “when”, and an event with a parameter uses the keyword “where”.

To make things even more confusing, this doesn’t apply everywhere: The Event-B structural editor always uses the keyword “where”, but the pretty print for the Event-B structural editor switches between the two. The default Rodin editor always uses the keyword "where". The Event-B syntax in this handbook has been generated with the L^aT_eXplugin, which also switches between the two keywords.