Changes to the Mathematical Language of Event-B
This document describes the evolution of the Event-B mathematical language that happened in release 1.0.0. See Event-B_Mathematical_Language for a full description of the language.
Generic Identity and Projections
Three operators were still unary while they could be atomic and generic:
- the identity relation
- the first projection
- the second projection
These operators are defined as follows in the old version:
If we drop the parameter, we get much more straightforward definitions that capture the essence of the operator. The new definitions are
We have the following equivalence between the old and the new versions of the operators
Moreover, in the case where the parameter is not needed, then it can be dropped altogether: no domain restriction is needed. For instance, to express that a relation is irreflexive, one would now write .
A new partition predicate is introduced. It is intended to provide an easier way to enter enumerated sets, while getting rid of the axioms needed to express pairwise distinctness (or disjointness). The partition operator is defined as follows:
where the are expressions bearing the same type.
Then, we can enter into a context :
which is a particular case of a set being defined by listing all its elements.
Operators used to build sets of relations or functions, viz.
- total relation
- surjective relation
- total surjective relation
- partial function
- total function
- partial injection
- total injection
- partial surjection
- total surjection
have no more relative priorities and loose associativity. Instead, users have to make it explicit by entering parenthesis in formulas.