File: GUARD-EXAMPLE.html

package info (click to toggle)
acl2 3.1-1
  • links: PTS
  • area: main
  • in suites: etch, etch-m68k
  • size: 36,712 kB
  • ctags: 38,396
  • sloc: lisp: 464,023; makefile: 5,470; sh: 86; csh: 47; cpp: 25; ansic: 22
file content (319 lines) | stat: -rw-r--r-- 9,881 bytes parent folder | download
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
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
<html>
<head><title>GUARD-EXAMPLE.html  --  ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h4>GUARD-EXAMPLE</h4>a brief transcript illustrating <a href="GUARD.html">guard</a>s in ACL2
<pre>Major Section:  <a href="TUTORIAL5-MISCELLANEOUS-EXAMPLES.html">TUTORIAL5-MISCELLANEOUS-EXAMPLES</a>
</pre><p>

This note addresses the question:  what is the use of <a href="GUARD.html">guard</a>s in
ACL2?  Although we recommend that beginners try to avoid <a href="GUARD.html">guard</a>s for
a while, we hope that the summary here is reasonably self-contained
and will provide a reasonable introduction to guards in ACL2.  For a
more systematic discussion, see <a href="GUARD.html">guard</a>.  For a summary of that
topic, see <a href="GUARD-QUICK-REFERENCE.html">guard-quick-reference</a>.<p>

Before we get into the issue of <a href="GUARD.html">guard</a>s, let us note that there are
two important ``modes'':<p>

<a href="DEFUN-MODE.html">defun-mode</a> -- ``Does this <a href="DEFUN.html">defun</a> add an axiom (`:logic mode') or not
(`:program mode')?''  (See <a href="DEFUN-MODE.html">defun-mode</a>.)  Only <code>:</code><code><a href="LOGIC.html">logic</a></code> mode
functions can have their ``<a href="GUARD.html">guard</a>s verified'' via mechanized proof;
see <a href="VERIFY-GUARDS.html">verify-guards</a>.<p>

<code><a href="SET-GUARD-CHECKING.html">set-guard-checking</a></code> -- ``Should runtime <a href="GUARD.html">guard</a> violations signal an
error (<code>:all</code>, and usually with <code>t</code> or <code>:nowarn</code>) or go undetected
(<code>nil</code>, <code>:none</code>)?  Equivalently, are expressions evaluated in Common Lisp
or in the logic?''  (See <a href="SET-GUARD-CHECKING.html">set-guard-checking</a>.)
<p>
<em>Prompt examples</em><p>

Here some examples of the relation between the ACL2 <a href="PROMPT.html">prompt</a> and the
``modes'' discussed above.  Also see <a href="DEFAULT-PRINT-PROMPT.html">default-print-prompt</a>.  The
first examples all have <code>ld-skip-proofsp nil</code>; that is, proofs are
<em>not</em> skipped.

<pre><p>

  ACL2 !&gt;    ; logic mode with guard checking on
  ACL2 &gt;     ; logic mode with guard checking off
  ACL2 p!&gt;   ; program mode with guard checking on
  ACL2 p&gt;    ; program mode with guard checking off<p>

</pre>

Here are some examples with <code><a href="DEFAULT-DEFUN-MODE.html">default-defun-mode</a></code> of <code>:</code><code><a href="LOGIC.html">logic</a></code>.

<pre><p>

  ACL2 &gt;     ; guard checking off, ld-skip-proofsp nil
  ACL2 s&gt;    ; guard checking off, ld-skip-proofsp t
  ACL2 !&gt;    ; guard checking on, ld-skip-proofsp nil
  ACL2 !s&gt;   ; guard checking on, ld-skip-proofsp t<p>

</pre>
<p>

<em>Sample session</em><p>


<pre>
ACL2 !&gt;(+ 'abc 3)<p>

ACL2 Error in TOP-LEVEL: The guard for the function symbol
BINARY-+, which is (AND (ACL2-NUMBERP X) (ACL2-NUMBERP Y)),
is violated by the arguments in the call (+ 'ABC 3).<p>

ACL2 !&gt;:set-guard-checking nil
;;;; verbose output omitted here
ACL2 &gt;(+ 'abc 3)
3
ACL2 &gt;(&lt; 'abc 3)
T
ACL2 &gt;(&lt; 3 'abc)
NIL
ACL2 &gt;(&lt; -3 'abc)
T
ACL2 &gt;:set-guard-checking t<p>

Turning guard checking on, value T.<p>

ACL2 !&gt;(defun sum-list (x)
        (declare (xargs :guard (integer-listp x)
                        :verify-guards nil))
        (cond ((endp x) 0)
              (t (+ (car x) (sum-list (cdr x))))))<p>

The admission of SUM-LIST is trivial, using the relation
O&lt; (which is known to be well-founded on the domain
recognized by O-P) and the measure (ACL2-COUNT X).
We observe that the type of SUM-LIST is described by the
theorem (ACL2-NUMBERP (SUM-LIST X)).  We used primitive type
reasoning.<p>

Summary
Form:  ( DEFUN SUM-LIST ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.03 seconds
   (prove: 0.00, print: 0.00, proof tree: 0.00, other: 0.03)
 SUM-LIST
ACL2 !&gt;(sum-list '(1 2 3))<p>

ACL2 Warning [Guards] in TOP-LEVEL:  Guard-checking will be inhibited
on recursive calls of the executable counterpart (i.e., in the ACL2
logic) of SUM-LIST.  To check guards on all recursive calls:
  (set-guard-checking :all)
To leave behavior unchanged except for inhibiting this message:
  (set-guard-checking :nowarn)<p>

6
ACL2 !&gt;(sum-list '(1 2 abc 3))<p>

ACL2 Error in TOP-LEVEL: The guard for the function symbol
BINARY-+, which is (AND (ACL2-NUMBERP X) (ACL2-NUMBERP Y)),
is violated by the arguments in the call (+ 'ABC 3).<p>

ACL2 !&gt;:set-guard-checking nil
;;;; verbose output omitted here
ACL2 &gt;(sum-list '(1 2 abc 3))
6
ACL2 &gt;(defthm sum-list-append
       (equal (sum-list (append a b))
              (+ (sum-list a) (sum-list b))))<p>

&lt;&lt; Starting proof tree logging &gt;&gt;<p>

Name the formula above *1.<p>

Perhaps we can prove *1 by induction.  Three induction
schemes are suggested by this conjecture.  Subsumption
reduces that number to two.  However, one of these is flawed
and so we are left with one viable candidate.<p>

...<p>

That completes the proof of *1.<p>

Q.E.D.
</pre>
<p>

<em>Guard verification vs. defun</em><p>


<pre><p>

      Declare Form                        Guards Verified?<p>

  (declare (xargs :mode :program ...))          no
  (declare (xargs :guard g))                    yes
  (declare (xargs :guard g :verify-guards nil)) no
  (declare (xargs ...&lt;no :guard&gt;...))           no<p>

ACL2 &gt;:pe sum-list
 l        8  (DEFUN SUM-LIST (X)
              (DECLARE (XARGS :GUARD (INTEGER-LISTP X)
                              :VERIFY-GUARDS NIL))
              (COND ((ENDP X) 0)
                    (T (+ (CAR X) (SUM-LIST (CDR X))))))
ACL2 &gt;(verify-guards sum-list)
The non-trivial part of the guard conjecture for SUM-LIST,
given the :type-prescription rule SUM-LIST, is<p>

Goal
(AND (IMPLIES (AND (INTEGER-LISTP X) (NOT (CONSP X)))
              (EQUAL X NIL))
     (IMPLIES (AND (INTEGER-LISTP X) (NOT (ENDP X)))
              (INTEGER-LISTP (CDR X)))
     (IMPLIES (AND (INTEGER-LISTP X) (NOT (ENDP X)))
              (ACL2-NUMBERP (CAR X)))).<p>

...<p>

ACL2 &gt;:pe sum-list
 lv       8  (DEFUN SUM-LIST (X)
              (DECLARE (XARGS :GUARD (INTEGER-LISTP X)
                              :VERIFY-GUARDS NIL))
ACL2 &gt;:set-guard-checking t

Turning guard checking on, value T.

ACL2 !&gt;(sum-list '(1 2 abc 3))<p>

ACL2 Error in TOP-LEVEL: The guard for the function symbol
SUM-LIST, which is (INTEGER-LISTP X), is violated by the
arguments in the call (SUM-LIST '(1 2 ABC ...)).  See :DOC wet
for how you might be able to get an error backtrace.<p>

ACL2 !&gt;:set-guard-checking nil
;;;; verbose output omitted here
ACL2 &gt;(sum-list '(1 2 abc 3))
6
ACL2 &gt;:comp sum-list
Compiling gazonk0.lsp.
End of Pass 1.
End of Pass 2.
Finished compiling gazonk0.lsp.
Loading gazonk0.o
start address -T 1bbf0b4 Finished loading gazonk0.o
Compiling gazonk0.lsp.
End of Pass 1.
End of Pass 2.
Finished compiling gazonk0.lsp.
Loading gazonk0.o
start address -T 1bc4408 Finished loading gazonk0.o
 SUM-LIST
ACL2 &gt;:q<p>

Exiting the ACL2 read-eval-print loop.
ACL2&gt;(trace sum-list)
(SUM-LIST)<p>

ACL2&gt;(lp)<p>

ACL2 Version 1.8.  Level 1.  Cbd "/slocal/src/acl2/v1-9/".
Type :help for help.
ACL2 &gt;(sum-list '(1 2 abc 3))
6
ACL2 &gt;(sum-list '(1 2 3))
  1&gt; (SUM-LIST (1 2 3))&gt;
    2&gt; (SUM-LIST (2 3))&gt;
      3&gt; (SUM-LIST (3))&gt;
        4&gt; (SUM-LIST NIL)&gt;
        &lt;4 (SUM-LIST 0)&gt;
      &lt;3 (SUM-LIST 3)&gt;
    &lt;2 (SUM-LIST 5)&gt;
  &lt;1 (SUM-LIST 6)&gt;
6
ACL2 &gt;:pe sum-list-append
          9  (DEFTHM SUM-LIST-APPEND
                     (EQUAL (SUM-LIST (APPEND A B))
                            (+ (SUM-LIST A) (SUM-LIST B))))
ACL2 &gt;(verify-guards sum-list-append)<p>

The non-trivial part of the guard conjecture for
SUM-LIST-APPEND, given the :type-prescription rule SUM-LIST,
is<p>

Goal
(AND (TRUE-LISTP A)
     (INTEGER-LISTP (APPEND A B))
     (INTEGER-LISTP A)
     (INTEGER-LISTP B)).<p>

...<p>

****** FAILED ******* See :DOC failure ****** FAILED ******
ACL2 &gt;(defthm common-lisp-sum-list-append
         (if (and (integer-listp a)
                  (integer-listp b))
             (equal (sum-list (append a b))
                    (+ (sum-list a) (sum-list b)))
             t)
         :rule-classes nil)<p>

&lt;&lt; Starting proof tree logging &gt;&gt;<p>

By the simple :rewrite rule SUM-LIST-APPEND we reduce the
conjecture to<p>

Goal'
(IMPLIES (AND (INTEGER-LISTP A)
              (INTEGER-LISTP B))
         (EQUAL (+ (SUM-LIST A) (SUM-LIST B))
                (+ (SUM-LIST A) (SUM-LIST B)))).<p>

But we reduce the conjecture to T, by primitive type
reasoning.<p>

Q.E.D.
;;;; summary omitted here
ACL2 &gt;(verify-guards common-lisp-sum-list-append)<p>

The non-trivial part of the guard conjecture for
COMMON-LISP-SUM-LIST-APPEND, given the :type-prescription
rule SUM-LIST, is<p>

Goal
(AND (IMPLIES (AND (INTEGER-LISTP A)
                   (INTEGER-LISTP B))
              (TRUE-LISTP A))
     (IMPLIES (AND (INTEGER-LISTP A)
                   (INTEGER-LISTP B))
              (INTEGER-LISTP (APPEND A B)))).<p>

...<p>

Q.E.D.<p>

That completes the proof of the guard theorem for
COMMON-LISP-SUM-LIST-APPEND.  COMMON-LISP-SUM-LIST-APPEND
is compliant with Common Lisp.
;;;; Summary omitted here.
ACL2 &gt;(defthm foo (consp (mv x y)))<p>

...<p>

Q.E.D.<p>

</pre>


<pre>
ACL2 &gt;(verify-guards foo)<p>

ACL2 Error in (VERIFY-GUARDS FOO): The number of values we
need to return is 1 but the number of values returned by the
call (MV X Y) is 2.<p>

&gt; (CONSP (MV X Y))<p>


ACL2 Error in (VERIFY-GUARDS FOO): The guards for FOO cannot
be verified because the theorem has the wrong syntactic
form.  See :DOC verify-guards.
</pre>

<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>