Rodin Handbook
This 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
 |
 |
 |
Rodin User’s Handbook v.2.8 |  |
 |
 |
2.2.3 Predicate Logic
In predicate logic, statements (which are called predicates) can be expressed with variables that can be quantified (e.g. “for all values of 
…”). Event-B uses predicate logic with the following features:
Predicates and expressions are distinguished.
All expressions have a data type, e.g. integer or set of integers.
Quantification over variables, not predicates, is supported. This includes quantification over sets.
A partial function semantics is included, e.g. the predicate
is not a tautology because 
does not represent a valid value. Comprehension sets are supported.
Predicates can be evaluated to a Boolean value.
|
|
|
|
|
|