3.2 Event-B’s modeling notation

In Event-B, we have two types of components: contexts and machines. Here we describe briefly the different elements of a context or machine. We do not use a specific syntax for describing the components because the syntax is dependent on the editor that is used. The default editor requires a structure which contains the elements that are described here.

Proof obligations are generated to guarantee certain properties of the modeled system. We will explain here which proof obligations are generated and we will list the goal and hypotheses that can be used when performing the proof for each one. This is done in the form:

	Description
Name	Label of the proof obligation (label refers to the label of the respective axiom/invariant/guard/etc.)
Goal	Goal that should be proved

$\includegraphics[width=7mm]{img/info_64.png}$
Please note that Rodin often does not show a proof obligation if it is obviously true. If you expect a proof obligation that Rodin does not show, you can enforce that the proof obligation is showed by changing the model temporarily in a way that the proof cannot be proven. E.g. you can introduce a division by zero to see the corresponding well-definedness condition.

We first describe context and machines and how their consistency is proven. There are several locations where proof obligations due to well-definedness conditions or predicates marked as theorems are raised. We summarized the proof obligations in separate sections (3.2.4 resp. 3.2.5).

Rodin Handbook

3.2 Event-B’s modeling notation