Friday, April 8, 2011

Writing Contracts

In the best thriller tradition, we left our hero, the Set type, in an awkward position at the end of the last episode.  Because Set has a subtype, HashSet, that doesn't allow nulls as values, the method Set.add(Object x) needed to have a precondition x != null.  But Set has another subtype, ArraySet, which does allow null values.  Therefore, we couldn't put a postcondition on Set.get() that guarantees that the returned value won't be null.  The Set type now precludes null inputs, but may return null values; this seems inconsistent.  Yet both contract decisions seem to be forced by Liskov's Behavioral Subtyping Principle!

In such cases, it is often helpful to look for missing abstractions.  Here, there is an obvious correlation between null inputs and outputs: some sets support null values in both cases, and the others don't in either.  The Set type should clearly distinguish between the two types of sets, by means of a query such as supportsNullValues().  The precondition of Set.add(Object x) will now be:

!supportsNullValues() ==> x != null

where "==>" denotes logical implication.  The postcondition of Set.get() will be:

!supportsNullValues() ==> $ret != null

where "$ret" denotes the returned value.  The contract for Set is now consistent in both cases.  If supportsNullValues() is true, the precondition on add and postcondition on get are inactive; if it's false, both are active.

Furthermore, we can now add a postcondition to HashSet.supportsNullValues(): $ret == false (or, equivalently, !$ret).  As a result, developers using HashSet know, by examining the contract, that add must not be given null values and get will never return null.  Similarly, ArraySet.supportsNullValues() will have a postcondition $ret == true (or simply $ret).  Developers using ArraySet will now know that they can provide add with null inputs, and may receive nulls from get.  Developers who use the Set type without knowing the particular implementation can act in one of two ways.  First, they can be cautious and not insert any null values into the set.  Because Set.get will only return elements previously inserted into the set, it won't return null in this case.  (Note that this is part of the contract that is difficult to specify formally, since it involves conditions on the behavior of the set over time.  However, it is an important part of the contract, and should be documented as such, using natural language.)  The second option is to call supportsNullValues() and act according to the value returned.

In the example, Set.add had another precondition that stated that the client is not allowed to add to the set an element that is already in it.  This is legal but not recommended.  In general, preconditions should contain any conditions under which the action of the method is not well defined.  For example, it makes no sense to ask for an element of an empty set, which is why Set.get has a precondition that the set isn't empty.  But adding to the set an element that is already there is perfectly well defined; the set simply doesn't change.  Instead of requiring clients to check this condition before calling add, the implementation of the add method should simply do the right thing and not add the element if it already exists in the set.  A little effort on the part of the implementer can save much effort for clients.

No comments:

Post a Comment