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
|
<html>
<head><title>GUARD-INTRODUCTION.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>GUARD-INTRODUCTION</h3>introduction to <a href="GUARD.html">guard</a>s in ACL2
<pre>Major Section: <a href="GUARD.html">GUARD</a>
</pre><p>
Most users can probably profit by avoiding dealing with guards most
of the time. If they seem to get in the way, they can be ``turned
off'' using the command <code>:</code><code><a href="SET-GUARD-CHECKING.html">set-guard-checking</a></code> <code>nil</code>; for more
about this, see <a href="SET-GUARD-CHECKING.html">set-guard-checking</a>. For more about guards in
general, see <a href="GUARD.html">guard</a>.
<p>
The guard on a function symbol is a formula about the formals of the
function. To see the guard on a function, use the keyword command
<code>:</code><code><a href="ARGS.html">args</a></code>. See <a href="ARGS.html">args</a>. To specify the guard on a function at
<code>defun-time</code>, use the <code>:</code><code><a href="GUARD.html">guard</a></code> <code>xarg</code>. See <a href="XARGS.html">xargs</a>.<p>
Guards can be seen as having either of two roles: (a) they are a
specification device allowing you to characterize the kinds of
inputs a function ``should'' have, or (b) they are an efficiency
device allowing logically defined functions to be executed directly
in Common Lisp. Briefly: If the guards of a function definition
are ``verified'' (see <a href="VERIFY-GUARDS.html">verify-guards</a>), then the evaluation of a
call of that function on arguments satisfying its guard will have
the following property:
<blockquote>
All subsequent function calls during that evaluation will be on
arguments satisfying the guard of the called function.
</blockquote>
The consequence of this fact for (a) is that your specification
function is well-formed, in the sense that the values returned by
this function on appropriate arguments only depend on the
restrictions of the called functions to their intended domains. The
consequence of this fact for (b) is that in the ACL2 system, when a
function whose guards have been verified is called on arguments that
satisfy its guard, then the raw lisp function defined by this
function's <code><a href="DEFUN.html">defun</a></code> event is used to evaluate the call. Note
however that even when the user-supplied <code><a href="DEFUN.html">defun</a></code> is not used, ACL2
uses a corresponding ``executable counterpart'' that generally
performs, we expect, nearly as well as the raw lisp function.
See <a href="COMP.html">comp</a> to see how <a href="COMPILATION.html">compilation</a> can speed up both kinds of
execution.<p>
Let us turn next to the issue of the relationship between guards and
evaluation. See <a href="GUARDS-AND-EVALUATION.html">guards-and-evaluation</a>.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
