Guard
Restricting the domain of a function
NOTE: Novices are often best served by avoiding guards.
The ACL2 system provides a mechanism for restricting a function to a
particular domain. Such restrictions are called ``guards.'' A definition's
guard has no effect on the logical axiom added when that definition is
accepted by ACL2. Moreover, the guard has NO EFFECT on the proof that a
recursive definition is admissible — informally, that it terminates).
(See mbt for a discussion of one way to use the guard explicitly to
assist with that proof while avoiding execution overhead.)
Guards can be useful as a specification device or for increasing execution
efficiency. To make such a restriction, use the :guard keyword (see
xargs) or, especially if you want the host Lisp compiler to use this
information, use type declarations (see declare; also see xargs for a discussion of the :split-types keyword). The general issue
of guards and guard verification is discussed in the topics listed below.
To begin further discussion of guards, see guard-introduction. That
section directs the reader to further sections for more details. To see just
a summary of some commands related to guards, see guard-quick-reference. For a discussion of the use of proof to verify the
absence of guard violations, see verify-guards.
Subtopics
- Verify-guards
- Verify the guards of a function
- Mbe
- Attach code for execution
- Set-guard-checking
- Control checking guards during execution of top-level forms
- Ec-call
- Execute a call in the ACL2 logic instead of raw Lisp
- Print-gv
- Print a form whose evaluation caused a guard violation
- The
- Special form for execution efficiency or run-time type checks
- Guards-and-evaluation
- The relationship between guards and evaluation
- Guard-debug
- Generate markers to indicate sources of guard proof obligations
- Set-check-invariant-risk
- Affect certain program-mode updates to stobjs or arrays
- Guard-evaluation-table
- A table that shows combinations of defun-modes and guard-checking
- Guard-evaluation-examples-log
- Log showing combinations of defun-modes and guard-checking
- Guard-example
- A brief transcript illustrating guards in ACL2
- Defthmg
- Variant of defthm supporting guard verification
- Invariant-risk
- Potential slowdown for program-mode updates to stobjs
or arrays
- With-guard-checking
- Suppress or enable guard-checking for a form
- Guard-miscellany
- Miscellaneous remarks about guards
- Guard-holders
- Remove trivial calls from a term
- Guard-formula-utilities
- Utilities that show guard proof obligations
- Set-verify-guards-eagerness
- The eagerness with which guard verification is tried.
- Guard-quick-reference
- Brief summary of guard checking and guard verification
- Set-register-invariant-risk
- Avoid invariant-risk checking for specified functions
- Guards-for-specification
- Guards as a specification device
- Guard-evaluation-examples-script
- A script to show combinations of defun-modes and guard-checking
- Guard-introduction
- Introduction to guards in ACL2
- Program-only
- Functions that cannot be in logic mode
- Non-exec
- Mark code as non-executable
- Set-guard-msg
- Specify what is printed when a guard is violated
- Safe-mode
- A mode that avoids guard violations on primitives
- Set-print-gv-defaults
- Set default keyword values for print-gv
- Guard-theorem-example
- How to use a previously-proved guard theorem
- With-guard-checking-event
- Suppress or enable guard-checking for an event form
- With-guard-checking-error-triple
- Suppress or enable guard-checking for a form
- Guard-checking-inhibited
- Avoiding certain warnings when evaluating ACL2 expressions
- Extra-info
- Sources of measure, guard, or constraint proof obligations
