C M S C     2 1 4
C o m p u t e r   S c i e n c e   I I
F a l l   2 0 0 2

Design By Contract

Introduction

Writing software isn't easy. The larger the number of lines that a program contains, the harder it is to write correctly. It's not just a simple matter of coding 10 times as much, but trying to organize it so that the resulting program is likely to work, be easily maintained. This often requires spending time planning and designing, rather than rushing to the computer and writing code. Over the years, programmers have sought ways to make programming more reliable and robust.

Since many computer scientists have strong math backgrounds, it's only natural to think that math might help in creating better software. Math is good at many things. In particular, it's good at being precise and unambiguous. If you understand math, then you can be much more precise in your description, at least, more so than in English or other natural languages.

In essence, that's where "design by contract" comes from. The idea is to describe properties of the classes. These properties are called: preconditions, postconditions, and class invariants

Let's define all three, and demonstrate the basics of design by contract on a stack class.

A method is a short name for a member function, which is the name used in another object oriented language: Smalltalk.

A condition is a logical statement that is either true or false, depending on the current values used. It can be written in English (or some other natural language), but is less precise when written in English.

You can write it in first order predicate logic. This gives you precision, but then you have to make sure that it translates to the code you've written.

So, a reasonable solution is to write it, as best you can, in first order predicate logic (or something close) and implement the condition as a helper function. By implementing it as a function, you have the added benefit that you can test whether the condition is being met or not.

Preconditions

Preconditions are conditions that must be true prior to running a method. Each method will have its own precondition. These conditions can apply to one of two things: data members or parameters. Typically, they apply to parameters. For example, you might have a BankAccount object and a depositMoney() method. The depositMoney() method would, presumably, take an argument indicating the amount of money to be deposited, and that money should be positive. So, a precondition would be money > 0.

If the person calling the method fails to observe the precondition, by passing in a negative argument, the depositMoney() may actually cause the account to become negative. This is actually OK, because that's the purpose of the precondition. It's a warning to the caller of the method to follow the precondition, and if the caller fails to heed the warning, then the object will (potentially) be corrupted.

Sometimes Or, if you have withdrawMoney(), the precondition may affect both the parameter (e.g., money > 0) and the data member (e.g., balance > 0).

You might, however, make a precondition for a method to be "true". This means, you place no restrictions on the input or the data members. Again, consider depositMoney(). You could allow the user to send in money that's negative. If negative, nothing is done (since it wouldn't make sense).

Postconditions

Where preconditions serve to let the caller of a method know when it's safe to call a method, postconditions let the caller of a method know what happens after the method has completed calling. Usually, postconditions are harder to specify.

The purpose of a postcondition is threefold:

In a nutshell, the postconditions tell you what happened after calling the method. The reason it's difficult to specify a postcondition is that it can be difficult to describe the underlying data structure.

For example, if you have a linked list, how do you describe it, so that it reflects the nature of the linked list? The answer is often: you don't. You may have to come up with some math notation that describes the essentials of what is happening.

Here's an example. For an unsorted list, you might add an element to the front of back. So, we can write the following.

list = elt + list'
where + is basically a concatentation operator, and elt is appended at the front of a list.

There's another reason postconditions are harder to specify. You have to describe what changed. That means, you have to describe what used to be, and what is now.

If you're careful, you may have noticed a quote. Call this mark, "prime". list' (read: list prime) will be the list as it was just as the method was being called. list is the list at the end of the call.

Thus, list = elt + list' means that the new list is the old list with elt attached at front. This becomes even more of a problem to describe for trees.

Ultimately, it's easier to write code to test postconditions than to describe it in English/first order logic. However, we'll do both, when we can, since a person who's looking at the classes will want to read it.

Class Invariants

Class invariants can be a little difficult to understand, so a small example can help. If you have a sorted list, then obviously, one class invariant is that the list should be sorted at all times.

The only times it might not be sorted is while a method is running. For example, if you add an element to a list, it may temporarily be unsorted, but then you sort.

Class invariants are useful because they help you avoid writing unnecessary code, and also help you think about what kind of behavior a class ought to have.

Again, consider the sorted list example. Suppose you implement the sorted list using an STL vector as a data member. STL vectors can be sorted by calling the sort algorithm.

You might be tempted to sort the vector data member all the time. For example, suppose you're trying to determine whether some element is in the sorted list. You decide, "I will sort it first, because I sort it elsewhere". But that's totally unnecessary, and in fact, may not compile.

A class invariant for a sorted list is that it's sorted. That means, you can assume, prior to running any method (except constructors) that the list is sorted. If the method doesn't change the list, then it doesn't make sense to sort it, even if you "just want to be safe". In fact, if it doesn't change the list, then the method is probably const, and if it's const, you won't be able to sort without causing compiler errors.

How Class Invariants Relate to Pre and Postconditions

Since class invariants are conditions that apply to the object at all times, they should, technically be part of both the precondition and postcondition. However, for brevity's sake, assume that class invariants are ANDed with the pre- and post-condition.

Constructors and Destructors

Constructors and destructors are two important methods in any class. Until the code for the constructor is run, the class invariant won't hold. That's because the constructor has yet to be run. Also, the class invariant doesn't have to hold once the destructor is complete, because, the object no longer exists.

The class invariant should hold after an object has been constructed, before it has been destructed, and the only time it may not hold is while a method of the class is being run. Prior to and after a method completes, the class invariant should hold.

Determining Conditions Prior to Coding

Usually, you determe preconditions, postconditions, and class invariants while designing a class. It's a good exercise, because it forces you to think about what assumptions you want to make about the class. Few people realize how many assumptions they make, but never state. By writing down the assumptions, it makes the class easier to understand, and hopefully code correctly.

Example: Stack

Let's look at an example of coding a stack. A stack should support the following operations. Let's assume the implementation is a linked list, and there is a size data member.

Let's come up with a list of class invariants. These invariants may change based on the implementation.

Then, we look at the precondition and postconditions of each of the methods.

In Relation to Whom?

Writing conditions also has another pitfall. Preconditions, postconditions, and class invariants can either be user-centric and/or implementer-centric. The conditions are useful to the person using the class, but often the implementer of the class will write conditions that only make sense because of the implementation picked.

From a user's perspective, the conditions should be unaffected by the actual implementation. So, either one needs to present a model to the user and give model variables (for example, let the user think there is a size data member, regardless of whether there is one or not), or to describe things purely in terms of the operations provided, which may be harder to do (algebraic descriptions try to do this).

However, from an implementer's perspective, writing down the conditions based on the implementation help specify the implementation, so that it's more likely to be correct.

Generally, we'll favor the implementer's perspective, since the goal is to write conditions that help us code the class, but it helps to realize when writing conditions (or parts of conditions) whether those conditions are from the user's or implementer's perspective.