File Search | Catalog | Content Search |

Home » Catalog » Debian » Other »
acl2_4.3.orig.tar.gz » Content »pkg://acl2_4.3.orig.tar.gz:15251431/acl2-sources/books/ info *downloads*## Readme.html

<HEAD><TITLE>The ACL2 Books Directory</TITLE></HEAD> <BODY TEXT="#000000"> <BODY BGCOLOR="#FFFFFF"> <H1>The ACL2 Books Directory</H1> <P> The word ``book'' has two senses to the ACL2 user. One is the normal one: a sequence of printed paper pages bound together between covers. There are such books about ACL2. Click <A HREF="http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html">here</A> for more information. <P> The other sense is a technical one: an ACL2 ``book'' is a file of definitions, theorems and other commands used to extend ACL2's reasoning abilities. Commands add ``rules'' to ACL2's data base. When a book is ``certified,'' ACL2 checks that all the commands in it can be successfully processed. A book can be ``included'' into an ACL2 session to extend the data base. This is the standard way users exchange useful sets of theorems. See the online documentation topic BOOKS for details. <P> The standard distribution of ACL2 comes with many books. They are stored on this directory. This is a guide to the available books. We include instructions on how to certify the books in this directory at the <A HREF="#CertificationInstructions">end</A> of this note. <P> Some of the links below are to files. Others are to directories. When you visit a directory, look at its <CODE>README</CODE> file. Most of these books were written by ACL2 users other than the authors of ACL2. Authorship is acknowledged in the individual files. <UL> <LI><A HREF="Makefile">Makefile</A>: a Unix file for recertifying all the books in this directory.</LI> <LI><A HREF="Makefile-generic">Makefile-generic</A>: a Unix file exploited by <CODE>Makefile</CODE>.</LI> <LI><A HREF="Makefile-subdirs">Makefile-subdirs</A>: a Unix file exploited by <CODE>Makefile</CODE>.</LI> <LI><A HREF="Makefile-psubdirs">Makefile-psubdirs</A>: a Unix file exploited by <CODE>Makefile</CODE>.</LI></LI> <LI><A HREF="README">README</A>: a text file directing you to this file.</LI> <LI><A HREF="Readme.html">Readme.html</A>: this file.</LI> <LI><A HREF="add-ons">add-ons</A>: books which add system-level functionality to ACL2; these should be considered experimental and potentially unsound.</LI> <LI><A HREF="arithmetic">arithmetic</A>: books about arithmetic. The book <CODE>books/arithmetic/top-with-meta.lisp</CODE> may be the most commonly used ACL2 arithmetic book. See the top of <A HREF="arithmetic/README">the README file in this directory</A> for a discussion of arithmetic libraries you may want to use, in particular this one or arithmetic-5. Arithmetic is an extraordinarily rich topic and none of our books fully do it justice. If you develop an improved arithmetic book, let us know!</LI> <LI><A HREF="arithmetic-5">arithmetic-5</A>: books about arithmetic contributed by Robert Krug. The following older libraries are basically superseded by arithmetic-5 (see README files in each directory): <A HREF="arithmetic-2">arithmetic-2</A>, <A HREF="arithmetic-3">arithmetic-3</A>, and <A HREF="arithmetic-4">arithmetic-4</A>.</LI> <A HREF="arithmetic-5">arithmetic-5</A>.</LI> <LI><A HREF="bdd">bdd</A>: books that exercise ACL2's BDD mechanism. </LI> <LI><A HREF="centaur">centaur</A>: books contributed by Centaur formal verification folks; see <CODE><A HREF="centaur/README">centaur/README</A></CODE> </LI> <LI><A HREF="certify-numbers.lisp">certify-numbers.lisp</A>: used to certify the <CODE>cowles</CODE> and <CODE>arithmetic</CODE> books when not using make, e.g., for example, when using a Macintosh. </LI> <LI><A HREF="clause-processors">clause-processors</A>: examples of the use of clause processors (e.g., external tools)</LI> <LI><A HREF="coi">coi</A>: The coi books comprise a "shelf" of ACL2 books related to the modeling of "computational objects" such as processors, memories, kernels, microcode, and so on. </LI> <LI><A HREF="concurrent-programs">concurrent-programs</A>: contributions by Sandip Ray (see </code>Readme.lsp</code> files in subdirectories)</LI> <LI><A HREF="cowles">cowles</A>: support for arithmetic books</LI> <LI><A HREF="cutil">cutil</A>: Centaur Basic Utilities <LI><A HREF="data-structures">data-structures</A>: books for common data structures, with utilities; see also subdirectory <a href="data-structures/memories">memories</a></LI> <LI><A HREF="deduction">deduction</A>: deduction engine(s)</LI> <LI><A HREF="defexec">defexec</A>: fast execution with mbe and defexec</LI> <LI><A HREF="defsort">defsort</A>: <code>defsort</code> defines a stable sort when given a comparison function</LI> <LI><A HREF="finite-set-theory">finite-set-theory</A>: finite sets in ACL2</LI> <LI><A HREF="fix-cert">fix-cert</A>: update relocated .cert files</LI> <LI><A HREF="hacking">hacking</A>: a library for those who wish to use trust tags to modify or extend core ACL2 behavior</LI> <LI><A HREF="hints">hints</A>: tests of hints, especially <code>:or</code> and <code>:custom</code> hints</LI> <LI><A HREF="hons-archive">hons-archive</A>: Implements Hons Archives (HARs), which are a way to write ACL2 objects to disk so they can be loaded in other ACL2 sessions. </LI> <LI><A HREF="ihs">ihs</A>: ``integer hardware specification'', integer arithmetic appropriate for hardware modeling</LI> <LI><A HREF="make-event">make-event</A>: illustrations of <code>make-event</code>, which implements the idea of macros that can take state</LI> <LI><A HREF="meta">meta</A>: metafunctions for arithmetic</LI> <LI><A HREF="misc">misc</A>: a grab-bag of useful books and utilities</LI> <LI><A HREF="models">models</A>: models, especially of digital systems, with associated proofs</LI> <LI><A HREF="nonstd">nonstd</A>: books in support of reasoning about the real numbers in ACL2 using non-standard analysis. If you want this directory, you will need to <a href="nonstd.tar.gz">download the gzipped tar file</a> to your <code>acl2-sources/books/</code> directory, and then gunzip and extract it there.</LI> <LI><A HREF="ordinals">ordinals</A>: books about ordinals</LI> <LI><A HREF="paco">paco</A>: Paco, a cut-down, simplified ACL2-like theorem prover for pedagogical use.</LI> <LI><A HREF="parallel">parallel</A>: example use of primitives for parallelism (with speed-up only in experimental extension that supports parallel evaluation)</LI> <LI><A HREF="powerlists">powerlists</A>: a data-structure suited to the analysis of recursive, data-parallel algorithms.</LI> <LI><A HREF="proofstyles">proofstyles</A>: Soundness and completeness of different proof strategies used in sequential program verification, along with (in subdirectory <code>invclock</code>logical equivalence of two proof styles for verifying programs using operational semantics, namely inductive invariants and clock functions.</LI> <LI><A HREF="quadratic-reciprocity">quadratic-reciprocity</A>: Gauss's Law of Quadratic Reciprocity</LI> <LI><A HREF="regex">regex</A>: a regular expression scanner implementation designed to be similar to GNU Grep</LI> <LI><A HREF="rtl">rtl</A>: floating-point arithmetic support, used for example in proofs about AMD rtl</LI> <LI><A HREF="security">security</A>: books supporting reasoning about security protocols</LI> <LI><A HREF="serialize">serialize</A>: routines for serializing ACL2 objects to disk</li> <LI><A HREF="sorting">sorting</A>: correctness and equivalence of several sort algorithms</LI> <LI><A HREF="str">str</A>: a rudimentary string library for ACL2</LI> <LI><A HREF="symbolic">symbolic</A>: generic proofs of partial and total correctness of sequential programs based on assertional reasoning</LI> <LI><A HREF="system">system</A>: checks of invariants on the ACL2 logical world, and verification of termination and guards of some system functions.</LI> <LI><A HREF="textbook">textbook</A>: solutions to the exercises in <I><A HREF="http://www.cs.utexas.edu/users/moore/publications/acl2-books/car/index.html">Computer-Aided Reasoning: An Approach</A></I></LI> <LI><A HREF="tools">tools</A>: macros and tools designed to make common constructs easier and less verbose to write</LI> <LI><A HREF="tutorial-problems">tutorial-problems/A>: solutions to exercises of a tutorial nature</LI> <LI><A HREF="unicode">unicode</A>: help for reading input from files</LI> <LI><A HREF="wp-gen">wp-gen</A>: Weakest precondition generation and examples</li> <LI><A HREF="xdoc">xdoc</A>: prototype XML documentation system</li> <LI><A HREF="workshops">workshops</A>: Books in support of ACL2 workshops, as listed just below. If you want this directory, you will need to <a href="http://www.cs.utexas.edu/users/moore/acl2/current/distrib/acl2-sources/books/workshops.tar.gz">download the gzipped tar file</a> to your <code>acl2-sources/books/</code> directory, and then gunzip and extract it there.</LI> <UL> <LI><A HREF="workshops/1999">workshops/1999</A>: books from ACL2 Workshop 1999, supporting and described in <I><A HREF="http://www.cs.utexas.edu/users/moore/publications/acl2-books/acs/index.html">Computer-Aided Reasoning: ACL2 Case Studies</A></I>, including full scripts for each case study and answers to all the exercises</LI> <LI><A HREF="workshops/2000">workshops/2000</A>: books and papers from ACL2 Workshop 2000</LI> <LI><A HREF="workshops/2002">workshops/2002</A>: books and papers from ACL2 Workshop 2002</LI> <LI><A HREF="workshops/2003">workshops/2003</A>: books and papers from ACL2 Workshop 2003</LI> <LI><A HREF="workshops/2004">workshops/2004</A>: books and papers from ACL2 Workshop 2004</LI> <LI><A HREF="workshops/2006">workshops/2006</A>: books from ACL2 Workshop 2006</LI> <LI><A HREF="workshops/2007">workshops/2007</A>: books from ACL2 Workshop 2007</LI> <LI><A HREF="workshops/2009">workshops/2009</A>: books from ACL2 Workshop 2009</LI> </UL> </UL> <P> If you seek a book you suspect someone might have created but which is not here, join the ACL2 mailing list and ask the community. <P> If you develop a book you think will be useful to the community, please submit it following the <a href="http://www.cs.utexas.edu/users/moore/acl2/books/index.html">instructions for contributing books to ACL2</a>. <P> <H2><A NAME="CertificationInstructions">Certification Instructions</A></H2> Many of these books are easily imagined to be of general value to ACL2 users, while others are more specialized. Although this subdivision is a bit arbitrary, we refer to books in the former category as "basic" books. By default, the <CODE>make</CODE> process certifies only the basic books. It may take several hours to certify all the books, but only a couple of hours to certify only the "basic" books. <P> All of the instructions below assume that you are standing in subdirectory <CODE>books</CODE> of the ACL2 distribution. <P> <B>EXAMPLES:</B> <P> To certify the <B>basic</B> books, assuming that `<CODE>acl2</CODE>' invokes ACL2, execute: <PRE> make </PRE> To certify <B>all</B> books, assuming that `<CODE>acl2</CODE>' invokes ACL2, execute the following after you download <code><a href="http://www.cs.utexas.edu/users/moore/acl2/v3-0/distrib/acl2-sources/books/workshops.tar.gz"> workshops.tar.gz</a></code> to your <code>acl2-sources/books/</code> directory, and then gunzip and extract it there. <PRE> make all-plus </PRE> To certify the <B>basic</B> books, assuming that `<CODE>my_acl2</CODE>' invokes ACL2, execute: <PRE> make ACL2=my_acl2 </PRE> To certify <B>all</B> books using an image with absolute pathname <CODE>/u/bin/allegro_acl2</CODE> on a Sparc, execute the following. Note that pathnames of images must be absolute pathnames (except that commands observable via the Unix path are OK). <PRE> make all-plus ACL2=/u/bin/allegro_acl2 </PRE> <BR><BR><BR><BR><BR><BR> </BODY> </HTML>

Results 1 - 1 of 1

© 1997-2017 FileWatcher.com