The books in this directory define a refinement proof correlating
a concurrent deque implementation to a simple deque specification.

The refinement proof is broken into the following chain:

     cdeq <-> cdeq+ <-> intr <-> intr+ >> spec

Gzipped tar file: cdeq.tar.gz

BOOK descriptions
-----------------
records.lisp     -- defines record operations and theorems
cdeq-defs.lisp   -- defines the step functions and several supporting lemmas
 -- presents proof that cdeq and cdeq+ are equivalent
 -- presents proof that cdeq+ and intr are equivalent
 -- presents proof that intr and intr+ are equivalent
 -- presents proof that intr+ is a refinement of spec

To build the books in this directory (in the correct order), perform the
following commands, or else just type make on a Unix or Linux
system if this directory is installed in a copy of the ACL2 distribution, under
books/workshops/2000/sumners1/cdeq/.

<shell> ACL2
<lisp>  (lp)
ACL2 !> (ld "make.lsp")


   -Rob Sumners
    robert.sumners@amd.com