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.3.1 IntroductionIn the following section, we use sans serif letters like , , , , …as placeholders for arbitrary expressions instead of , , , which represent EventB identifiers. For example, the and in could be a placeholder for and . We use the to state that an expression, predicate or assignment can be equivalently rewritten as if ’s welldefinedness condition is fulfilled. We have tried to find a balance between having a precise and concise description for all EventB’s mathematical components and having a text that is still easily readable. Many of the operators can be expressed using other, simpler constructs. Other, like equality () or universal quantification () are simply described with natural language. When we introduce new identifiers while expressing an operator (e.g. by using a set comprehension), we assume that the new identifier does not occur free in the rewritten expressions (see Section 3.3.1.3 for more information on free identifiers).
3.3.1.1 Data typesIn EventB we have 3 kinds of basic data types:
From all data types , two other kinds of data types can be constructed:
Expressions that are constructed by the rules above are called type expressions. 3.3.1.1.1 A note about the notationWe use the Greek letters , , , …to represent arbitrary data types. For an expression , we write to state that is of type . In the following descriptions of EventB’s mathematical constructs, we will describe the types of all constructs and their components. For example, we will describe the maplet whose type is defined by with and . We do not restrict the types of and . For predicates, we simply describe the data types of their components. The predicate itself does not have a type. For example, consider the components’ types for the equality of two expressions : and . By stating that and are both of type , we express that both expressions must have the same type but do not make any further assumptions about their types. 3.3.1.2 WelldefinednessA predicate which describes the condition under which an expression or predicate in EventB can be safely evaluated is the welldefinedness condition. An example with integer division makes this clear: The expression only makes sense when . Welldefinedness conditions are usually used for welldefinedness proof obligations (3.2.5). In Rodin, the operator defines which welldefined condition a predicate or expression has. When applied to the above example, integer division can be formatted as follows: . In the following sections, we state for each mathematical construct what the welldefinedness conditions are. In many cases, this is just the conjunction of the welldefinedness conditions for the different syntactical parts of a construct.
3.3.1.3 Free identifiersFree identifiers in predicates and expressions are those identifiers which are used but not introduced by quantifiers. More formally, we define the set of free identifiers of an expression or predicate recursively as follows:
3.3.1.4 Structure of the subsections The following reference subsections will have the form the form:
