## Rodin HandbookThis work is sponsored by the Deploy Project This work is sponsored by the ADVANCE Project This work is licensed under a Creative Commons Attribution 3.0 Unported License |
## 3.2 Event-B’s modelling notationIn 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:
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. |