2.1 Outline

Background before getting started (2.2): We give a brief description of what Event-B is, what it is being used for and what kind of background knowledge we expect.
Installation (2.3): We guide you through downloading, installing and starting Rodin and point out platform differences. We install the provers. We name the visible views and describe what they are doing.
A Machine, and nothing else (2.4): We introduce the first machine: a traffic light with booleans for signals. We introduce guards which result in the proof obligations being automatically discharged. We explain how proof labels are read without changing to the proof perspective.
Mathematical notation (2.5): At this point we quickly go through the most important aspects of predicate calculus and provide pointers to the reference chapter and to external literature. We cover everything used by the traffic light system, we introduce all data types and we provide a brief intoduction of sets and relations. We also explain the difference between predicates and expressions. For example, we explain here how to understand the difference between TRUE and $\top$ .
Introducing Contexts (2.6): We introduce contexts to apply the theoretical concepts that were introduced in the previous section. We use the Agatha-Puzzle to step by step introduce more and more complex elements. We point out that partitions are a typical pitfall, we cover theorems and also mention well-definedness.
Event-B Concepts (2.7): This is another theoretical section that provides more background about the previous examples. For instance, we analyze the anatomy of a machine and introduce all elements that a machine or context may have. We give references to literature about the theory but do not go into the details of the calculus. We describe the sees and refines concepts which will be applied in the next section. We will briefly mention concepts like data refinement and witnesses but leave the details to the literature.
Expanding the Traffic Light System (2.8): We apply what we learned in the previous section by introducing a context with traffic light colors and a refinement to integrate them. We will introduce another refinement for the push buttons.
Proving (2.9): So far all proof obligations were discharged automatically. Now we switch to the proving perspective and explore it for the first time. We change the configuration for the auto prover, invalidate proofs and show that with the new configuration they will not discharge any more. We prove a simple proof by hand and describe the provers available.
Complete Abrial Example (2.10): We will pick an interesting example from the Abrial book if we get permission. We can also use one of the Rodin Wiki Tutorial examples (e.g. Location Access Controller).
Outlook (2.11): This concludes the tutorial, but we will provide many pointers for further reading. In particular, we will point to the literature from the Deploy project and the Wiki and to plugins that solve specific problems.

Rodin Handbook

2.1 Outline