		Search-engine friendly clone of the ACL2 documentation.

Guard

Guard-miscellany

Miscellaneous remarks about guards

The discussion of guards concludes here with a few miscellaneous remarks. (Presumably you found this documentation by following a link; see guards-for-specification.) For further information related to guards other than what you find under ``guard,'' see any of the following documentation topics: guard-example, set-verify-guards-eagerness, set-guard-checking, verify-guards, and (for a discussion of keyword :split-types) xargs.

Defun can be made to try to verify the guards on a function. This is controlled by the ``defun-mode'' of the defun; see defun-mode. The defun-mode is either as specified with the :mode xarg of the defun or else defaults to the default defun-mode. See default-defun-mode. If the defun-mode of the defun is :logic and either a guard is specified explicitly or :verify-guards t is specified in the xargs, then we attempt to verify the guards of the function. Otherwise we do not. (But see set-verify-guards-eagerness for how to modify this behavior.)

It is sometimes impossible for the system to verify the guards of a recursive function at definition time. For example, the guard conjectures might require the invention and proof of some inductively derived property of the function (as often happens when the value of a recursive call is fed to a guarded subroutine). So sometimes it is necessary to define the function using :verify-guards nil then to state and prove key theorems about the function, and only then have the system attempt guard verification. Post-defun guard verification is achieved via the event verify-guards. See verify-guards.

It should be emphasized that guard verification affects only two things: how fast ACL2 can evaluate the function and whether the function is executed correctly by raw Common Lisp, without guard violations. Since ACL2 does not use the raw Common Lisp definition of a function to evaluate its calls unless that function's guards have been verified, the latter effect is felt only if you run functions in raw Common Lisp rather than via ACL2's command loop.

Guard verification does not otherwise affect the theorem prover or the semantics of a definition. If you are not planning on running your function on ``big'' inputs and you don't care if your function runs correctly in raw Common Lisp (e.g., you have formalized some abstract mathematical property and just happened to use ACL2 as your language), there is no need to suffer through guard verification. Often users start by not doing guard verification and address that problem later. Sometimes you are driven to it, even in mathematical projects, because you find that you want to run your functions particularly fast or in raw Common Lisp.

Finally, we note that ACL2 collects up guards from declare forms in order of appearance. So for example, the declare form

(declare (xargs :guard (foo x))
         (type string x)

will generate the guard (and (foo x) (stringp x)), while the form

(declare (type string x)
         (xargs :guard (foo x))

will generate the guard (and (stringp x) (foo x)). The only exceptions to this rule are that all :stobjs and :dfs declarations will be treated as through they precede all :guard and type declarations.