3.3.7 Typing

$\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}$


of type


$\textsf{E}\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}\alpha $ is an expression that has exactly the value of $\textsf{E}$ but its type is specified by the type expression $\alpha $ (

$\mathsf{\textsf{E}}$ is restricted to expressions whose type does not depend on an argument of that expression. These are the constant relations $\mathop {\mathrm{id}}\nolimits $, $\mathop {\mathrm{prj}_1}\nolimits $, $\mathop {\mathrm{prj}_2}\nolimits $ and the empty set $\emptyset $.

Another location where the operator can be used is the declaration of bound variables in quantifiers and patterns in lambda expressions. Each identifier can be followed by $\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}$ and the identifier’s type.


$\textsf{E}\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}\alpha = \textsf{E}$


$\textsf{E}\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}\alpha \in \alpha $ with $\textsf{E}\in \alpha $


$\mathcal{L}(\textsf{E}\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}\alpha ) \mathrel {\widehat=}\mathcal{L}(\textsf{E})$


The predicate $\emptyset =\emptyset $ is not correctly typed in Event-B because the types of $\emptyset $ are not inferable. A valid alternative would be:
$(\emptyset \mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}\mathord {\mathbb Z}) = \emptyset $

The predicate $\exists x,y ~ \mathord {\mkern 1mu\cdot \mkern 1mu}~  x\neq y$ is not correctly typed because the types of $x$ and $y$ cannot be inferred: A valid alternative (for integers) is:
$\exists x\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}\mathord {\mathbb Z},y ~ \mathord {\mkern 1mu\cdot \mkern 1mu}~  x\neq y$

The following lambda expression uses the $\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}$ operator:
$(\lambda x\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}\mathord {\mathbb Z}\mapsto y\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}\mathord {\mathrm{BOOL}}~ |~  x>0 ~ \mathord {\mkern 1mu\cdot \mkern 1mu}~  x+1)$
An arguably more readable version without the use of $\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}$ is:
$(\lambda x\mapsto y ~ |~  x>0 \land y\in \mathord {\mathrm{BOOL}}~ \mathord {\mkern 1mu\cdot \mkern 1mu}~  x+1)$