## Rodin HandbookThis work is sponsored by the Deploy Project This work is sponsored by the ADVANCE Project This work is licensed under a Creative Commons Attribution 3.0 Unported License |
## 2.5.5 Relations Relations are a powerful instrument when modelling systems. From a mathematical point of view, a relation is just a set of pairs. Formally, when we have two sets and , we can specify that is a relation between both by (ASCII: With , we can check if two elements and are related in respect to . We use a small example to illustrate relations. Let and . We define the relation with . The To find out to which elements the objects of the set are related to, we can use the Event-B supports several operators to work with relations (3.3.5). We will not go into more detail during the course of the tutorial. An important special case of relations are functions. Functions are relations where each element of the domain is uniquely related to one element of the range. Event-B directly supports operators to describe partial and total functions, which can be injective, surjective or bijective. |