Rodin Handbook
This work is sponsored by the Deploy Project
This work is licensed under a Creative Commons Attribution 3.0 Unported License
 |
 |
 |
User Manual for Rodin v.2.3 |  |
 |
 |
4.5.2 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: Without parameter, “when” is used, with a parameter, “where” is used.
To confuse things even more, this doesn’t apply everywhere: The structural editor always shows “where”, but the pretty print toggles between the two. The Event-B in this handbook has been generated with the LaTeXplugin, which also toggles the keyword.
|
|
|
|
|
|