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 |
3.2.8 Visibility of identifiersExpressions and predicates are comprised of certain Event-B elements. The following table describes the elements that each predicate or expression use:
However, expressions and predicates can only use elements that are identified within a specific scope:
Witnesses and actions have additional elements in their scope. Section 3.2.4.4.4 provides more information about witnesses, and Section 3.3.8 explains the scope for actions that have different types of assignments in further detail. |