3.4 Create an Operator Definition

Event-B mathematical language has many useful operators. Examples include cardinality operator $card$ , the finiteness predicate operator $finite$ and the function application $.(.)$ . Other useful operators can be defined using the Theory plug-in. The following figure shows a definition of a sequence operator.

$\includegraphics{SeqOperator.png}$

Figure 5: Sequence Operator Definition

Note the numbering in the above picture. The following explains each part of the definition:

Syntax Symbol: this specifies the syntax token that will be reserved for the new operator (sequence in our example). It should not clash with any previously defined symbol in the mathematical language available to the theory.
Syntactic Class: this specifies whether the new operator is an expression operator or a predicate operator. For example, the cardinality operator $card$ is an expression operator of integer type, and the finiteness operator $finite$ is a predicate operator. In our case, the sequence operator is an expression operator. The button can be toggled off if a predicate operator is required instead.
Notation: this specifies whether the symbols is a prefix or an infix operator. In the existing mathematical language, $+$ is an infix operator whereas $partition$ is a prefix predicate operator. In our example, the sequence operator is specified as prefix.
Associativity: this specifies whether the operator is associative. Note that this has semantic implications, and as such a proof obligation is generated to check the associativity property.
Commutativity: this specifies whether the operator is commutative. Note that this has semantic implications, and as such a proof obligation is generated to check the commutativity property.
Operator Arguments: an operator may have a number of arguments (all of which may be expressions).
Argument Identifier: this specifies the name of the argument of the operator. It has to be a legal Event-B identifier (similar to carrier sets, constant, variables etc.).
Argument Type: this specifies the type of the argument. In our case, the sequence operator takes a set of type $A$ . Since $A$ is a type parameter, the sequence is polymorphic.
Direct Definition: this provides the direct definition of the operator. In our case (see the red-boxed field), it asserts that sequences are total functions from a contiguous integer range starting at 1 to the set $a$ the argument of the operator $seq$ .

The proof obligations associated with an operator definition are the following:

./Op-WD operator well-definedness strength if a well-definedness condition is explicitly specified.
./Op-COMMUT the commutativity proof obligation, generated if the operator is tagged as commutative.
./Op-ASSOC the associativity proof obligation, generated if the operator is tagged as associative.