The Object Constraint Language: Getting Your Models Ready for MDA (2nd Edition)

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

Related

Категории