[plt-scheme] Dracula 2.4 and DoubleCheck

I am pleased to announce the release of Dracula version 2.4 and the
new DoubleCheck book for Dracula.

Dracula is the ACL2 emulation language for DrScheme.  Version 2.4
includes the speed improvements from version 2.1, several bug fixes
and documentation updates, and the new DoubleCheck book.

More information on Dracula and DoubleCheck can be found at
http://www.ccs.neu.edu/home/cce/acl2/ and full documentation on
DoubleCheck can be found in the DrScheme Help Desk after installing
Dracula.

DoubleCheck is a library that provides randomized testing as a
supplement to theorem proving.  It can be used to establish confidence
in a program before proving theorems, or after a failed proof attempt
to find counterexamples.  DoubleCheck works by testing program
properties (potential theorems) with random values for each free
variable.  Here is a sample DoubleCheck property:

;; Test whether the result of nth is actually a member of the given list.
(defproperty nth-produces-a-member 100

 (;; Let lst be a list of between 1 and 10 symbols.
  (lst (random-list-of (random-symbol) (random-int-between 1 10))
       (symbol-listp lst))

  ;; Let idx be a valid index into lst.
  (idx (random-int-between 0 (1- (len lst)))
       (and (natp idx) (< idx (len lst)))))

 ;; Test whether (nth idx lst) is actually in lst.
 (member-equal (nth idx lst) lst))

(check-properties)

Dracula records each property as it is defined.  When the user calls
(check-properties), it runs each property multiple times (in this
case, 100) and reports the random values used in any failure cases.

When a property has been tested to satisfaction, the user can send it
to ACL2 rather than Dracula.  ACL2 interprets each property as a
theorem and simply ignores check-properties.  The example above
corresponds to the ACL2 theorem:

(defthm nth-produces-a-member
 (implies (and (symbol-listp lst)
               (natp idx)
               (< idx (len lst)))
          (member-equal (nth idx lst) lst)))

--
Carl Eastlund