## Rodin HandbookThis work is sponsored by the Deploy Project This work is sponsored by the ADVANCE Project This work is licensed under a Creative Commons Attribution 3.0 Unported License |
## 2.5.1 PredicatesIn 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 (ASCII:
We can use When a variable is introduced by a quantifier, the type of the variable must be clear. In this case Rodin can infer that must be of type integer because the operator is defined only on integers. Sometimes the type cannot be inferred, e.g., in and could be integers, Boolean values or some other type. In this case, we must make the type of the variables explicit by stating that and are elements of the appropriate sets. Let’s use integers again to correct the previous expression: The conjunction operator () has a stronger binding that the implication , so the above expression is equivalent to
As you can see, we again added type information for . We put the type information on the left side of the implication () for the universal quantification , but for existential quantification we add it via a conjunction (). |