3.2 Event-B’s modelling 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.

Proof obligations are generated to guarantee that certain properties of the modelled system are valid. 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 will be presented in the form:

Please note that Rodin often does not show a proof obligation if it is obviously true. If you expect to see a proof obligation that Rodin does not show, you can force that the proof obligation to be shown by changing the model temporarily so that the proof obligation cannot be automatically discharged. For example, you could introduce a division by zero to see the corresponding well-definedness condition.

We will begin by describing contexts and machines and how to prove their consistency. There are several locations where proof obligations for well-definedness conditions or predicates marked as theorems are raised. We summarized the proof obligations in separate sections. Well-definedness proof obligations are discussed in Section 3.2.5 and proof obligations for theorems are discussed in Section 3.2.6.