GUARD-EVALUATION-EXAMPLES-SCRIPT

Major Section:  GUARD

Below is a script that illustrates the combination of defun-modes -- :program mode, :logic mode without guards verified, and :logic mode with guards verified -- with values from set-guard-checking -- t (the default), :all, :none, and nil. (It does not illustrate the value :nowarn, which is the same as t except for inhibiting a warning.) The script also illustrates cases where the guard is not, or is, t.

See guard-evaluation-examples-log for result of running this script. Before presenting the script below, we give some instructions in case you want to run it yourself.

See set-guard-checking for discussion of the interaction between defun-modes and guard-checking that is illustrated by this script. Also see guard-evaluation-table for a succinct table, with associated discussion, that covers in detail the interactions illustrated here.

The script mentions the running of ``Tracing Code''. The code is the following sequence of commands.

(trace$ fact)
:set-guard-checking t
(fact 2)
(fact t)
:set-guard-checking :all
(fact 2)
(fact t)
:set-guard-checking :none
(fact 2)
(fact t)
:set-guard-checking nil
(fact 2)
(fact t)

If you want to run the script yourself, you may find it handy to use the following Emacs keyboard macro for running the tracing code in 2-window mode, with the cursor in the window with the script and ACL2 running in the other window.

(fset 'step-guard-script
   [?C-a ?C-  ?C-e ?M-w ?C-a ?C-n
    ?C-x ?o ?M-> ?C-y return ?C-x ?o])


; Put it on a key (if you have defined the indicated keymap by using
; emacs/emacs-acl2.el):
(define-key ctl-t-keymap "r" 'step-guard-script)

The script follows.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Program mode
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defun fact (x)
         (declare (xargs :guard (integerp x)
                         :mode :program))
         (if (posp x)
             (* x (fact (1- x)))
           1))


; Run the Tracing Code here.  It shows execution in raw Lisp in the t and nil
; cases of :set-guard-checking, but not in the :all or :none cases.  We get a
; guard violation for argument t in the case :set-guard-checking t.


:u


(defun fact (x)
         (declare (xargs :guard t
                         :mode :program))
         (if (posp x)
             (* x (fact (1- x)))
           1))


; Run the Tracing Code here.  It should give the same results as above,
; except that we no longer get a guard violation in the case
; :set-guard-checking t.


:u


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Logic mode, guard other than t
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defun fact (x)
         (declare (xargs :guard (integerp x)
                         :verify-guards nil
                         :mode :logic))
         (if (posp x)
             (* x (fact (1- x)))
           1))


; Run the Tracing Code here.  It should give guard violations for (fact t)
; with guard-checking set to t or :all.  It should never run in raw Lisp,
; because we have not verified guards.  In the t case, we should get a
; warning about avoiding the guard check on recursive calls.


(verify-guards fact)


; Run the Tracing Code here.  The results should be as described just above,
; except that now we go into raw Lisp for (fact 2) with guard-checking other
; than :none.


:u
:u


; The following definition is the same as above, except that guards are
; verified.


(defun fact (x)
         (declare (xargs :guard (integerp x)
                         :mode :logic))
         (if (posp x)
             (* x (fact (1- x)))
           1))


; Run the Tracing Code here.  We should get the same traces as in the
; immediately preceding case, since guards had been verified in both cases.


:u


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Logic mode, guard t
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defun fact (x)
         (declare (xargs :guard t
                         :verify-guards nil
                         :mode :logic))
         (if (posp x)
             (* x (fact (1- x)))
           1))


; Run the Tracing Code here.  We should never go in to raw Lisp, because
; guards have not been verified.  We will see the same traces for (fact 2) as
; with the (integerp x) guard above with :verify-guards nil specified, except
; that there is no warning for :set-guard-checking t about recursive calls.
; And, there are no guard violations for (fact t), of course, since posp
; (necessarily, if we are to verify guards) has a guard of t.


(verify-guards fact)


; Run the Tracing Code here.  Now that guards have been verified, the :none
; trace for (fact 2) differs from the corresponding (guard-verified) trace
; for guard (integerp x) because now the guard is t, so we can (and do) go
; directly into raw Lisp without the need to check the guard.  The (fact 2)
; traces other than for :none are the same as in the corresponding trace for
; guard (integerp x).  And of course (fact t) now computes without guard
; violations, and using raw Lisp even in the :none case,