User Manual for Rodin v.2.3: 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 typed by an invariant $cars\_ go \in \mathord {\mathrm{BOOL}}$ . In the next section, we’ll see constants that will be typed by axioms (also predicates) and later we’ll see parameters that will be typed by guards (again, predicates).

In general, each term in Event-B has 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

An 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 modeling 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 raise a syntax error). Instead you can write $b = \mathord {\mathrm{TRUE}}\mathbin \Rightarrow x>2$ .

In the reference section (3.3) the types of each operator in Event-B are described in detail.

Rodin Handbook

2.5.2 Data types