Difference between revisions of "Changes to the Mathematical Language of Event-B"
imported>Nicolas |
imported>Nicolas |
||
Line 10: | Line 10: | ||
These operators are defined as follows: | These operators are defined as follows: | ||
− | <math> | + | <math> |
− | \begin{matrix} | + | \begin{matrix} |
E\mapsto F &\in\id(S) && E\in S\;\land\; F = E\\ | E\mapsto F &\in\id(S) && E\in S\;\land\; F = E\\ | ||
(E\mapsto F)\mapsto G &\in\prjone(r) | (E\mapsto F)\mapsto G &\in\prjone(r) | ||
Line 17: | Line 17: | ||
(E\mapsto F)\mapsto G &\in\prjtwo(r) | (E\mapsto F)\mapsto G &\in\prjtwo(r) | ||
&& E\mapsto F\in r\;\land\; G = F . | && E\mapsto F\in r\;\land\; G = F . | ||
− | \end{matrix} | + | \end{matrix} |
− | </math> | + | </math> |
If we drop the parameter, we get | If we drop the parameter, we get | ||
Line 24: | Line 24: | ||
operator. The new definitions are | operator. The new definitions are | ||
− | <math> | + | <math> |
− | \begin{matrix} | + | \begin{matrix} |
− | E\mapsto F &\in\id && E = F\\ | + | E\mapsto F &\in\id && E = F\\ |
− | (E\mapsto F)\mapsto G &\in\prjone && E = G\\ | + | (E\mapsto F)\mapsto G &\in\prjone && E = G\\ |
− | (E\mapsto F)\mapsto G &\in\prjtwo && F = G . | + | (E\mapsto F)\mapsto G &\in\prjtwo && F = G . |
− | \end{matrix} | + | \end{matrix} |
− | </math> | + | </math> |
We have the following equivalence between the old | We have the following equivalence between the old | ||
and the new versions of the operators | and the new versions of the operators | ||
− | <math> | + | <math> |
− | \begin{matrix} | + | \begin{matrix} |
\textbf{Old Version} & \textbf{New Version}\\ | \textbf{Old Version} & \textbf{New Version}\\ | ||
\id(S) & S\domres id\\ | \id(S) & S\domres id\\ | ||
\prjone(r) & r\domres\prjone\\ | \prjone(r) & r\domres\prjone\\ | ||
\prjtwo(r) & r\domres\prjtwo . | \prjtwo(r) & r\domres\prjtwo . | ||
− | \end{matrix} | + | \end{matrix} |
− | </math> | + | </math> |
Moreover, in the case where the parameter is not needed, then it can | Moreover, in the case where the parameter is not needed, then it can | ||
Line 48: | Line 48: | ||
to express that a relation <math>r</math> is irreflexive, one would now write | to express that a relation <math>r</math> is irreflexive, one would now write | ||
<math>r\binter\id = \emptyset</math>. | <math>r\binter\id = \emptyset</math>. | ||
− | |||
− | |||
== Partition == | == Partition == |
Revision as of 16:18, 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
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.