User Manual for Rodin v.2.3: 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 that evaluates to 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 should hold for all possible values a variable might have. 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:

$\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 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. Let’s express the statement 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 for the universal quantification on the left side of the implication ( $\mathbin \Rightarrow$ ), but for existential quantification we add it via a conjunction ( $\land$ ).

Rodin Handbook

2.5.1 Predicates