#lang scribble/doc
@(require scribble/manual scribble/eval "evaluator.ss"
(for-label "../language/dracula.scm"))
@title[#:style 'quiet (scheme "doublecheck")]
@(define doublecheck-evaluator
(evaluator '(include-book "doublecheck" :dir :teachpacks)))
@specform[(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.
@section{Properties}
@deftogether[(
@defform/subs[
#:literals [:value]
(defproperty name (bind ...) test)
([bind (var hyp maybe-value)]
[maybe-value code:blank (code:line :value random-expr)])
]
@defform[(check-properties)]
)]{
Use @scheme[defproperty] to define DoubleCheck tests in a file, then call
@scheme[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 @scheme[defproperty] form defines a property called @scheme[name] which
states that @scheme[test] must be true for all assignments to free variables,
much like @scheme[defthm]. The binding clauses declare the free variables and
constrain their values with hypotheses, much like the common use of
@scheme[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
@scheme[: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 @scheme[implies]. Any random distributions, if
supplied, are ignored.
@bold{Example:}
@schemeblock[
(code:comment #, @t{Prove that reverse is its own inverse:})
(defthm reverse-reverse-theorem
(implies (true-listp lst)
(equal (reverse (reverse lst)) lst)))
(code:comment #, @t{Now test the same thing with DoubleCheck:})
(defproperty reverse-reverse-property
((lst (true-listp lst)))
(equal (reverse (reverse lst)) lst))
(code:comment #, @t{Run the tests:})
(check-properties)
]
}
@section{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 @scheme[:value] clauses of @scheme[defproperty], or in other random
distributions.
@deftogether[(
@defproc[(random-sexp) t]
@defproc[(random-atom) atom]
@defproc[(random-boolean) booleanp]
@defproc[(random-symbol) symbolp]
@defproc[(random-char) characterp]
@defproc[(random-string) stringp]
@defproc[(random-number) acl2-numberp]
@defproc[(random-rational) rationalp]
@defproc[(random-integer) integerp]
@defproc[(random-natural) natp]
)]{
These distributions produce random elements of the builtin Dracula types. When
no distribution is given for a property binding, @scheme[defproperty] uses
@scheme[random-sexp] by default.
}
@defproc[(random-between [lo integerp] [hi integerp]) integerp]{
Produces an integer uniformly distributed between @scheme[lo] and @scheme[hi],
inclusive; @scheme[lo] must be less than or equal to @scheme[hi].
}
@defproc[(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.
}
@defproc[(random-element-of [lst proper-consp]) t]{
Chooses among the elements of @scheme[lst], distributed uniformly.
}
@defform/subs[
#:literals [:size]
(random-list-of expr maybe-size)
([maybe-size code:blank (code:line :size size)])
]{
Constructs a random list of length @scheme[size] (default
@scheme[(random-data-size)]), each of whose elements is the result of evaluating
@scheme[expr].
}
@defform/subs[
#:literals [:size]
(random-sexp-of expr maybe-size)
([maybe-size code:blank (code:line :size size)])
]{
Constructs a random @scheme[cons]-tree with @scheme[size] total
@scheme[cons]-pairs (default @scheme[(random-data-size)]), each of whose leaves
is the result of evaluating @scheme[expr].
}
@defform[(defrandom name (arg ...) body)]{
The @scheme[defrandom] form defines new random distributions. It takes the same
form as @scheme[defun], but the body may refer to other random distributions.
@bold{Example:}
@schemeblock[
(code:comment #, @t{Construct a distribution for random association lists:})
(defrandom random-alist (len)
(random-list-of (cons (random-atom) (random-sexp)) :size len))
(code:comment #, @t{...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)))
]
}
@defform/subs[
#:literals [:weight]
(random-case clause ...)
([clause expr (code:line 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 @scheme[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.
@bold{Example:}
@schemeblock[
(code:comment #, @t{Create a distribution for random expressions:})
(defrandom random-expression (max-depth)
(random-case
(random-symbol) (code:comment #, @t{variable})
(random-string) (code:comment #, @t{string literal})
(random-number) (code:comment #, @t{number literal})
(code:comment #, @t{one-argument function call})
(code:comment #, @t{(probability decreases with max-depth)})
(list (random-symbol) (random-expression (1- max-depth)))
:weight (- 1 (/ 1 max-depth))))
]
}