10.1 Constructs for Postconditions

There are two ways to write constraints for operations: preconditions and postconditions. In postconditions, you can use a number of special constructs. Two special keywords represent, to some extent, the working of time: result and @pre . Another aspect of time is represented by messaging. The following subsections explain all the constructs that can be used in postconditions only.

10.1.1 The @pre Keyword

The @ pre keyword indicates the value of an attribute or association at the start of the execution of the operation. The keyword must be postfixed to the name of the item concerned . In the case of an operation, it must proceed the parentheses, as shown in the following example:

  context  LoyaltyProgram::enroll(c : Customer)  pre  : not (participants->includes(c))  post  : participants = participants@pre->including(c) 

The precondition of this example states that the customer to be enrolled cannot already be a member of the program. The postcondition states that the set of customers after the enroll operation must be the set of customers before the operation with the enrolled customer added to it. We could also add a second postcondition stating that the membership for the new customer has a loyalty account with zero points and no transactions:

  post  : Membership->select(m : Membership  m.participants = c)->           forAll( account->notEmpty() and                   account.points = 0  and                   account.transactions->isEmpty() ) 

10.1.2 The result Keyword

The keyword result indicates the return value from the operation. The type of result is defined by the return type of the operation. In the following example, the type of result is LoyaltyProgram . Note that a navigation from an association class ” in this case, Membership ”always results in a single object (see Section 8.2.1):

  context  Transaction::getProgram() : LoyaltyProgram  post  : result = self.card.Membership.programs 

In this example, the result of the getProgram operation is the loyalty program against which the transaction was made.

10.1.3 The oclIsNew Operation

To determine whether an object is created during the execution of an operation, the oclIsNew operation can be used. It returns true if the object to which it is applied did not exist at precondition time, but does exist at postcondition time. In the following example, the postcondition states that in between pre- and postcondition time, at least one customer has been added to the set of participants. This customer object is created between pre- and postcondition time, its name is equal to the parameter n , and its date of birth is equal to the parameter d :

  context  LoyaltyProgram::enrollAndCreateCustomer( n : String,                                                d: Date ) : Customer  pre  : -- none  post  : result.oclIsNew() and       result.name = n and       result.dateOfBirth = d and       participants->includes( result ) 

Note that a postcondition does not specify the statements in the body of the operation. There are many ways in which the postcondition can become true.

10.1.4 The isSent Operator

To specify that communication has taken place, the isSent operator (denoted as ^) may be used in postconditions. This operator takes a target object and a message as operands. It has a boolean result. The following example on the standard observer pattern states that the message update(12, 14) has been sent to the target object observer between pre- and postcondition time of the hasChanged operation:

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

As with messages in an interaction diagram, update is either a call to an operation defined in the type of observer , or it is the sending of a signal specified 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 or signal definition.

If the actual arguments of the operation or signal are not known, or not restricted in any way, they can be left unspecified. This is indicated by a question mark. Following the question mark is an optional type, which may be necessary to find the correct operation when the same operation exists with different parameter types, as shown in the following example:

  context  Subject::hasChanged()  post  :  observer^update(? : Integer, ? : Integer) 

This example states that the message update has been sent to observer , but that the actual values of the parameters are not known or not relevant.

Note that the postcondition does not state that the message has been received by the target. Depending on the communication mechanism between source and target, some messages may get lost or be delivered later than postcondition time.

10.1.5 The message Operator

During execution of an operation many messages may have been sent that represent calls to the same operation, or send signals according to the same signal definition. To work with collections of messages, OCL defines a special OclMessage type. Any operation call or signal being sent is virtually wrapped in an instance of OclMessage . One can obtain access to all OclMessages that wrap a matching call or signal, through the message operator (denoted as ^^). A call or signal matches when the operation name and the argument types given after the message operator correspond to the formal definition of the operation or signal, as shown in the following example:

 observer^^update(12, 14) 

This expression results in the sequence of messages sent that match update(12, 14) being sent by the contextual instance to the object called observer during the execution of the operation. Each element of the sequence is an instance of OclMessage . Any collection operation can subsequently be applied to this sequence.

Because the message operator results in a sequence of instances of OclMessage , it can also be used to specify collections of messages sent to different targets, as shown in the following example:

  context  Subject::hasChanged()  post  :  let  messages : Sequence(OclMessage) =               observers->collect(o                              o^^update(? : Integer, ? : Integer) )  in  messages->notEmpty() 

The local variable messages is a sequence of OclMessage instances built from the messages that have been sent to one of the observers and match update(? : Integer, ? : Integer) as well. Note that the collect operation flattens the sequence, so that its elements are of type OclMessage , and not of type Sequence(OclMessage) .

The message operator helps explain the isSent operator in another way. Virtually, the isSent operator represents the application of the operation notEmpty on the sequence of OclMessages . Therefore, the following postcondition is semantically equal to the postcondition in Section 10.1.4:

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

In a postcondition with a message operand, one can refer to the parameters of the operation or signal using the formal parameter names from the operation or signal definition. For example, if the operation update has been defined with formal parameters named i and j , we can write the following:

  context  Subject::hasChanged()  post  : let messages : Sequence(OclMessage) =                      observer^^update(? : Integer, ? : Integer)  in  messages->notEmpty() and       messages->exists( m  m.i > 0 and m.j >= m.i ) 

In this example, the values of the parameters i and j are not known, but some restrictions apply. First, i must be greater than zero; and second, the value of parameter j must be larger than or equal to i .