VERIFY-TERMINATION

convert a function from :program mode to :logic mode 
Major Section:  EVENTS


Example:
(verify-termination fact)


General Forms:
(verify-termination fn dcl ... dcl)
(verify-termination (fn1 dcl ... dcl)
                    (fn2 dcl ... dcl)
                    ...)
where fn and the fni are function symbols having :program mode (see defun-mode) and all of the dcls are either declare forms or documentation strings. The first form above is an abbreviation for 
(verify-termination (fn dcl ... dcl))
so we limit our discussion to the second form. Each of the fni must be in the same clique of mutually recursively defined functions, but not every function in the clique need be among the fni.

Verify-termination attempts to establish the admissibility of the fni. Verify-termination retrieves their definitions, creates modified definitions using the dcls supplied above, and resubmits these definitions. You could avoid using verify-termination by typing the new definitions yourself. So in that sense, verify-termination adds no new functionality. But if you have prototyped your system in :program mode and tested it, you can use verify-termination to resubmit your definitions and change their defun-modes to :logic, addings hints without having to retype or recopy the code.

The defun command executed by verify-termination is obtained by retrieving the defun (or mutual-recursion) command that introduced the clique in question and then possibly modifying each definition as follows. Consider a function, fn, in the clique. If fn is not among the fni above, its definition is left unmodified other than to add (declare (xargs :mode :logic)). Otherwise, fn is some fni and we modify its definition by inserting into it the corresponding dcls listed with fni in the arguments to verify-termination, as well as (declare (xargs :mode :logic)). In addition, we throw out from the old declarations in fn the :mode specification and anything that is specified in the new dcls.

For example, suppose that fact was introduced with: 

(defun fact (n)
  (declare (type integer n)
           (xargs :mode :program))
  (if (zp n) 1 (* n (fact (1- n))))).
Suppose later we do (verify-termination fact). Then the following definition is submitted. 
(defun fact (n)
  (declare (type integer n))
  (if (zp n) 1 (* n (fact (1- n))))).
Observe that this is the same definition as the original one, except the old specification of the :mode has been deleted so that the defun-mode now defaults to :logic. Although the termination proof succeeds, ACL2 also tries to verify the guard, because we have (implicitly) provided a guard, namely (integerp n), for this function. (See guard for a general discussion of guards, and see type-spec for a discussion of how type declarations are used in guards.) Unfortunately, the guard verification fails, because the subterm (zp n) requires that n be nonnegative, as can be seen by invoking :args zp. (For a discussion of termination issues relating to recursion on the naturals, see zero-test-idioms.) So we might be tempted to submit the following: 
(verify-termination
 fact 
 (declare (xargs :guard (and (integerp n) (<= 0 n))))).
However, this is considered a changing of the guard (from (integerp n)), which is illegal. If we instead change the guard in the earlier defun after undoing that earlier definition with :ubt fact, then (verify-termination fact) will succeed.