2.5 Adding Preconditions and Postconditions

Preconditions and postconditions are constraints that specify the applicability and effect of an operation without stating an algorithm or implementation. Adding them to the model results in a more complete specification of the system.

2.5.1 Simple Preconditions and Postconditions

The context of preconditions and postconditions is specified by the name of the class that holds the operation and the operation signature (its name , parmeters, and return type). In the R&L example, the class LoyaltyAccount has an operation isEmpty . ^[1] When the number of points on the account is zero, the operation returns the value true . The postcondition states this more precisely; it tells us that the operation returns the outcome of the boolean expression points = 0 . The return value of the operation is indicated by the keyword result:

^[1] Note that this operation is different from the isEmpty operation defined on collections.

  context  LoyaltyAccount::isEmpty(): Boolean  pre  : -- none  post  : result = (points = 0) 

There is no precondition for this operation, so we include a comment, none, where the precondition should be placed, indicated by the double dash. Including a precondition, even if it is an empty one, is optional. Rather, it is a matter of style. We prefer to state even empty preconditions, because we think this is clearer. If, for instance, this example were part of a list of operations with their pre- and postconditions and the precondition for the isEmpty operation was the only one missing, the reader might misinterpret its meaning and think that the precondition was mistakenly forgotten.

2.5.2 Previous Values in Postconditions

In a postcondition, the expression can refer to values at two moments in time:

• The value at the start of the operation

• The value upon completion of the operation

The normal value of an attribute, association end, or query operation in a postcondition is the value upon completion of the operation. To refer to the value of a property at the start of the operation, postfix the property name with the keyword @pre , as shown in the following example:

  context  Customer::birthdayHappens()  post  : age = age@pre + 1 

The term age refers to the value of the attribute after the execution of the operation. The term age@pre refers to the value of the attribute age before the execution of the operation.

When you need the pre-value of a query operation, the @pre is postfixed to the operation name, before the parameters, as shown in the next example:

  context  Service::upgradePointsEarned(amount: Integer)  post  : calcPoints() = calcPoints@pre() + amount 

The @pre postfix is allowed only in OCL expressions that are part of a postcondition.

2.5.3 Messaging in Postconditions

Another thing allowed only in postconditions is specifying that communication has taken place. This can be done using the hasSent ('^') operator. For example, you can specify the standard observer pattern:

  context  Subject::hasChanged()  post  : observer^update(12, 14) 

The observer^update(12, 14) results in true if an update message with arguments 12 and 14 was sent to the observer object during the execution of the operation hasChanged(). update() is either an operation defined in the class of observer , or a signal specified elsewhere in the UML model. The argument(s) of the message expression ( 12 and 14 in this example) must conform to the parameters of the operation/signal definition.