Difference between revisions of "Changes to the Mathematical Language of Event-B"
imported>Laurent |
imported>Mathieu m (category) |
||
Line 97: | Line 97: | ||
have no more relative priorities and loose associativity. Instead, users have to make it explicit by entering parenthesis in formulas. | have no more relative priorities and loose associativity. Instead, users have to make it explicit by entering parenthesis in formulas. | ||
+ | |||
+ | [[Category:Event-B]] | ||
+ | [[Category:User documentation]] |
Revision as of 14:05, 6 April 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.
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
.
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 loose associativity. Instead, users have to make it explicit by entering parenthesis in formulas.