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
cdeq-phase1.lisp -- presents proof that cdeq and cdeq+ are equivalent
cdeq-phase2.lisp -- presents proof that cdeq+ and intr are equivalent
cdeq-phase3.lisp -- presents proof that intr and intr+ are equivalent
cdeq-phase4.lisp -- presents proof that intr+ is a refinement of spec

To build the books in this directory (in the correct order),
perform the following commands:

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


   -Rob Sumners
    robert.sumners@amd.com