View source for Changes to the Mathematical Language of Event-B

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 <math>\id</math>
* the first projection  <math>\prjone</math>
* the second projection <math>\prjtwo</math>

These operators are defined as follows in the old version:

 <math>
 \begin{matrix}
  E\mapsto F &\in\id(S) && E\in S\;\land\; F = E\\
  (E\mapsto F)\mapsto G &\in\prjone(r)
  && E\mapsto F\in r\;\land\; G = E\\
  (E\mapsto F)\mapsto G &\in\prjtwo(r)
  && E\mapsto F\in r\;\land\; G = F    .
 \end{matrix}
 </math>

If we drop the parameter, we get
much more straightforward definitions that capture the essence of the
operator.  The new definitions are

 <math>
 \begin{matrix}
 E\mapsto F &\in\id && E = F\\
 (E\mapsto F)\mapsto G &\in\prjone && E = G\\
 (E\mapsto F)\mapsto G &\in\prjtwo && F = G    .
 \end{matrix}
 </math>

We have the following equivalence between the old
and the new versions of the operators

 <math>
 \begin{matrix}
    \textbf{Old Version} & \textbf{New Version}\\
    \id(S)  & S\domres id\\
    \prjone(r) & r\domres\prjone\\
    \prjtwo(r) & r\domres\prjtwo  .
 \end{matrix}
 </math>

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 <math>r</math> is irreflexive, one would now write
<math>r\binter\id = \emptyset</math>.

== Partition ==

A new partition predicate is introduced. It is intended to provide an easier way to enter enumerated sets, while getting rid of the <math>\frac{n(n-1)}{2}</math> axioms needed to express pairwise distinctness (or disjointness). The partition operator is defined as follows:

 <math>
 \begin{array}{ll}
 partition(E_0, E_1, \ldots, E_n)\defi &
  E_0 = E_1\bunion \cdots\bunion E_n \\ &
  \;\land\; E_1\binter E_2=\emptyset
  \;\land\;\cdots
  \;\land\; E_{n-1}\binter E_n = \emptyset \\ &
  (\;\land\; i \ne j \limp E_i \binter E_j = \emptyset ) \\
 \end{array}
 </math>


where the <math>E_i</math> are expressions bearing the same type.

Then, we can enter into a context :

 <math>
  \begin{array}{ll}
    \mathsf{set}  & S\\
    \mathsf{constant}  & a_1\\
    \vdots & \vdots\\
    \mathsf{constant}  & a_n\\
    \mathsf{axiom}  & partition(S, \{a_1\}, \ldots, \{a_n\})
  \end{array}
 </math>

which is a particular case of a set being defined by listing all its elements.

== Operator Associativity ==

Operators used to build sets of relations or functions, viz.
* relation
* total relation
* surjective relation
* total surjective relation
* partial function
* total function
* partial injection
* total injection
* partial surjection
* total surjection
* bijection

have no more relative priorities and lose associativity. Instead, users have to make it explicit by entering parenthesis in formulas.