3.2.4 "doublecheck"

(include-book "doublecheck" :dir :teachpacks)

This teachpack defines automated random test generation as a complement to theorem proving. Each property declared via DoubleCheck is tested randomly by Dracula, and verified logically by ACL2.

3.2.4.1 Properties

(defproperty name (bind ...) test)   bind   =   (var hyp maybe-value)           maybe-value   =       |   :value random-expr

(check-properties)

Use defproperty to define DoubleCheck tests in a file, then call check-properties at the end to display the results. This opens a GUI in DrScheme (but renders test results as text in this documentation).

Each defproperty form defines a property called name which states that test must be true for all assignments to free variables, much like defthm. The binding clauses declare the free variables and constrain their values with hypotheses, much like the common use of implies in theorems.

When properties are run in Dracula, it generates random values for the variables during each trial. The hypotheses are used to constrain these values. The user may declare the random distribution used for each variable with a :value clause, or leave it to the default distribution of ACL2 values.

When properties are run in ACL2, they are equivalent to a theorem with hypotheses expressed using implies. Any random distributions, if supplied, are ignored.

Example:

; Prove that reverse is its own inverse:

(defthm reverse-reverse-theorem

(implies (true-listp lst)

(equal (reverse (reverse lst)) lst)))

; Now test the same thing with DoubleCheck:

(defproperty reverse-reverse-property

((lst (true-listp lst)))

(equal (reverse (reverse lst)) lst))

; Run the tests:

(check-properties)

3.2.4.2 Random Distributions

Randomness is an inherently imperative process. As such, it is not reflected in the logic of ACL2. The random distribution functions of DoubleCheck may only be used within :value clauses of defproperty, or in other random distributions.

(random-sexp) → t

(random-atom) → atom

(random-boolean) → booleanp

(random-symbol) → symbolp

(random-char) → characterp

(random-string) → stringp

(random-number) → acl2-numberp

(random-rational) → rationalp

(random-integer) → integerp

(random-natural) → natp

These distributions produce random elements of the builtin Dracula types. When no distribution is given for a property binding, defproperty uses random-sexp by default.

(random-between lo hi) → integerp

lo : integerp

hi : integerp

Produces an integer uniformly distributed between lo and hi, inclusive; lo must be less than or equal to hi.

(random-data-size) → natp

Produces a natural number weighted to prefer small numbers, appropriate for limiting the size of randomly produced values. This is the default distribution for the length of random lists and the size of random s-expressions.

(random-element-of lst) → t

lst : proper-consp

Chooses among the elements of lst, distributed uniformly.

(random-list-of expr maybe-size)

maybe-size   =       |   :size size

Constructs a random list of length size (default (random-data-size)), each of whose elements is the result of evaluating expr.

(random-sexp-of expr maybe-size)

maybe-size   =       |   :size size

Constructs a random cons-tree with size total cons-pairs (default (random-data-size)), each of whose leaves is the result of evaluating expr.

(defrandom name (arg ...) body)

The defrandom form defines new random distributions. It takes the same form as defun, but the body may refer to other random distributions.

Example:

; Construct a distribution for random association lists:

(defrandom random-alist (len)

(random-list-of (cons (random-atom) (random-sexp)) :size len))

; ...and now use it:

(defproperty acons-preserves-alistp

((alist (alistp alist) :value (random-alist (random-between 0 10)))

(key (atom key) :value (random-atom))

(datum t))

(alistp (acons key datum alist)))

(random-case clause ...)

clause   =   expr     |   expr :weight weight

Chooses an expression from the clauses, each with the associated weight (defaulting to 1), and yields its result; the other expressions are not evaluated. This is useful with defrandom for defining recursive distributions.

Be careful of the branching factor; a distribution with a high probability of unbounded recursion is often unlikely to terminate. It is useful to give a depth parameter to limit recursion.

Example:

; Create a distribution for random expressions:

(defrandom random-expression (max-depth)

(random-case

(random-symbol) ; variable

(random-string) ; string literal

(random-number) ; number literal

; one-argument function call

; (probability decreases with max-depth)

(list (random-symbol) (random-expression (1- max-depth)))

:weight (- 1 (/ 1 max-depth))))