6.4 Operations

This section explains the different functions which expressions may have for operations in the model. The model elements that may be used in an expression whose context is an operation are all attributes, query operations, states, and associations of the contextual type, plus the parameters of the operation.

6.4.1 Preconditions and Postconditions

The first two ways in which expressions may be used for operations are pre- and postconditions: two forms of constraints. A precondition is a boolean expression that must be true at the moment when the operation starts its execution. A postcondition is a boolean expression that must be true at the moment when the operation ends its execution. A precondition specifies that the expression must evaluate to true; otherwise, the operation will not be executed. The meaning of a postcondition specifies that the expression must evaluate to true; otherwise , the operation has not executed correctly.

The context is denoted by the keyword context followed by the name of the type to which the operation belongs; a double colon ; the complete operation signature ”that is, the name of the operation; all parameters and their types; and the return type of the operation. Usually, the complete operation signature is defined in the UML class diagram.

Following this context definition are lines ”labeled with the keywords pre : and post : ”that contain the actual pre- and postconditions, respectively. The general syntax looks like the following:

  context  Type1::operation(arg : Type2) : ReturnType  pre  : -- some expression using the param arg and features of the       -- contextual type  post  : -- some expression using the param arg, features of the       -- contextual type, the @pre keyword, and messaging       -- expressions 

The contextual instance is always an instance of the type for which the operation has been defined.

Note that in contrast to invariants, which must always be true, pre- and postconditions need be true only at a certain point in time: before and after execution of an operation, respectively.

6.4.2 Body of Query Operations

Query operations can be fully defined by specifying the result of the operation in a single expression. By definition, query operations have no side effects. Execution of a query operation results in a value or set of values, nothing more. The context is indicated in the same manner as for pre- and postconditions. Instead of the keywords pre or post , the keyword body is used, followed by the body expression:

  context  CustomerCard::getTransactions(from : Date, until: Date )                                 : Set(Transaction)  body  : transactions->select( date.isAfter( from ) and                             date.isBefore( until ) )