;;===========================================================================
;; Copyright (C) 1999 Institut fuer Informatik, University of Kiel, Germany
;;===========================================================================
;; File:         README
;; Author:       Wolfgang Goerigk
;; Content:      README for ACL2 Book Contribution
;; as of:        12/04/00, University of Kiel, Germany
;;---------------------------------------------------------------------------
;; $Revision: 1.1 $
;; $Id: README,v 1.1 2000/04/16 12:09:36 wg Exp wg $
;;===========================================================================

 The  series of ACL2  books in  this directory  goes with  the article
 "Wolfgang Goerigk:  Compiler Verification  Revisited" as part  of the
 book  "Computer Aided Reasoning:  ACL2 Case  Studies" edited  by Matt
 Kaufmann, Pete Manolios and J Strother Moore.

======================================================================

This distribution contains the following files:

 - REAME            ; this file
 - machine.lisp     ; the TL machine formalization
 - compiler.lisp    ; the SL (miniComLisp) to TL compiler
 - exercises.lisp   ; solutions to the exercises from the paper
 - evaluator.lisp   ; the SL semantics
 - proof1.lisp      ; part 1 of the compiler correctness proof
 - proof.lisp       ; part 2 of the compiler correctness proof

On a  Unix system, you can certify  the books by typing  make, if this
directory  is  under  books/case-studies/  in  an  ACL2  distribution.
Otherwise, In  order to use the  ACL2 scripts, you  should certify the
book "machine". Start ACL2 in this directory and type

   (certify-book "machine" 0 t)  

You may  then step through the  other scripts or certify  them as well
(using a similar command, see below).

----------------------------------------------------------------------

TL Machine and SL to TL Compiler:
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   o "machine"     
   o "compiler"    (includes the book "machine")

define the TL  Machine (see "machine.lisp") and the  SL to TL Compiler
(see  "compiler.lisp").  The  machine formalization  must  be compiled
using  (certify-book "machine"  0 t),  or  equivalently, (certify-book
"machine"), before  you process the events  in compiler or  any of the
other scripts below (since they include the machine book).

Solutions to the Exercises
~~~~~~~~~~~~~~~~~~~~~~~~~~

    o "exercises"   (includes the book "compiler")

 gives solutions to the exercises from the article and some additional
 stuff.
 
SL Semantics and Compiler Correctness Proof
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

    o "evaluator"   (includes the book "compiler")
    o "proof1"      (includes the book "evaluator")
    o "proof.lisp"  (includes the book "proof1")

 The books  "proof1" and "proof"  (in that order)  prove the SL  to TL
 compiler  correct with  respect to  the SL  semantics (as  defined in
 "evaluator.lisp") and the machine semantics.

 If you  certify these books, you  will find ACL2  complain about some
 missing guard verification, but you  may just ignore the warnings. If
 you certify  the books,  you should (1)  certify "machine",  then (2)
 certify  "compiler", then  (3)  "evaluator", then  (4) "proof1",  and
 finally you may also certify "proof". You may step through the proofs
 as well, but "machine" must be compiled.