		Search-engine friendly clone of the ACL2 documentation.

Cgen

Test?

Test/Check a conjecture for counterexamples.

Examples

(acl2s::test? (equal (reverse (reverse x)) x))

(test? (implies (and (posp (car x))
                     (posp (cdr x)))
                (= (cdr x) (len x))))


(defun perm (x y)
  (if (endp x)
    (endp y)
    (and (member (car x) y)
         (perm (cdr x) (remove1 (car x) y)))))

(test?
  (implies (and (consp X)
                (member a Y))
           (equal (perm (remove a X)
                        (remove a Y))
                  (perm X Y))))

Note: test? is in ACL2S package.

Usage:

(test? form
       [:hints hints]
       [acl2s-defaults keyword options]
)

Introduction

test? is a powerful counterexample generation facility, based on random testing, that is intended to be used to increase confidence in the truth of a conjecture by providing extensive testing.

test? combines random testing with the power of ACL2 via our data definition framework (defdata). It guarantees that any counterexamples generated are truly counterexamples to the original conjecture. A counterexample is just a binding that maps the variables in the original conjecture to values in the ACL2 universe. In cases where the value of variables are irrelevant, we bind the variables to the symbol ? : these bindings still provide counterexamples, but should raise alarms, since chances are that there is a specification error.

If no counterexample is found, there are three possibilities. First, it is possible that the conjecture is false, in which case increasing the amount of testing we do may lead to the discovery of a counterexample. Second, it is also possible that ACL2 proves that the conjecture is true, in which case we print a message reporting success. Finally, the conjecture may be true, but ACL2 cannot prove it. For all of these three cases, we consider testing to have succeeded, so test? will report success.

test? is an embedded event and can be used in ACL2 ACL2::books. But it is recommended to use them only in the design and in the debug phase, since its use requires trust-tags.

Control Parameters

We can furthur control the behavior of test? using keyword options or acl2s-defaults. All the parameters in acl2s-defaults are available as keyword options to the test? macro and they override the current defaults. The most important parameters to tweak are num-trials, verbosity-level, testing-enabled.

More Examples

(defdata small-pos (enum '(1 2 3 4 5 6 7 8 9)))
(test?
  (implies (and (integerp c1)
                (integerp c2)
                (integerp c3)
                (small-posp x1)
                (small-posp x2)
                (small-posp x3)
                (< x1 x2)
                (< x2 x3)
                (equal 0 (+ c1 c2 c3))
                (equal 0 (+ (* c1 x1) (* c2 x2) (* c3 x3))))
           (and (= 0 c1) (= 0 c2) (= 0 c3))))


(defun square-root1 (i ri)
  (declare (xargs :mode :program))
  (if (>= (floor i ri) ri)
      ri
      (square-root1 i (floor (+ ri (floor i ri)) 2))))

(defun square-root (i)
  (declare (xargs :mode :program))
  (square-root1 i (floor i 2)))

(defun square (x)
   (* x x))


(test?
  (implies (natp i)
           (and (<= (square (square-root i)) i)
                (< i (square (1+ (square-root i)))))))




(defdata triple (list pos pos pos))

(defun trianglep (v)
  (and (triplep v)
       (< (third v) (+ (first v) (second v)))
       (< (first v) (+ (second v) (third v)))
       (< (second v) (+ (first v) (third v)))))

(defun shape (v)
  (if (trianglep v)
      (cond ((equal (first v) (second v))
             (if (equal (second v) (third v))
                 "equilateral"
               "isosceles"))
            ((equal (second v) (third v)) "isosceles")
            ((equal (first v) (third v)) "isosceles")
            (t "scalene"))
    "error"))

(acl2s-defaults :set num-trials 1000000)
(acl2s-defaults :set testing-enabled :naive)

(test?
 (implies (and (triplep x)
               (trianglep x)
               (> (third x) 256)
               (= (third x)
                  (* (second x) (first x))))
          (not (equal "isosceles" (shape x)))))

(acl2s-defaults :set num-trials 1000)

(acl2s-defaults :set testing-enabled t)


(include-book "arithmetic/top-with-meta" :dir :system)

(test?
 (implies (and (triplep x)
               (trianglep x)
               (> (third x) 256)
               (= (third x)
                  (* (second x) (first x))))
          (not (equal "isosceles" (shape x)))))

Advanced Notes

We note that in order to be able to generate counterexamples, we do not allow ACL2 to use any of the following processes: induction, generalization, and cross-fertilization. We do allow destructor-elimination, though in rare cases, user defined elim rules may generalize the conjecture. Such situations are recognized. If you want to enable the above processes, use thm instead, but note that counterexamples shown might not be of the top-level conjecture.