Abstract Preconditions

Returning to the example of the Set type, suppose now that its implementation ArraySet uses a fixed-size array to hold the set elements, and is therefore limited in size (or "bounded").  The maximum size, called the set's capacity, is given when the ArraySet object is constructed and the array is allocated.  The method ArraySet.add, which can add a new element to the set, now needs to have a postcondition size() < capacity(), where size() returns the current size of the set and capacity() returns the maximum size.

Side note: in such cases, it is common to provide the size() method, but less careful designers don't provide capacity().  The assumption is that you ought to know the capacity, since you gave this value when creating the set.  But, of course, you may be using a set created by someone else.  Writing contracts often alerts you to the necessity of adding such informative methods.

According to Liskov's Behavioral Subtyping Principle (see The Correct Use of Inheritance), ArraySet may not strengthen a method precondition.  Therefore, Set must also declare the same precondition (or a stronger one) on the add method.  In general, however, sets don't need to be bounded, and therefore this precondition is inappropriate there.  What is wrong?  The first thing to question is the inheritance hierarchy: is ArraySet really a subtype of Set?  More generally, are bounded sets types of sets?  At first blush, the answer is obviously yes.  But on deeper thought, it seems that we have our abstractions a little bit off.  There are really three concepts involved here: general sets, bounded sets, and unbounded sets.  Both bounded and unbounded sets are kinds of sets; bounded sets have the size() < capacity() precondition, while unbounded sets don't.  Again, it seems like general sets must have this precondition as well, to comply with the Behavioral Subtyping Principle.

Certainly, general sets need to have some precondition that subsumes the boundedness condition, but it doesn't need to have the same form.  The abstract meaning of the precondition is that the set may not be full when adding a new element.  In this form, the precondition is applicable to any set; bounded sets may sometimes be full, while unbounded sets will never be full.  So we need to add  to the Set type, which represents general sets, a method full() that returns a boolean value.  The precondition on Set.add will be !full().  At this level, this precondition is abstract: its precise meaning is unknown.  A client that uses an object of this type therefore needs to check that the set isn't full before adding an element.  The implementation of Set.full may provide some default value, or may be absent, in which case the Set type itself is abstract.

ArraySet.full overrides Set.full to return the value of the expression size() < capacity().  In addition, this method has a postcondition $ret == size() < capacity().  Clients of ArraySet now know the precise condition under which they are permitted to call the add method.  In contrast, unbounded implementations of Set, such as HashSet, override Set.full() to return false, with a postcondition $ret == false (or !$ret).  Clients of HashSet therefore know that the precondition on add is really vacuous: it will never be true, and therefore they are allowed to call add under all circumstances.

If the concepts of bounded and unbounded sets are deemed important enough, it is possible to define them as classes (or interfaces) in their own right, and put the relevant contracts there.  In this way, the missing abstractions are crystallized in the design, with precise contracts that obey the Behavioral Subtyping Principle without forcing a formulation of the precondition that is specific to a subtype.