Verifying Preconditions

Several of the Scheme procedures that we have written or studied in preceding labs presuppose that their arguments will meet specific preconditions -- constraints on the types or values of its arguments. For instance, the spots-leftmost procedure from the third reading on list recursion requires its argument to be a non-empty list of spots.

;;; Procedure:
;;;   spot-leftmost
;;; Parameters:
;;;   spot1, a spot
;;;   spot2, a spot
;;; Purpose:
;;;   Determine the leftmost of spot1 and spot2.
;;; Produces:
;;;   leftmost, a spot.
;;; Preconditions:
;;;   spot1 and spot2 have the correct form for spots.
;;; Postconditions:
;;;   leftmost is equal to either spot1 or spot2.
;;;   leftmost is either in the same column as both spot1 and spot2 or
;;;     has the same column as one, and is to the left of the other.
(define spot-leftmost
  (lambda (spot1 spot2)
    (if (< (spot-col spot1) (spot-col spot2))
        spot1
        spot2)))

;;; Procedure:
;;;   spots-leftmost
;;; Parameters:
;;;   spots, a list of spots
;;; Purpose:
;;;   Find the leftmost spot in spots
;;; Produces:
;;;   leftmost, a spot
;;; Preconditions:
;;;   spots is nonempty.
;;;   spots contains only spots.
;;; Postconditions:
;;;   leftmost is an element of spots
;;;   For each spot, s, in spots
;;;     (spot-col leftmost) <= (spot-col s)
(define spots-leftmost
  (lambda (spots)
    (if (null? (cdr spots))
        (car spots)
        (spot-leftmost (car spots) (spots-leftmost (cdr spots))))))

If some careless programmer invokes spots-leftmost and gives it, as an argument, the empty list, or a list in which one of the elements is not a spot, or perhaps even some Scheme value that is not a list at all, the computation that the definition of spots-leftmost describes cannot be completed.

> (spots-leftmost null)
cdr: expects argument of type <pair>; given ()
> (spots-leftmost (list 1))
1
> (spots-leftmost 2)
cdr: expects argument of type <pair>; given 2

As you can see, none of these error messages are particularly helpful. And, worse yet, in one case spots-leftmost returns a value, but that value is not a spot. Whose responsibility is it to handle these types of errors? As we will see, it is possible to share responsibility between the person who writes a procedure and the person who calls a procedure.

A procedure definition is like a contract between the author of the definition and someone who invokes the procedure. The postconditions of the procedure are what the author guarantees: When the computation directed by the procedure is finished, the postconditions shall be met. Usually the postconditions are constraints on the value of the result returned by the procedure. For instance, the postcondition of the square procedure,

(define square
  (lambda (val)
    (* val val)))

is that the result is the square of the argument val.

The preconditions are the guarantees that the invoker of a procedure makes to the author, the constraints that the arguments shall meet. For instance, it is a precondition of the square procedure that val is a number.

If the invoker of a procedure violates its preconditions, then the contract is broken and the author's guarantee of the postconditions is void. (If val is, say, a list or a spot, then the author can't very well guarantee to return its square. What would that even mean?) To make it less likely that an invoker violates a precondition by mistake, it is usual to document preconditions carefully and to include occasional checks in one's programs, ensuring that the preconditions are met before starting a complicated computation.

Many of Scheme's primitive procedures have such preconditions, which they enforce by aborting the computation and displaying a diagnostic message when the preconditions are not met:

> (/ 1 0)
/: division by zero 
> (log 0)
log: undefined for 0 
> (+ 1 'two)
+: expects type <number> as 2nd argument, given: two; other arguments were: 1
> (length 116)
length: expects argument of type <proper list>; given 116

To enable us to enforce preconditions in the same way, most implementations of Scheme provides a procedure named error, which takes a string as its first argument. Calling the error procedure aborts the entire computation of which the call is a part and causes the string to be displayed as a diagnostic message.

For instance, we could enforce spots-leftmost's precondition that its parameter be a non-empty list of spots by rewriting its definition thus:

(define spots-leftmost
  (lambda (spots)
    (if (or (not (list? spots))
            (null? spots)
            (not (all-spots? spots)))
        (throw "spots-leftmost: requires a non-empty list of spots")
        (if (null? (cdr spots))
            (car spots)
            (spot-leftmost (car spots) (spots-leftmost (cdr spots)))))))

In this definition, we assume the existence of an all-spots? predicate that that takes any list as its argument and determines whether or not all of the elements of that list are spots. We will have to write that procedure soon.

Now the spots-leftmost procedure enforces its preconditions

> (spots-leftmost 139)
Error: spots-leftmost: requires a non-empty list of spots
> (spots-leftmost null)
Error: spots-leftmost: requires a non-empty list of spots
> (spots-leftmost (list 11))
Error: spot-leftmost: requires a non-empty list of spots

Of course, while these error messages are better than the original error messages, they don't tell us the complete story. In particular, they don't tell us what the value of the incorrect parameter is. Fortunately, error can take additional parameters, which it presents verbatim.

(define spots-leftmost
  (lambda (spots)
    (if (or (not (list? spots))
            (null? spots)
            (not (all-spots? spots)))
        (throw "spots-leftmost: requires a non-empty list of spots, received" spots)
        (if (null? (cdr spots))
            (car spots)
            (spot-leftmost (car spots) (spots-leftmost (cdr spots)))))))

> (spots-leftmost 139)
Error: spots-leftmost: requires a non-empty list of spots, received 139
> (spots-leftmost null)
Error: spots-leftmost: requires a non-empty list of spots, received ()
> (spots-leftmost (list 11))
Error: spot-leftmost: requires a non-empty list of spots, received (11)

Including precondition testing in your procedures often makes them markedly easier to analyze and check, so we recommend the practice, especially during program development. There is a trade-off, however: It takes time to test the preconditions, and that time will be consumed on every invocation of the procedure. Since time is often a scarce resource, it makes sense to save time by skipping the test when you can prove that the precondition will be met. This often happens when you, as programmer, control the context in which the procedure is called as well as the body of the procedure itself.

For example, in the preceding definition of spots-leftmost, although it is useful to test the precondition when the procedure is invoked “from outside” by a potentially irresponsible caller, it is a waste of time to repeat the test of the precondition for any of the recursive calls to the procedure. At the point of the recursive call, you already know that spots is a list of spots (because you tested that precondition on the way in) and that its cdr is not empty (because the body of the procedure explicitly tests for that condition and does something other than a recursive call if it is met). Hence, the cdr must also be a non-empty list of strings. It is unnecessary (and therefore wasteful) to confirm this again at the beginning of the recursive call.

One solution to this problem is to replace the definition of spots-leftmost with two separate procedures, a “husk” and a “kernel”. The husk interacts with the outside world, performs the precondition test, and launches the recursion. The kernel is supposed to be invoked only when the precondition can be proven true; its job is to perform the main work of the original procedure, as efficiently as possible:

(define spots-leftmost
  (lambda (spots)
    ; Make sure that spots is a non-empty list of spots
    (if (or (not (list? spots))
            (null? spots)
            (not (all-spots? spots)))
        (throw "spots-leftmost: requires a non-empty list of spots")
        ; Find the leftmost of that list.
        (spots-leftmost-kernel spots))))
(define spots-leftmost-kernel
  (lambda (spots)
    (if (null? (cdr spots))
        (car spots)
        (spot-leftmost (car spots) (spots-leftmost-kernel (cdr spots))))))

The kernel has the same preconditions as the husk procedure, but does not need to enforce them, because we invoke it only in situations where we already know that the preconditions are satisfied.

The one weakness in this idea is that some potentially irresponsible caller might still call the kernel procedure directly, bypassing the husk procedure that he's supposed to invoke. In a subsequent reading and lab, we'll see that there are a few ways to put the kernel back inside the husk without losing the efficiency gained by dividing the labor in this way.

Are we done? Mostly. However, instead of giving the same error message for every type of error, we might customize error messages for the particular kind of error, giving a different error message in each case. The spots-leftmost procedure is perhaps not the best example, because all three kinds of errors are essentially a failure to provide a non-empty list of spots, but we'll use it as a demonstration anyway.

(define spots-leftmost
  (lambda (spots)
    (cond
      ((not (list? spots))
       (throw "spots-leftmost: requires a non-empty list of spots, received a non-list: " spots))
      ((null? spots)
       (throw "spots-leftmost: requires a non-empty list of spots, received the empty list"))
      ((not (all-spots? spots))
       (throw "spots-leftmost: requires a non-empty list of spots, received a list that includes at least one non-spot: " spots))
      (else
       (spots-leftmost-kernel spots)))))
(define spots-leftmost-kernel
  (lambda (spots)
    (if (null? (cdr spots))
        (car spots)
        (spot-leftmost (car spots) (spots-leftmost-kernel (cdr spots))))))

In general, we include precondition checking in our procedures using the following pattern.

(define safe-procedure
  (lambda (parameters)
    (cond
      ((precondition-check-1)
       (error "failed first precondition" parameters))
      ((precondition-check-2)
       (error "failed second precondition" parameters))
      ...
      ((precondition-check-n)
       (error "failed last precondition" parameters))
      (else
       (procedure-kernel parameters)))))