CSC/ECE 517 Fall 2007/wiki3 2 at

Programming by contract

Programming by Contract is a way of specifying the behavior of a function, and the name arises from its formal similarity to a legal contract. The preconditions define the conditions whose truth the caller guarantees to ensure before calling the function, and the postconditions define the conditions whose truth the function guarantees to establish by virtue of its execution. One of the purposes in this is to avoid redundant validity checks at each level in a stack of called functions.

Consider the following example for counting the number of vowles:

int is_vowelpair (const char *p)
{
    return is_vowel(*p) && is_vowel (*(p+1));
}

int count_vowelpairs (char *s)
{ 
    int sum = 0;
    
    for (; *s != '\0'; s++)
        if (is_vowelpair(s))
            sum++;
    return sum;
} 

The functions count_vowels and count_vowelpairs both receive as input argument a pointer to a C string. Neither function applies any validity check to the pointer, so there is an implicit precondition that the caller supply a valid pointer. To follow the rules of programming by contract we should make this an explicit precondition, albeit one that is so common and obvious that it hardly seems to need stating.

There are four possibilities for the pointer passed in as argument:

It contains a valid address that is indeed the address of a valid C string (including the null string). It contains a valid address but the memory at that address does not comprise a valid C string. It contains a bit pattern that is not a valid address (e.g., it is outside the addressing range, or the memory is not readable). It contains the null pointer. Our contract imposes the precondition that the pointer must be valid as specified in the first case above. There is no reasonable way to detect the second case, and for the third case it is usual to delegate detection (and handling) to the exception mechanism of the operating system11.

The fourth case is the interesting one. Null is a valid value for a pointer, but it is (by definition) an invalid address that will generally cause an addressing exception if dereferenced. It is, however, trivial for the function to detect that a null pointer argument has been passed. Therefore, we can propose a general rule that makes life easier for callers of a function: If a pointer to a null object is a valid argument, a null pointer should also be a valid argument with the same meaning. In the specific examples we are studying here, we should change the contract by weakening the precondition to allow the first and fourth cases, and implement the function to immediately return the value 0 if a null pointer is passed as the argument. The purpose of this rule is to relieve callers of the need to make the test for a null pointer; for a language like C the gain is not obvious, but for functional style languages like Lisp the gain is significant.

Programming by contract places responsibility squarely on the shoulders of the caller for ensuring that specified preconditions for a function are met, and relieves the function of any responsibility for verifying that preconditions are met. As intended, this has the desirable effect of eliminating redundant validity checking. In real life, however, it also has an undesirable side effect: If the caller makes a mistake and does not in fact meet the preconditions, the function is likely to fail, and the cause of the failure may be difficult to track down. A pointer that is null or contains an invalid address is usually easy to diagnose; since an exception will be caused immediately an attempt is made to deference it, but other errors may cause failures far removed from the root cause. Therefore it is good practice for a function to perform reasonable validity checks for its preconditions, and in the C language the preferred technique is to use assertions. "Reasonable" is, of course, a slippery word; it would be reasonable, for example, to test whether an integer lies within a specified range, but not to test whether a binary search tree was indeed valid.