ACL2 is both a programming language in which you can model computer systems and a tool to help you prove properties of those models.
ACL2 is part of the Boyer-Moore family of provers, for which its authors have received the 2005 ACM Software System Award.
Functions that display or change history
ACL2 keeps track of the commands that you have executed that have extended the logic or the rule database, as by the definition of macros, functions, etc. Using the facilities in this section you can review the sequence of commands executed so far. For example, you can ask to see the most recently executed command, or the command 10 before that, or the command that introduced a given function symbol. You can also undo back through some previous command, restoring the logical world to what it was before the given command.
The annotations printed in the margin in response to some of these commands (such as `P', `L', and `V') are explained in the documentation for :pc.
Several technical terms are used in the documentation of the history commands. You must understand these terms to use the commands. These terms are documented via :doc entries of their own. See command, see events, see command-descriptor, and see logical-name.
Libraries (Books).
Libraries of books (files containing definitions and theorems) extend the code that we have written. The installation instructions explain how to fetch the community books, which are contributed and maintained by the members of the ACL2 community. For more information, see the acl2-books project page.
Documentation.
There is an extensive user's manual for the ACL2 system, and an even more comprehensive manual that documents not only the ACL2 system but also many community books. See below to learn more.
License and Copyright.
ACL2 is freely available under the terms of the LICENSE file distributed with ACL2. License, copyright, and authorship information is available from the ACL2 documentation.
Extensions.
The ACL2 distribution includes the following extensions, which were developed by the individuals shown.
ACL2(r)
Support for the real numbers by way of non-standard analysis
Ruben Gamboa
ACL2(h)
Support for hash cons, applicative hash tables, and function memoization for reuse of previously computed results
Bob Boyer, Warren A. Hunt, Jr., Jared Davis, and Sol Swords
ACL2(p)
Support for parallel evaluation
David L. Rager
Another extension of ACL2 is the Eclipse-based ACL2 Sedan (ACL2s). Unlike the systems above, ACL2s is distributed and maintained by Pete Manolios and his research group. ACL2s comes with a standard executable ACL2 image for Windows, but it also comes with pre-certified community books and an extension of ACL2 with additional features, including extra automation for termination proofs as well as counterexample generation.
To learn about ACL2, read at least the following two links.
Industrial Applications of ACL2 (10 minutes) to help you understand what sophisticated users can do;
A Flying Tour (10 minutes) to get an overview of the system and what skills the user must have.
If you want to learn how to use ACL2, we recommend that you read a selection of the materials referenced below, depending on your learning style, and do suggested exercises.
A Walking Tour (1 hour) provides an overview of the theorem prover.
The Try ACL2 [External link to http://tryacl2.org] web site provides interactive lessons to get you started using ACL2.
Introduction to the Theorem Prover (10-40 hours) provides instruction on how to interact with the system. Unlike the three documents above, this document expects you to think! It cites the necessary background pages on programming in ACL2 and on the logic and then instructs you in the-method, which is how expert users use ACL2. It concludes with some challenge problems for the ACL2 beginner (including solutions) and an FAQ. Most users will spend several hours a day for several days working through this material.
The book Computer-Aided Reasoning: An Approach [External link to http://www.cs.utexas.edu/users/moore/publications/acl2-books/car/index.html] is worth a careful read, as you work exercises and learn the-method.
Annotated ACL2 Scripts and Demos contains relatively elementary proof scripts that have been annotated to help train the newcomer.
Many files (``books'') in the ACL2 community books (see community-books) are extensively annotated.
An Alternative Introduction document, while largely subsumed by the Introduction to the Theorem Prover mentioned above, still might be useful because it covers much of the tutorial material in a different way.
At this point you are probably ready to use ACL2 on your own small projects. A common mistake for beginners is to browse the documentation and then try to do something that is too big! Think of a very small project and then simplify it!
Note that ACL2 has a very supportive user network. See the link to ``Mailing Lists'' on the ACL2 home page [External link to http://www.cs.utexas.edu/users/moore/acl2] .
The topics listed below are a hodge podge, developed over time. Although some of these are not mentioned above, you might find some to be useful as well.
If you liked this article, subscribe to the feed by clicking the image below to keep informed about new contents of the blog:
0 commenti:
Post a Comment