Rodin User’s Handbook v.2.4: Predicates

2.5.1 Predicates

In the traffic light example, we have already encountered several predicates: The invariants of a model and the guards of an event. The proof obligations generated by Rodin are also predicates. A predicate is simply an expression, the value of which is either true or false.

The simplest predicates are $\mathord {\top }$ (ASCII: true) and $\mathord {\bot }$ (ASCII: false). We can also assert if arbitrary objects of the same type are equal with $=$ or not equal with $\neq$ (ASCII: /=). Predicates can be combined with the usual logical operators:

	symbol	ASCII
conjunction (and)	$\land$	`&`
disjunction (or)	$\lor$	`or`
implication	$\mathbin \Rightarrow$	`=>`
equivalence	$\mathbin \Leftrightarrow$	`<=>`
negation (not)	$\lnot$	`not`

We can use universal quantification to express a statement that is valid for all possible values a variable might have. The universal quantifier is $\forall$ (ASCII: !). For example, in order to show that any given number $x$ greater than zero and multiplied with two is greater than one, we can use the following expression:

$\forall x \mathord {\mkern 1mu\cdot \mkern 1mu}x>0 \mathbin \Rightarrow 2\cdot x > 1 \qquad \quad \textrm{ASCII: } \texttt{!x.\ x>0\ =>\ 2*x\ >\ 1}$

When a variable is introduced by a quantifier, the type of the variable must be clear. In this case Rodin can infer that $x$ must be of type integer because the operator $<$ is defined only on integers. Sometimes the type cannot be inferred, e.g., in

$\forall a,b \mathord {\mkern 1mu\cdot \mkern 1mu}a\neq b \mathbin \Rightarrow b\neq a \qquad \quad \textrm{ASCII: } \texttt{!a,b.\ a/=b\ =>\ b/=a}$

$a$ and $b$ could be integers, Boolean values or some other type. In this case, we must make the type of the variables explicit by stating that $a$ and $b$ are elements of the appropriate sets. Let’s use integers again to correct the previous expression:

$\forall a,b \mathord {\mkern 1mu\cdot \mkern 1mu}a\in \mathord {\mathbb Z}\land b\in \mathord {\mathbb Z}\land a\neq b \mathbin \Rightarrow b\neq a \qquad \quad \textrm{ASCII: } \texttt{!a,b.\ a:INT \& b:INT \& a/=b => b/=a}$

The conjunction operator ( $\land$ ) has a stronger binding that the implication $\mathbin \Rightarrow$ , so the above expression is equivalent to

$\forall a,b \mathord {\mkern 1mu\cdot \mkern 1mu}(a\in \mathord {\mathbb Z}\land b\in \mathord {\mathbb Z}\land a\neq b) \mathbin \Rightarrow b\neq a$

$\includegraphics[width=7mm]{img/warning_64.png}$
If you are unsure which of the operators bind stronger, we advise you to use parenthesis to avoid mistakes.

Existential quantification on the other hand is used to state that there is an object of a certain type fulfilling a given property. The existential quantifier is $\exists$ (ASCII: #). The following example expression states that there is a Boolean value different from $\mathord {\mathrm{TRUE}}$ :

$\exists x \mathord {\mkern 1mu\cdot \mkern 1mu}x\in \mathord {\mathrm{BOOL}}\land x\neq \mathord {\mathrm{TRUE}}\qquad \quad \textrm{ASCII: } \texttt{\# x.\ x:BOOL\ \& \ x/=TRUE}$

As you can see, we again added type information for $x$ . We put the type information on the left side of the implication ( $\mathbin \Rightarrow$ ) for the universal quantification , but for existential quantification we add it via a conjunction ( $\land$ ).