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.2 Data typesWe have seen that each identifier (i.e. a variable, constant or parameter) must have a distinguished type. If we can introduce an identifier anywhere, we usually must also add a predicate with which the identifier’s type can be determined. In the traffic light example, a variable cars_go was introduced and the type was set by an invariant . In the next section, we’ll see that the type of constants is set by axioms (also predicates) and later we’ll see that the type for parameters will be determined by using guards (again, predicates). As a rule, each term in Event-B must have a certain type. When saving a Event-B component, Rodin starts the type checker to ensure that types are correctly used. For example, the terms on both sides of an equality () must have the same type. If this is not the case, Rodin will generate an error message. For each type there exists a set that denotes exactly all elements that belong the type. We will now briefly give an overview about all types you might encounter.
In Section 3.3 the types of each operator in Event-B are described in detail. |