Difference between revisions of "Changes to the Mathematical Language of Event-B"
imported>Nicolas m (→Partition) |
imported>Nicolas m (→Partition) |
||
Line 56: | Line 56: | ||
<math> | <math> | ||
− | \begin{ | + | \begin{array}{ll} |
partition(E_0, E_1, \ldots, E_n)\defi & | partition(E_0, E_1, \ldots, E_n)\defi & | ||
E_0 = E_1\bunion \cdots\bunion E_n \\ & | E_0 = E_1\bunion \cdots\bunion E_n \\ & | ||
Line 63: | Line 63: | ||
\;\land\; E_{n-1}\binter E_n = \emptyset \\ & | \;\land\; E_{n-1}\binter E_n = \emptyset \\ & | ||
(\;\land\; i \ne j \limp E_i \binter E_j = \emptyset ) \\ | (\;\land\; i \ne j \limp E_i \binter E_j = \emptyset ) \\ | ||
− | \end{ | + | \end{array} |
</math> | </math> | ||
Line 80: | Line 80: | ||
\end{array} | \end{array} | ||
</math> | </math> | ||
+ | |||
+ | which is a particular case of a set being defined by listing all its elements. | ||
== Operator Associativity == | == Operator Associativity == | ||
{{TODO}} | {{TODO}} |
Revision as of 15:28, 12 March 2009
This document describes the evolution of the Event-B mathematical language that will soon take place. The previous version of the language will still be supported.
Identity and Projections
Three operators were still unary while they could be atomic:
- the identity relation
- the first projection
- the second projection
These operators are defined as follows:
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
.
Partition
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.
Operator Associativity
TODO