5 - The Event-B modeling notation and proof obligation rules

Summary

In previous chapters, we used the Event-B notation and the various corresponding proof obligation rules without introducing them initially in a systematic fashion. We presented them instead in the examples when they were needed. This was sufficient for the simple examples we studied because we used part of the notation and part of the proof obligation rules only. But it might not be adequate to continue in this way when presenting more elaborate examples in subsequent chapters. The purpose of this chapter is thus to correct this. First, we present the Event-B notation as a whole, in particular the bits not used so far, and then we present all the proof obligation rules. This will be illustrated with a simple running example.

The Event-B notation

Introduction: machines and contexts

The primary concept in doing formal developments in Event-B is that of a model. A model contains the complete mathematical development of a Discrete Transition System. It is made of several components of two kinds: machines and contexts. Machines contain the dynamic parts of a model, namely variables, invariants, theorems, variants, and events, whereas contexts contain the static parts of a model, namely carrier sets, constants, axioms, and theorems. This is illustrated in Fig. 5.1. Items belonging to machines or contexts (variables, invariants, etc.) are called modeling elements.

A model can contain contexts only, or machines only, or both. In the first case, the model represents a pure mathematical structure with sets, constants, axioms, and theorems.