User Manual for Rodin v.2.3: Introduction

3.3.1 Introduction

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}}\}$ .
User defined 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$ contains the pairs where the first element is of type $\alpha$ and the second element 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 $E$ , we write $E\in \alpha$ to state that $E$ is of type $\alpha$ . In the following descriptions of Event-B’s mathematical construct we describe the types of all constructs and their components.

For example, we will describe the maplet $E\mapsto F$ which is defined as $E\mapsto F\in \alpha \mathbin \times \beta$ with $E\in \alpha$ and $F\in \beta$ . We do not make any restrictions on the types $\alpha$ and $\beta$ .

For predicates, we just describe the data types of their components. The predicate itself does not have a type. For example, consider the components’ types of the equality of two expressions $E=F$ : $E\in \alpha$ and $F\in \alpha$ . By stating that $E$ and $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$ makes only sense when $y\neq 0$ .

Well-definedness conditions are usually used for the well-definedness proof obligations.

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.

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 Free(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 A & \mathop {\mathrm{bool}}\nolimits (A) & \mathop {\mathbb P\hbox{}}\nolimits (A) & \mathop {\mathbb P\hbox{}}\nolimits _1(A) & \mathrm{finite}(A) \\ \mathop {\mathrm{card}}\nolimits (A) & \mathrm{union}(A) & \mathrm{inter}(A) & A^{-1} & \mathop {\mathrm{dom}}\nolimits (A) \\ \mathop {\mathrm{ran}}\nolimits (A) & -A & \min (A) & \max (A) \end{array}$	$\textsl{Free}(A)$
$\begin{array}{lllll} A\land B & A\lor B & A\mathbin \Rightarrow B & A\mathbin \Leftrightarrow B & A=B \\ A\neq B & A\in B & A\not\in B & A\subseteq B & A\not\subseteq B \\ A\subset B & A\not\subset B & A\mathbin {\mkern 1mu\cup \mkern 1mu}B & A\mathbin {\mkern 1mu\cap \mkern 1mu}B & A\setminus B \\ A\mathbin \times B & A\mathbin \leftrightarrow B & A\mathbin {\leftarrow \mkern -14mu\leftrightarrow }B & A\mathbin {\leftrightarrow \mkern -14mu\rightarrow }B & A\mathbin {\leftrightarrow \mkern -14mu\leftrightarrow }B \\ A\mathbin \lhd B & A\mathbin {\lhd \mkern -14mu-}B & A\mathbin \rhd B & A\mathbin {\rhd \mkern -14mu-}B & A\mathbin ;B \\ A\circ B & A\mathbin {\lhd \mkern -9mu-}B & A\mathbin \\| B & A\mathbin \otimes B & A[B] \\ A \mathbin {\mkern 6mu\mapstochar \mkern -6mu\rightarrow } B & A\mathbin \rightarrow B & A \mathbin {\mkern 9mu\mapstochar \mkern -9mu\rightarrowtail } B & A\mathbin \rightarrowtail B & A \mathbin {\mkern 6mu\mapstochar \mkern -6mu\twoheadrightarrow } B \\ A\mathbin \twoheadrightarrow B & A\mathbin { \rightarrowtail \mkern -18mu\twoheadrightarrow } B & A(B) & A+B & A-B \\ A\cdot B & A\div B & A\bmod B & A\mathbin {\widehat{\enskip }}B & A\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}B \end{array}$	$\textsl{Free}(A)\cup \textsl{Free}(B)$
$\begin{array}{lllll} \{ ~ E_1,\ldots ,E_ n~ \} & \mathrm{partition}(E_1,\ldots ,E_ n) \end{array}$	$\textsl{Free}(E_1)\cup \ldots \cup \textsl{Free}(E_ n)$
$\begin{array}{lllll} \forall \textsl{ids}~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ P & \exists \textsl{ids}~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ P \end{array}$	$\textsl{Free}(P)\setminus \textsl{ids}$
$\begin{array}{lllll} \{ ~ \textsl{ids}~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ P~ \|~ E~ \} & \bigcup \nolimits \textsl{ids}~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ P~ \|~ E & \bigcap \nolimits \textsl{ids}~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ P~ \|~ E \end{array}$	$(\textsl{Free}(P)\cup \textsl{Free}(E))\setminus \textsl{ids}$
$\begin{array}{lllll} \{ ~ E~ \|~ P~ \} & \bigcup \nolimits E~ \|~ P & \bigcap \nolimits E~ \|~ P \end{array}$	$\textsl{Free}(P)\setminus \textsl{Free}(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 more formal definition
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 (Section 3.2.3.4.6).
Example: We add examples to some constructs to clarify their use.

Rodin Handbook