Major Section: ACL2-BUILT-INS
Non-exec is a macro such that logically,
(non-exec x) is equal to
x. However, the argument to a call of
non-exec need not obey the
usual syntactic restrictions for executable code, and indeed, evaluation of a
non-exec will result in an error. Moreover, for any form
occurring in the body of a function (see defun) that is a call of
non-exec, no guard proof obligations are generated for that form.
The following example, although rather contrived, illustrates the use of
non-exec. One can imagine a less contrived example that efficiently
computes return values for a small number of fixed inputs and, for other
inputs, returns something logically ``consistent'' with those return values.
(defun double (x) (case x (1 2) (2 4) (3 6) (otherwise (non-exec (* 2 x)))))We can prove that
doubleis compliant with Common Lisp (see guard) and that it always computes
(* 2 x).
(verify-guards double) (thm (equal (double x) (* 2 x)))We can evaluate double on the specified arguments. But a call of
non-execresults in an error message that reports the form that was supplied to
ACL2 !>(double 3) 6 ACL2 !>(double 10) ACL2 Error in TOP-LEVEL: ACL2 has been instructed to cause an error because of an attempt to evaluate the following form (see :DOC non- exec): (* 2 X). To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. ACL2 !>
During proofs, the error is silent; it is ``caught'' by the proof mechanism
and generally results in the introduction of a call of
hide during a
Also see defun-nx for a utility that makes every call of a function
non-executable, rather than a specified form. The following examples
defun-nx, in particular illustratating the
non-exec in avoiding guard proof obligations.
; Guard verification fails: (defun-nx f1 (x) (declare (xargs :guard t)) (car x)) ; Guard verification succeeds after changing the guard above: (defun-nx f1 (x) (declare (xargs :guard (consp x))) (car x)) ; Guard verification succeeds: (defun f2 (x) (declare (xargs :guard t)) (non-exec (car x))) ; Evaluating (g1) prints "Hello" before signaling an error. (defun g1 () (f1 (cw "Hello"))) ; Evaluating (g2) does not print before signaling an error. (defun g2 () (non-exec (cw "Hello"))) ; Evaluating (h1) gives a guard violation for taking reciprocal of 0. (defun h1 () (f1 (/ 1 0))) ; Evaluating (h2) does not take a reciprocal, hence there is no guard ; violation for that; we just get the error expected from using non-exec. (defun h2 () (non-exec (/ 0)))