Rodin User’s Handbook v.2.8: Data types

2.5.2 Data types

We have seen that each identifier (i.e. a variable, constant or parameter) must have a distinguished type. If we can introduce an identifier anywhere, we usually must also add a predicate with which the identifier’s type can be determined. In the traffic light example, a variable cars_go was introduced and the type was set by an invariant $cars\_ go \in \mathord {\mathrm{BOOL}}$ . In the next section, we’ll see that the type of constants is set by axioms (also predicates) and later we’ll see that the type for parameters will be determined by using guards (again, predicates).

As a rule, each term in Event-B must have a certain type. When saving a Event-B component, Rodin starts the type checker to ensure that types are correctly used. For example, the terms on both sides of an equality ( $=$ ) must have the same type. If this is not the case, Rodin will generate an error message. For each type there exists a set that denotes exactly all elements that belong the type. We will now briefly give an overview about all types you might encounter.

Integers: We have already seen numbers, which are of type integer ( $\mathord {\mathbb Z}$ ). Example terms of type $\mathord {\mathbb Z}$ are $5$ , $x+7$ and $7 \cdot y - 3$ .
Booleans: We have already seen the Boolean type ( $\mathord {\mathrm{BOOL}}$ ) in the previous section (2.4). It has exactly two elements, $\mathord {\mathrm{BOOL}}= \{ \mathord {\mathrm{TRUE}},$ $\mathord {\mathrm{FALSE}}\}$ .
Carrier sets: A user can introduce a new type by adding its name to the Sets section of a context. We see that in more detail in the next section (2.6).
Sets: If we have terms of a certain type, we can easily construct sets of that type. E.g. $1$ and $2\cdot x$ denote integers ( $\mathord {\mathbb Z}$ ) and $\{ 1,2\cdot x\}$ is a set of integers ( $\mathop {\mathbb P\hbox{}}\nolimits (\mathord {\mathbb Z})$ ). $\mathop {\mathbb P\hbox{}}\nolimits (S)$ (ASCII: POW) denotes the power set (the set of all subsets) of $S$ .
Pairs: If we have two terms, we can construct a pair. For example, with $2$ and $\mathord {\mathrm{TRUE}}$ , we can construct the pair $2\mapsto \mathord {\mathrm{TRUE}}$ (ASCII: 2|->TRUE). The type of that pair is $\mathord {\mathbb Z}\mathbin \times \mathord {\mathrm{BOOL}}$ , where $\mathbin \times$ denotes the Cartesian product. Set of pairs (“relations”) play an important role in modelling languages like Event-B.

$\includegraphics[width=7mm]{img/warning_64.png}$
Please do not confuse predicates and Boolean values! For example, if you want to express the condition “if the variable $b$ is true, $x$ should be greater than 2”, you cannot write $b \mathbin \Rightarrow x>2$ (That would produce a syntax error). Instead you have to write $b = \mathord {\mathrm{TRUE}}\mathbin \Rightarrow x>2$ .

In Section 3.3 the types of each operator in Event-B are described in detail.

Rodin Handbook

2.5.2 Data types