Rodin User’s Handbook v.2.8: Introduction

3.3.1 Introduction

In the following section, we use sans serif letters like $\textsf{a}$ , $\textsf{A}$ , $\textsf{b}$ , $\textsf{B}$ , …as placeholders for arbitrary expressions instead of $a$ , $A$ , $b$ , $B$ which represent Event-B identifiers. For example, the $\textsf{e}$ and $\textsf{S}$ in $\textsf{e}\in \textsf{S}$ could be a placeholder for $5+2$ and $\mathord {\mathbb N}$ .

We use the $\textsf{A}\mathrel {\widehat=}\textsf{B}$ to state that an expression, predicate or assignment $\textsf{A}$ can be equivalently rewritten as $\textsf{B}$ if $\textsf{A}$ ’s well-definedness condition is fulfilled. We have tried to find a balance between having a precise and concise description for all Event-B’s mathematical components and having a text that is still easily readable. Many of the operators can be expressed using other, simpler constructs. Other, like equality ( $=$ ) or universal quantification ( $\forall$ ) are simply described with natural language.

When we introduce new identifiers while expressing an operator (e.g. by using a set comprehension), we assume that the new identifier does not occur free in the rewritten expressions (see Section 3.3.1.3 for more information on free identifiers).

$\includegraphics[width=7mm]{img/info_64.png}$
For a concise summary of the Event-B mathematical toolkit, download the four-page Event-B Cheat Sheet. We would like to thank Ken Robinson for making it available.

3.3.1.1 Data types

In Event-B we have 3 kinds of basic data types:

$\mathord {\mathbb Z}$ is the set of all integers.
$\mathord {\mathrm{BOOL}}$ is the set of Booleans. It has two elements $\mathord {\mathrm{BOOL}}= \{ \mathord {\mathrm{TRUE}},\mathord {\mathrm{FALSE}}\}$ .
Users can define carrier sets. These are defined in the Sets section of a context. Carrier sets are never empty. There is no other assumption made about carrier sets unless it is stated explicitly as an axiom.

From all data types $\alpha , \beta$ , two other kinds of data types can be constructed:

$\mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ contains the sets of elements of $\alpha$ .
$\alpha \mathbin \times \beta$ is the set of pairs where the first element is of type $\alpha$ and the second element is of type $\beta$ .

Expressions that are constructed by the rules above are called type expressions.

3.3.1.1.1 A note about the notation

We use the Greek letters $\alpha$ , $\beta$ , $\gamma$ , …to represent arbitrary data types. For an expression $\textsf{E}$ , we write $\textsf{E}\in \alpha$ to state that $\textsf{E}$ is of type $\alpha$ . In the following descriptions of Event-B’s mathematical constructs, we will describe the types of all constructs and their components.

For example, we will describe the maplet $\textsf{E}\mapsto \textsf{F}$ whose type is defined by $\textsf{E}\mapsto \textsf{F}\in \alpha \mathbin \times \beta$ with $\textsf{E}\in \alpha$ and $\textsf{F}\in \beta$ . We do not restrict the types of $\alpha$ and $\beta$ .

For predicates, we simply describe the data types of their components. The predicate itself does not have a type. For example, consider the components’ types for the equality of two expressions $\textsf{E}=\textsf{F}$ : $\textsf{E}\in \alpha$ and $\textsf{F}\in \alpha$ . By stating that $\textsf{E}$ and $\textsf{F}$ are both of type $\alpha$ , we express that both expressions must have the same type but do not make any further assumptions about their types.

3.3.1.2 Well-definedness

A predicate which describes the condition under which an expression or predicate in Event-B can be safely evaluated is the well-definedness condition. An example with integer division makes this clear: The expression $x\div y$ only makes sense when $y\neq 0$ .

Well-definedness conditions are usually used for well-definedness proof obligations (3.2.5).

In Rodin, the $\mathcal{L}$ -operator defines which well-defined condition a predicate or expression has. When applied to the above example, integer division can be formatted as follows: $\mathcal{L}(x\div y) \mathrel {\widehat=}y\neq 0$ .

In the following sections, we state for each mathematical construct what the well-definedness conditions are. In many cases, this is just the conjunction of the well-definedness conditions for the different syntactical parts of a construct.

$\includegraphics[width=7mm]{img/info_64.png}$
The $\mathcal{L}$ -operator cannot be expressed in Event-B itself. It is only used to describe Event-B’s concept of well-definedness and how the well-definedness proof obligations are generated.

3.3.1.3 Free identifiers

Free identifiers in predicates and expressions are those identifiers which are used but not introduced by quantifiers. More formally, we define the set of free identifiers $\textsl{Free}(\textsf{E})$ of an expression or predicate $E$ recursively as follows:

Expression / Predicate	Free identifiers
Identifier $x$	$\{ x\}$
Integer $n$	$\emptyset$
$\begin{array}{lllll} \mathord {\top }& \mathord {\bot }& \mathord {\mathrm{BOOL}}& \mathord {\mathrm{TRUE}}& \mathord {\mathrm{FALSE}}\\ \emptyset & \mathop {\mathrm{id}}\nolimits & \mathop {\mathrm{prj}_1}\nolimits & \mathop {\mathrm{prj}_2}\nolimits & \mathord {\mathbb Z}\\ \mathord {\mathbb N}& \mathord {\mathbb N}_1 \end{array}$	$\emptyset$
$\begin{array}{lllll} \lnot \textsf{A}& \mathop {\mathrm{bool}}\nolimits (\textsf{A}) & \mathop {\mathbb P\hbox{}}\nolimits (\textsf{A}) & \mathop {\mathbb P\hbox{}}\nolimits _1(\textsf{A}) \\ \mathrm{finite}(\textsf{A}) & \mathop {\mathrm{card}}\nolimits (\textsf{A}) & \mathrm{union}(\textsf{A}) & \mathrm{inter}(\textsf{A}) \\ \textsf{A}^{-1} & \mathop {\mathrm{dom}}\nolimits (\textsf{A}) & \mathop {\mathrm{ran}}\nolimits (\textsf{A}) & -\textsf{A}\\ \min (\textsf{A}) & \max (\textsf{A}) \end{array}$	$\textsl{Free}(\textsf{A})$
$\begin{array}{lllll} \textsf{A}\land \textsf{B}& \textsf{A}\lor \textsf{B}& \textsf{A}\mathbin \Rightarrow \textsf{B}& \textsf{A}\mathbin \Leftrightarrow \textsf{B}& \textsf{A}=\textsf{B}\\ \textsf{A}\neq \textsf{B}& \textsf{A}\in \textsf{B}& \textsf{A}\not\in \textsf{B}& \textsf{A}\subseteq \textsf{B}& \textsf{A}\not\subseteq \textsf{B}\\ \textsf{A}\subset \textsf{B}& \textsf{A}\not\subset \textsf{B}& \textsf{A}\mathbin {\mkern 1mu\cup \mkern 1mu}\textsf{B}& \textsf{A}\mathbin {\mkern 1mu\cap \mkern 1mu}\textsf{B}& \textsf{A}\setminus \textsf{B}\\ \textsf{A}\mathbin \times \textsf{B}& \textsf{A}\mathbin \leftrightarrow \textsf{B}& \textsf{A}\mathbin {\leftarrow \mkern -14mu\leftrightarrow }\textsf{B}& \textsf{A}\mathbin {\leftrightarrow \mkern -14mu\rightarrow }\textsf{B}& \textsf{A}\mathbin {\leftrightarrow \mkern -14mu\leftrightarrow }\textsf{B}\\ \textsf{A}\mathbin \lhd \textsf{B}& \textsf{A}\mathbin {\lhd \mkern -14mu-}\textsf{B}& \textsf{A}\mathbin \rhd \textsf{B}& \textsf{A}\mathbin {\rhd \mkern -14mu-}\textsf{B}& \textsf{A}\mathbin ;\textsf{B}\\ \textsf{A}\circ \textsf{B}& \textsf{A}\mathbin {\lhd \mkern -9mu-}\textsf{B}& \textsf{A}\mathbin \\| \textsf{B}& \textsf{A}\mathbin \otimes \textsf{B}& \textsf{A}[\textsf{B}] \\ \textsf{A} \mathbin {\mkern 6mu\mapstochar \mkern -6mu\rightarrow } \textsf{B}& \textsf{A}\mathbin \rightarrow \textsf{B}& \textsf{A} \mathbin {\mkern 9mu\mapstochar \mkern -9mu\rightarrowtail } \textsf{B}& \textsf{A}\mathbin \rightarrowtail \textsf{B}& \textsf{A} \mathbin {\mkern 6mu\mapstochar \mkern -6mu\twoheadrightarrow } \textsf{B}\\ \textsf{A}\mathbin \twoheadrightarrow \textsf{B}& \textsf{A}\mathbin { \rightarrowtail \mkern -18mu\twoheadrightarrow } \textsf{B}& \textsf{A}(\textsf{B}) & \textsf{A}+\textsf{B}& \textsf{A}-\textsf{B}\\ \textsf{A}\cdot \textsf{B}& \textsf{A}\div \textsf{B}& \textsf{A}\bmod \textsf{B}& \textsf{A}\mathbin {\widehat{\enskip }}\textsf{B}& \textsf{A}\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}\textsf{B}\end{array}$	$\textsl{Free}(\textsf{A})\cup \textsl{Free}(\textsf{B})$
$\begin{array}{lllll} \{ ~ \textsf{E}_1,\ldots ,\textsf{E}_ n~ \} & \mathrm{partition}(\textsf{E}_1,\ldots ,\textsf{E}_ n) \end{array}$	$\textsl{Free}(\textsf{E}_1)\cup \ldots \cup \textsl{Free}(\textsf{E}_ n)$
$\begin{array}{lllll} \forall \textsl{ids}~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}& \exists \textsl{ids}~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}\end{array}$	$\textsl{Free}(\textsf{P})\setminus \textsl{ids}$
$\begin{array}{lllll} \{ ~ \textsl{ids}~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ \|~ \textsf{E}~ \} & \bigcup \nolimits \textsl{ids}~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ \|~ \textsf{E}& \bigcap \nolimits \textsl{ids}~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ \|~ \textsf{E}\end{array}$	$(\textsl{Free}(\textsf{P})\cup \textsl{Free}(\textsf{E}))\setminus \textsl{ids}$
$\begin{array}{lllll} \{ ~ \textsf{E}~ \|~ \textsf{P}~ \} & \bigcup \nolimits \textsf{E}~ \|~ \textsf{P}& \bigcap \nolimits \textsf{E}~ \|~ \textsf{P}\end{array}$	$\textsl{Free}(\textsf{P})\setminus \textsl{Free}(\textsf{E})$

3.3.1.4 Structure of the subsections

The following reference subsections will have the form the form:

math. Symbol	`ASCII representation`	Name of the operator
…	…	…

Description: A short description of what the operator does
Definition: A formal definition of what the operator does
Types: A description of the types of all arguments and, if the operation is an expression, the expression’s type
WD: A description of the well-definedness conditions using the $\mathcal{L}$ operator
Feasibility: Non-deterministic assignments may have feasibility conditions. These are used in the proof obligations of an event (3.2.4.4.6).
Example: For some constructs, an example is provided to clarify their use.

Rodin Handbook