GUARDS-FOR-SPECIFICATION

Major Section:  GUARD

A use of guard verification that has nothing to do with efficiency is as a way to gain confidence in specifications. This use has the feel of ``types'' in many traditional programming languages, though guards allow much greater expressiveness than most systems of types (and unfortunately, as a result they are not syntactically checkable).

For more discussion of guards in general, see guard.

Suppose you have written a collection of function definitions that are intended to specify the behavior of some system. Perhaps certain functions are only intended to be called on certain sorts of inputs, so you attach guards to those functions in order to ``enforce'' that requirement. And then, you verify the guards for all those functions.

Then what have you gained, other than somewhat increased efficiency of execution (as explained above), which quite possibly isn't your main concern? You have gained the confidence that when evaluating any call of a (specification) function whose arguments satisfy that function's guard, all subsequent function calls during the course of evaluation will have this same property, that the arguments satisfy the guard of the calling function. In logical terms, we can say that the equality of the original call with the returned value is provable from weakened versions of the definitions, where each definitional axiom is replaced by an implication whose antecedent is the requirement that the arguments satisfy the guard and whose consequent is the original axiom. For example,

(defun foo (x)
  (declare (xargs :guard (consp x)))
  (cons 1 (cdr x)))

(equal (foo x)
       (cons 1 (cdr x)))

(implies (consp x)
         (equal (foo x)
                (cons 1 (cdr x))))