## 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: r:POW(A**B)). Because relations are so common, there is also a symbol to denote a relation, so a shorter way to write the above expression is (ASCII: r:A<->B).

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 domain of are all elements occurring on the left side and the range are all elements on the right .

To find out to which elements the objects of the set are related to, we can use the relational image: . Often we want to know to which object a single element is related. We just write it as a singleton set: .

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.