1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87

; This file illustrates Version 1.8 as of Nov 2, 1994. We start in
; the default :logic mode with guard checking on, i.e. ,the prompt
; is ACL2 !>.
(defun sumlist (x)
(declare (xargs :guard (integerlistp x) :verifyguards nil))
(cond ((endp x) 0)
(t (+ (car x) (sumlist (cdr x))))))
; Note that we disable guard verification above. We can now evaluate
; calls of this function.
(sumlist '(1 2 3 4)) ; this call succeeds.
(sumlist '(1 2 abc 3 4 . xyz)) ; this one fails because of a guard violation.
; It is surprising, perhaps, to note that the violation is on the guard of
; endp, not the guard of sumlist. Because we have not yet verified the guards
; of sumlist we only have a logical definition. But because endp has had its
; guards verified, we can run either the Common Lisp or the logical version of
; it and with guard checking on we are running the Common Lisp one.
; So we switch to no guard checking...
:setguardchecking nil
(sumlist '(1 2 abc 3 4 . xyz)) ; Now this call succeeds.
; We prove an important theorem about sumlist. Note that we do not have
; to restrict it with any hypotheses.
(defthm sumlistappend
(equal (sumlist (append a b))
(+ (sumlist a) (sumlist b))))
; Ok, we now move on to the task of showing these results hold in Common Lisp.
(verifyguards sumlist) ; this is just like it was in Version 1.7
:comp sumlist ; this compiles both the Common Lisp version of
; sumlist and the logical (Nqthmlike ``*1*'')
; version
; Now we exit the loop and install a trace on the Common Lisp program
; sumlist, and then reenter the loop.
:q
(trace sumlist)
(lp)
; Recall that guard checking is still off. The following call violates the
; guards of sumlist, but since guard checking is off, we get the logical
; answer. It is done without running the Common Lisp version of sumlist.
; That is, no trace output is evident.
(sumlist '(1 2 abc 3 4)) ; succeeds (but runs the compiled *1* function)
; But the following call prints a lot of trace output. Because the
; guard is satisfied and we can run sumlist directly in Common Lisp.
(sumlist '(1 2 3 4)) ; succeeds (running compiled sumlist)
; Next we turn our attention to verifying that sumlistappend
; holds in Common Lisp. If we try
(verifyguards sumlistappend)
; it fails. Among other things, the guard for append is violated since we know
; nothing about a. We need a version of the theorem with some hypotheses
; restricting the variables. We state the theorem with IF so that the
; hypotheses govern the conclusion. (At the moment in Version 1.8 IMPLIES is a
; function, not a macro, and hence in (IMPLIES p q), q is not governed by p.)
(defthm commonlispversionofsumlistappend
(if (and (integerlistp a)
(integerlistp b))
(= (sumlist (append a b))
(+ (sumlist a) (sumlist b)))
t)
:ruleclasses nil)
; The theorem above is trivially proved, because its conclusion is true
; without the hypotheses. But we can now verify that its guards hold.
(verifyguards commonlispversionofsumlistappend)
; So that expression will all evaluate to nonnil without error in
; Common Lisp (except for resource errors).
