📄 http:^^www.cs.utexas.edu^users^sawada^acl2^acl2-doc.html
字号:
MIME-Version: 1.0
Server: CERN/3.0
Date: Monday, 06-Jan-97 21:39:36 GMT
Content-Type: text/html
Content-Length: 4568
Last-Modified: Wednesday, 04-Sep-96 03:37:07 GMT
<head><title>ACL2 Version 1.9</title></head><!WA0><img src="http://www.cs.utexas.edu/users/sawada/ACL2/logo.gif" align=top ALT="ACL2"><BR><BR><BR><h1>ACL2 Version 1.9</h1>Copyright (C) 1989-96 <!WA1><A HREF="http://www.cli.com">Computational Logic, Inc. (CLI)</A>.All rights reserved.<p><h2>ACL2 is a programming language in which you can model computer hardware andsoftware, as well as a tool to help you prove properties of those models.</h2><BR>The paper <!WA2><A HREF="http://www.cs.utexas.edu/users/reports/bkm96.ps">ACL2 Theorems about Commercial Microprocessors</A>(with Bishop Brock) briefly discusses the system and two ``industrialstrength'' applications, the Motorola CAP project and the AMD5K86 floatingpoint division project. See also <!WA3><A HREF="#Selected References">Selected References</A>.<BR><BR>We have two Web browser ``<!WA4><A HREF="http://www.cs.utexas.edu/users/sawada/ACL2/acl2-doc-48.html#The Tours">Tours</A>'' to introduce you to ACL2,as well as a <!WA5><A HREF="http://www.cs.utexas.edu/users/sawada/ACL2/acl2-doc-1.html#ACL2-TUTORIAL">Tutorial</A>.<BR><BR>To obtain ACL2<ul><li>Read the <!WA6><A HREF="http://www.cli.com/ftp/pub/acl2/LICENSE">License Agreement</A> and if you agree to its terms,<li>download the ACL2 <!WA7><A HREF="ftp://ftp.cli.com:/pub/acl2/v1-9/acl2.tar.gz">Sources and Documentation</A> and then<li>follow the <!WA8><A HREF="http://www.cli.com/ftp/pub/acl2/v1-9/README">Installation Instructions</A>.You may be able to save time by obtaining a<!WA9><A HREF="#Images">binary image</A> before following the Installation Instructions.</ul><h2>Matt Kaufmann and J Strother Moore</h2>September 3, 1996<br><br><H2><A NAME="Selected References">Selected References</A></H2><UL><li><!WA10><A HREF="http://www.cs.utexas.edu/users/reports/km94.ps">Design Goals for ACL2</A>-- an early report identifying aspects of Nqthm of special concern duringthe design of ACL2.<li><!WA11><A HREF="http://www.cs.utexas.edu/users/reports/km96.ps">ACL2: An Industrial Strength Version of Nqthm</A>-- how we scaled up the Nqthm (``Boyer-Moore'') logic to CommonLisp, preserving the use of total functions within the logic but achievingCommon Lisp execution speeds.<li><!WA12><A HREF="http://devil.ece.utexas.edu:80/~lynch/divide/divide.html">A Mechanically Checked Proof of the Correctness of the Kernel of the AMD5K86 Floating-Point Division Algorithm</A>(with Tom Lynch) -- the mathematical details of the floating-pointdivision proof.<li><!WA13><A HREF="http://www.cs.utexas.edu/users/reports/y96a.ps">Interactive Consistency in ACL2</A>(by Bill Young) -- an ACL2 translation of Rushby's PVS improvement toBevier and Young's Nqthm formalization of the Pease, Shostak and Lamport OralMessages (``Byzantine Generals'') problem.<li><!WA14><A HREF="http://www.cs.utexas.edu/users/reports/y96b.ps">The Specification of a Simple Autopilot in ACL2</A>(by Bill Young) -- an ACL2 translation of Butler's PVS formalization of asimple autopilot.<li><!WA15><A HREF="http://www.cs.utexas.edu/users/reports/bm96.ps">Mechanized Formal Reasoning about Programs and Computing Machines</A>(by Boyer and Moore) -- explains a formalization style which hasbeen extremely successful in enabling mechanized reasoning about programsand machines, illustrated in ACL2.<li><!WA16><A HREF="ftp://ftp.cli.com:/pub/acl2/v1-9/acl2-sources/doc/TEX/acl2-book.ps.gz">ACL2 Documentation</A>-- the complete ACL2 documentation tree in the form of a compressed (gzip'd)postscript file. When uncompressed the documentation is approximately 3.5megabytes of postscript and prints as an 800 page book. The documentation ismost useful in its HTML or Texinfo forms, where the links in it can be browsedinteractively. The complete HTML documentation tree is available via the Indexbelow or organized by<!WA17><A HREF="http://www.cs.utexas.edu/users/sawada/ACL2/acl2-doc-major-topics.html">Major Topics</A>.We recommend that you start with the guided <!WA18><A HREF="http://www.cs.utexas.edu/users/sawada/ACL2/acl2-doc-48.html#The Tours">Tours</A>.</ul><!WA19><A HREF="http://www.cs.utexas.edu/users/sawada/ACL2/acl2-doc-index.html"><!WA20><img src=http://www.cs.utexas.edu/users/sawada/ACL2/index.gif></A><H2><A NAME="Images">Images</A></H2>If your machine is listed below, you can avoid rebuilding ACL2 by obtaining abinary image. You should nevertheless read the<!WA21><A HREF="http://www.cli.com/ftp/pub/acl2/LICENSE">License Agreement</A>and obtain the<!WA22><A HREF="ftp://ftp.cli.com:/pub/acl2/v1-9/acl2.tar.gz">Sources and Documentation</A>.Then download the appropriate image and follow theQUICK AND EASY INSTALLATION INSTRUCTIONS in<!WA23><A HREF="http://www.cli.com/ftp/pub/acl2/v1-9/README">Installation Instructions</A>.<ul><li><!WA24><A HREF="ftp://ftp.cli.com:/pub/acl2/v1-9/images/os-4-sparc-saved_acl2.tar.gz">Sun OS 4.1.3_U1 for Sparc</A><li><!WA25><A HREF="ftp://ftp.cli.com:/pub/acl2/v1-9/images/solaris-2-5-sparc-saved_acl2.tar.gz">Solaris 2.5 for Sparc</A><li><!WA26><A HREF="ftp://ftp.cli.com:/pub/acl2/v1-9/images/solaris-2-5-x86-saved_acl2.tar.gz">Solaris 2.5 for x86</A></ul>⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -