In-Depth
From UML to Design by Contract
A trustworthy, reusable component will clearly advertise the set of services it provides in its interface. More information can be gained about how to use a service by examining an operation's signature and accompanying comments. However, is this all the information necessary to fully understand how to use a component? For example, rummaging around in the implementation to discover whether or not a Video Rental Abstract Data Type (ADT) allows customers to rent more than 10 videos defeats the purpose of an interface. Design by Contract (DBC) promotes techniques for strengthening the semantics of classes and their properties right from their inception. We make the case for employing DBC as a standard component specification and documentation technique throughout the design, development, testing, and deployment phases of a component. We show how to combine the Unified Modeling Language's (UML) Object Constraint Language (OCL) with the design techniques first developed by Bertrand Meyer for Eiffel, stressing the benefits of retaining clear component specifications throughout the design, implementation, and deployment phases.
DBC is a software engineering approach that focuses on reliability right from the start of the development process. Software systems are viewed as collections of communicating components whose interactions are based on precisely defined contracts. Contracts specify the rights and obligations of suppliers and users of components through a simple assertion language applied to operations on the component interface. Application of DBC techniques from the very beginning of a component life cycle has a profound effect on software quality. An introduction to DBC can be found at http://www.eiffel.com/doc/manuals/technology/contract/page.html.1
UML2 is a widely accepted object-oriented analysis and design notation. UML includes the OCL3 that is used to specify all kinds of constraints over components in the constituent models.
In this article, we introduce DBC and then describe how a small example is depicted in UML and specified in OCL (see "A Video Rental Example," "UML and OCL," and "Video Specification"). Next, the OCL specification is translated into run-time checkable Eiffel assertions (see "Executable Specifications"). In the final section, conclusions are drawn about the benefits of applying the discipline of DBC across the whole software life cycle (see "Lesson Learned—Specify Early!).
DESIGN BY CONTRACT
Contracts are generally understood to be formal agreements that bind two or more parties. Good contracts are those that exactly specify the rights and obligations of each participant.
DBC originated with Bertrand Meyer's development of Eiffel.4 It employs the contracting metaphor to separate and clarify the responsibilities of software suppliers and clients in order to improve the reliability of software systems. The spirit of DBC is triggered by the question, "Which design style is preferable—tolerant or demanding?" A tolerant style means the service designer has to take full responsibility to guarantee the correctness of the service, in all conceivable circumstances, while a demanding style expects the clients of a service to abide by certain prerequisites. It is clear that the demanding style is the only approach suitable for building robust, reusable software components. No designer can ever anticipate the future uses of a component. However, they can specify under what circumstances the component will be guaranteed to work.
DBC is central to the Eiffel method. The Eiffel method and notation covers analysis, design, specification, and implementation. Contracts are captured by assertions. Assertions enable designers to view the relationship between a class and its clients by explicitly stating each party's rights and obligations. Assertions are Boolean expressions employing simple, first-order predicate logic describing the semantic properties of classes; in DBC, assertions serve as the specification of software components—i.e., what a component does, rather than how it does it.4 Assertions are regarded in the Eiffel method as an essential element of the component interface, providing valuable documentation and a basis for test-case generation. Although this is beyond the scope of this article, it is worth noting that assertions combined with inheritance provide a powerful mechanism for applying disciplined semantics to designing class hierarchies. Abstract classes properly instrumented with assertions become reusable specifications, guiding the development of future generations of inheriting implementations.
A VIDEO RENTAL EXAMPLE
We will use the simple example of a Video Account used by a Customer to rent videos. The Video Account has a collection of rented videos and has access to the Video Store's stock of available videos. A limit is placed on the number of videos that can be released to a customer at any one time. Our small example will focus on two operations: release, which registers an available video in the customer's collection of rented videos once the payment has been processed; and renew, which renews a video rental unless it is reserved for another customer. The UML class diagram is shown in Figure 1.
Figure 1. Class diagram of a video rental application.
UML and OCL
The Object Constraint Language (OCL) is a formal language that expresses side effect-free constraints3,6,7 in UML models. A side effect-free operation is defined as one that will not change the state of the system when executed, such as attribute accesses or a true function call. In a UML model, a side effect-free operation is defined as one whose isQuery attribute equals True.
OCL is a typed language. The OCL type hierarchy is depicted in Figure 2. Notice that in addition to the basic types Integer, Real, Boolean, and String, OCL offers Enumeration and Collection with subtypes Set, Bag, and Sequence.
Figure 2: OCL type hierarchy.
In addition to the standard operations available on the basic types, OCL provides ways to deal with Enumerations and Collections. Operations available on collections and its subtypes include size; includes(object:OclAny): Boolean; count(object:OclAny): Integer; includesAll(c: Collection):Boolean; isEmpty:Boolean; notEmpty:Boolean; sum:T; exists (expr): Boolean; forAll (expr): Boolean; and iterate(expr).
VIDEO SPECIFICATION IN OCL
We now specify the semantics of release and renew as precisely as possible, using OCL pre-condition and post-condition constraints on the operations, and also invariants on the class VideoAccount as a whole. We take the interface view, concerning ourselves with what the operations do, not how they are implemented.
Release
Context: VideoAccount::release (aVideo: Video) (1)
Pre:
store.stock -> count (aVideo) = 1 (2)
aVideo.available (3)
self.hired-> size < self.videohirelimit="" (4)="" self.hired="" -=""> count(aVideo) = 0 (5)
Post:
store.stock -> count (aVideo) = 1 (6)
aVideo.hired (7)
store.stock -> size = store.stock@pre (8)
self.hired -> count ( aVideo) = 1 (9)
self.hired -> size = self.hired@pre + 1 (10)
(1) The target Context is the VideoAccount release operation.
Before a video is released, the following conditions must hold:
(2) There must exist only one video in the store's stock of videos that is the same as this one.
Note that we are traversing associations from the VideoAccount to the Store and from the Store to the stock of Videos.
Also be aware this constraint is stronger than: store.stock -> exists(v | v = aVideo), which states that there must be at least one of this video in stock.
(3) The video must be available.
(4) The number of videos already hired must be less than the limit permitted for this VideoAccount.
(5) The video being hired must not already be rented on this VideoAccount.
After a video has been released, the following will hold:
(6) There exists (at most) one video in the store's stock of videos that is the same as the released video.
(7) The video is hired.
(8) The size of the Store's stock of videos remains the same.
Note that we are making explicit what happens to the stock of videos when one is hired. The stock collection does not change.
(9) There is exactly one video in this VideoAccount's collection of hired videos that is the same as this one. This is a stronger constraint than one which merely states that the released video exists in the collection. Here, we are traversing the hired association to a collection of videos.
(10) The size of the pool of hired videos for this account will have increased by one.
Renew
Context: VideoAccount::renew (aVideo: video) (1)
Pre:
not aVideo.available (2)
self.hired -> count (aVideo) = 1 (3)
not aVideo.reserved (4)
Post:
not aVideo.available (5)
self.hired -> count ( aVideo) = 1 (6)
self.hired -> size = self.hired@pre (7)
(1) The target Context is the VideoAccount renew operation.
Before a video is renewed the following conditions must hold:
(2) As the video should already be in this Account's hired collection, it should not be available.
(3) Here, we are checking that the collection of Videos hired out to this account contains the video in question.
(4) The Video is not reserved by someone else.
It is often useful to state explicitly that particular values do not change. Here, we are confirming that:
(5) The Video will remain in the "not available" state.
(6) It is still the only video with this reference in the account's collection of hired videos.
(7) The collection of hired videos is the same size as before the renew operation.
A complete specification of release and renew would include post-conditions ensuring that the state of properties not involved in an operation remained the same after the operation. Pragmatically, however, it is usually sufficient to specify the post-state of properties involved in an operation.
Context: VideoAccount (1)
Invariant
self.hired.count >= 0 (2)
self.hired.count <= videohirelimit="" (3)="" self.hired="" -=""> forAll (v: Video | not v.available) (4)
self.hired -> forAll (v: Video |
store.stock -> exists ( w:Video | w = v)) (5)
(1) The Invariant context is VideoAccount.
(2) Property videos_hired must never be negative.
(3) The number of videos hired must always be less than the video hire limit for this account.
(4) Each video in this account's hired collection must be not available.
(5) Each video in this account's hired collection must exist in the store's video stock.
Note that in (3), hired videos have their available property set to False. However, looking back at the renew operation, a hired video can also have its reserved property set. This should be reflected in the invariant of the Video class:
Context: Video
Invariant
self.available implies
(self.reserved or not self.reserved)
EXECUTABLE SPECIFICATIONS
You will now appreciate the amount of work that has gone into precisely defining the relationships between the key properties of the release and renew operations. Along the way, the nature of the store's stock collection has been clarified—it holds a set of all videos in stock and the set does not change when a video is rented out; instead the available status of the video is changed from true to false.
It is important to note that we have made no decisions about how these ADTs and their relationships will be implemented—we are working purely in terms of the properties of these entities. Exactly what kind of data structures we will employ can be left to the design/implementation phase.
The question now is, "How do we preserve and propagate all this careful analysis and specification into the design and implementation phases?"
OCL specifications can be translated directly into Eiffel assertions. The assertions are compiled and checked at runtime.5 In Listing 1, we show the interface to class VIDEO_ACCOUNT for the two operations.
Notice that the requirement of having only one instance of any video in stock has prompted a design decision to use a SET ADT, which will take care of this constraint automatically. Also, taking advantage of standard set operations, the hired_videos_in_pool invariant can be expressed by a function call to the SET is_subset operation.
LESSON LEARNED—SPECIFY EARLY!
We have seen how the OCL constraints have been easily translated into Eiffel assertions. Eiffel assertions are executable; if assertion checking is enabled, a contract broken by the client (pre-condition) or by the supplier (post-condition or invariant) will cause an exception to be raised at runtime. For example, if a client attempts to renew a video without first checking that it is in the VIDEO_ACCOUNT's video_hired set, then an exception will be raised in the client (calling routine). So the effort put into specification during analysis pays real dividends during design and implementation.
Obvious advantages of adopting this disciplined approach to analysis and design are:
- Many ambiguities are sorted out and documented in the classes during analysis. For example, it is clear that releasing a video does not remove it from the Store's stock.
- Assertions plus comments provide excellent documentation for robust components.
- Designers of classes can specify exactly the conditions under which it is safe to invoke an operation and need not check in the body of the class that the constraints hold, as the runtime will check them before the operation is invoked.
- Clients have a clear understanding of their obligations before invoking an operation, and the post-operation state of the target object.
- Assertions form an excellent basis for debugging, testing, and quality assurance.
Although Eiffel was the first to systematically employ assertions, efforts are being made to provide similar facilities in other languages, for example Reto Kramer's I-Contracts. Adopting DBC for all stages of the software development process is an essential step on the path to a high-quality, robust, component industry.
REFERENCES
- See http://www.eiffel.com/doc/manuals/technology/contract/page.html.
- Rumbaugh, J., G. Booch, and I. Jacobson. The Unified Modeling Language User Guide, Addison–Wesley, Reading, MA, 1999.
- IBM, et al. Object Constraint Language Specification Technical Report, Rational Software, Sept. 1997. see http://www.ibm.com/software/ad/standards.cocl.html.
- Meyer, B. Object-Oriented Software Construction, Prentice Hall, Saddle River, NJ, 1997.
- Meyer, B. Eiffel-The Language, Prentice Hall, Saddle River, NJ, 1992.
- Warmer, J. and A. Kleppe. "OCL: The Constraint Language for the UML," JOOP, 12(2): p. 10–13, May 1999.
- Warmer, J. and A. Kleppe. The Object Constraint Language: Precise Modeling with UML, Addison–Wesley, Reading, MA, 1999.
FOOTNOTE
* The work reported in this paper has been funded in part by the Cooperative Research Centre Program through the Department of Industry, Science, and Tourism of the Commonwealth Government of Australia.