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
|
<html>
<head><title>Guards.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>Guards</h2>
<p>
Common Lisp functions are partial; they are not defined for all
possible inputs. But ACL2 functions are total. Roughly speaking,
the logical function of a given name in ACL2 is a <b>completion</B> of
the Common Lisp function of the same name obtained by adding some
arbitrary but ``natural'' values on arguments outside the ``intended
domain'' of the Common Lisp function.<p>
ACL2 requires that every ACL2 function symbol have a ``guard,''
which may be thought of as a predicate on the formals of the
function describing the intended domain. The guard on the primitive
function <code><a href="CAR.html">car</a></code> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a>, for example, is <code>(or (consp x) (equal x nil))</code>,
which requires the argument to be either an ordered pair or
<code>nil</code>. We will discuss later how to specify a guard for a
defined function; when one is not specified, the guard is <code>t</code> which
is just to say all arguments are allowed.<p>
<b>But guards are entirely extra-logical</B>: they are not involved in
the axioms defining functions. If you put a guard on a defined
function, the defining axiom added to the logic defines the function
on <b>all</B> arguments, not just on the guarded domain.<p>
So what is the purpose of guards? <p>
The key to the utility of guards is that we provide a mechanism,
called ``guard verification,'' for checking that all the guards in a
formula are true. See <a href="VERIFY-GUARDS.html">verify-guards</a>. This mechanism will attempt
to prove that all the guards encountered in the evaluation of a
guarded function are true every time they are encountered. <p>
For a thorough discussion of guards, see the paper [km97] in the
ACL2 <a href="BIBLIOGRAPHY.html">bibliography</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>
|
