![]()
Goals: In order to understand how basic properties of a model can be expressed in Event-B, we need a brief introduction of predicates, terms and data types.
In Event-B, we use a mathematical notation to describe the systems we want to model. This allows us to be very precise about the model’s properties.