3.8 Completing Use Cases

In UML use cases, pre- and postconditions may be used. These may also be written using OCL. Because use cases are an informal way of stating requirements, and OCL is a formal language, some adjustments need to be made when the pre- and postconditions of use cases are to be defined using OCL expressions.

3.8.1 Preconditions and Postconditions

Although use cases can be considered to be operations defined on the complete system, we cannot identify the complete system as a type, because it is not a class, an interface, a datatype, or a component. Therefore, the pre- and postconditions of a use case have no contextual type or contextual instance. As a consequence, the keyword self cannot be used.

In addition, it is not clear which model elements may be referenced in the expression. Normally, all elements held by the contextual type may be used. Here, there is no contextual type. Therefore, the model elements that may be used must be explicitly stated. This can be done by formalizing the types mentioned in the use case, e.g., Customer and Order , in an accompanying class diagram; and adding to the use case template a section called (for instance) concerns , with a list of variable declarations, e.g., newCustomer : Customer, newOrder : Order .

Yet another consequence is that we cannot write a context definition, as there is no contextual type to be referenced. This is not a problem. The OCL expressions may be directly included in the use case at the position indicated by the use case template.

The following example illustrates a use case for the R&L system. It describes how customer cards are upgraded and how invalid cards are removed from the system. Because not all information about the attributes and operations in the system could be included in Figure 2-1, the CustomerCard class ”with all attributes used in the following use case ”is reprinted in Figure 3-12.

[View full width]

 
 [View full width] 
  Use case title  : Check customer cards for loyalty program  Summary  : On a regular basis the cards of all participants in a loyalty program are  checked. Those that have been invalidated are removed, and those that have been used often  are upgraded to the next service level.  Primary actor  : user  Uses  : - the class diagrams for the Royal & Loyal system as shown in         Figure 2-1 and Figure 3-12       -  lp  of type  LoyaltyProgram  , which is the loyalty program for         which the cards are checked       -  upgradeLimit  of type  Integer  , which indicates how many         points must have been earned before a card is upgraded       -  fromDate  of type  Date  , which gives the date from which to         calculate points to see if an upgrade is required  Precondition  : none  Main success scenario  : 1. The actor starts the use case and gives the  upgradeLimit  . This value must be larger  than 0. 2. The system selects all cards that have been invalidated or have a goodThru date that  lies before today, and shows them to the user. 3. The actor checks the invalid cards, and marks any card that must not be removed by  giving a new  goodThru  date. 4. The system removes all invalid cards, except the ones that have received a new   goodThru  date. 5. The actor gives the  fromDate  . This date must be before today. 6. The system calculates for all remaining cards the number of points earned in the period  starting with  fromDate  until today, and shows the cards for which this number is higher  than the  upgradeLimit.  7. The actor checks the cards to be upgraded, and marks any card that must not be upgraded. 8. The system upgrades the selected cards.  Extensions  :    -- indicate what is to be done when the  upgradeLimit  and  fromDate  -- do not uphold their conditions  Postcondition  : -- all  goodThru  dates are in the future lp.participants.cards.goodThru->forAll( d  d.isAfter( Date::now ) and -- all cards that have earned enough points and have not been marked -- otherwise are upgraded  let  upgradedCards : Set( CustomerCard ) =            lp.participants.cards->select( c                   c.getTotalPoints( fromDate ) >= upgradeLimit                  and c.markedNoUpgrade = false )  in  upgradedCards->forAll( c             lp.levels->indexOf( c.Membership.currentLevel ) =            lp.levels->indexOf( c.Membership.currentLevel@pre ) + 1 

Figure 3-12. Class CustomerCard , with all its attributes and operations