{{An ACL2 Tutorial Matt Kaufmann (speaker) and J Strother Moore Department of Computer Sciences, University of Texas at Austin kaufmann@cs.utexas.edu moore@cs.utexas.edu NOTE: Please feel free to ask questions. I've left a few minutes for questions at the end, but we can use any of that time during the talk instead. +++++}} ================================================================= {{Section: Introduction ACL2 is: o `ACLACL' - `A Computational Logic for Applicative Common Lisp' - a functional programming language compatible with Common Lisp - a first-order logic with induction and recursive definition - a mechanized proof system o authored by Matt Kaufmann and J Moore - begun by Bob Boyer and J Moore in 1989 (more like 1971....) o written primarily in itself - applicative state (stobjs), multiple values, ... o used in a number of verification efforts, including industry o freely available under GPL at http://www.cs.utexas.edu/users/moore/acl2/ - links: demos (e.g. this), mailing lists, documentation, ... +++++}} {{About this talk: o User perspective: how to interact effectively with ACL2 - ACL2 is viewed as a controllable black box o NOT covered: - Implementor perspective (e.g., heuristics) - How to build fancy custom reasoning tools - ACL2 as a functional programming language - Applications (See links to publications, workshops, tutorials, books) - Eclipse-based interfaces (ACL2s, DrACuLa) - Other stuff.... +++++}} {{How to do proofs with ACL2: o Prove rules, typically conditional rewrite rules, for ACL2 to apply automatically to put terms in normal form. o Obtain effective feedback from a failed proof, to discover additional rules to prove -- then try the proof again after proving such rules. See online/HTML/Emacs-Info documentation, e.g., for THE-METHOD. Let's start.... I will introduce Lisp syntax as I go, though very briefly. Proceedings paper includes references, omitted here. +++++}} ========================================================== {{Section: Basics of Interaction with ACL2 Here I'll present the main demo, perm-rev.lisp: Define recursively a notion of permutation, and prove: o This notion is an equivalence relation. o The reverse of a list is a permutation of the list. Of course this is just a small, pedagogical example. But it does illustrate typical interaction style. ########## DEMO ##########}} {{Summary of what was shown in the first demo: o Using simplification checkpoints to debug proof failures o Top-down proof development, with skip-proofs and undoing o Helpful proof automation, in particular rewriting - conditional, contextual, congruence-based - heuristics, e.g. for stopping loops (see :DOC loop-stopper) o Prover hints o Touched on library development and scopes (see :DOC local), and perhaps ``proof-checker'' goal manager. o Destructor-style recursion o Automation (proving termination, doing induction, rewriting) +++++}} ==================================================== {{Section: A JVM Model Next, we demonstrate the so-called M5 model of the Java Virtual Machine (JVM), to show a bit how ACL2 models digital systems. I'll go quickly through file jvm-demo/demo.input now, with a focus on illustrating ACL2 use, not on the JVM. ########## DEMO ########## }} {{This demo illustrated several aspects of ACL2: o Library re-use; see :DOC include-book o Namespace support; see :DOC defpkg o Efficient evaluation supporting simulation of models o User-defined syntax; see :DOC defmacro +++++}} ========================================================= {{Section: Proof Debugging and Theory Management This short demo shows how ACL2 can help to identify rules that slow it down. I'll run through file dmr.lisp now.... ########## DEMO ########## }} {{Lessons of this demo included: o Management of enabled rule sets (see :DOC theories) o Helpful statistics on rule use (see :DOC accumulated-persistence), with helpful feedback on options o Dynamic monitoring of the rewrite stack (see :DOC dmr) +++++}} ========================================================= {{Section: Concluding Remarks For more about ACL2, including applications, see the home page. Feel free to talk with me later today -- e.g., put me on the spot with your own challenge problems. Advertisement: Tomorrow's UITP talk at 4:00 (another debugging tool, for example....) Acknowledgements: NSF, DARPA, others; see home page. Thanks also to Sandip Ray for helpful feedback during preparation of this talk. Questions? +++++}} More, as time permits: ---------------------- ACL2 runs on a number of Common Lisp implementations. Why? - Some find implementation errors that others miss. - Lots of options for users (different Lisps have different strengths, e.g.: ^C-C problem on Windows for SBCL; nice debugger on Allegro CL, but it's not free) - Continuity -- Lisps can come and go Below is a partial list of useful ACL2 features not mentioned above, many of them requested by users. o quantification via Skolemization (see :DOC defun-sk) o MBE ("must be equal"), a primitive for user-installed executable counterparts -- Example is given in tomorrow's UITP talk -- Example from Rob Sumners disributed as set of books culminating in books/defexec/other-apps/qsort/final-theorem.lisp, where: isort: simple functional insertion sort qsort: uses local single-threaded object (see :DOC stobj and see :DOC with-local-stobj) (defun sort-list (x) (declare (xargs :guard (true-listp x))) (mbe :logic (isort x) :exec (qsort x))) -- Example: When I was at AMD I added a bunch of mbe calls, resulting in appropriate proof obligations but no changes to existing proofs o proof control, including user-installed metatheoretic simplifiers, user-supplied syntactic conditions for rewrite rules, and dynamically computed hints o traditional tactics (see :DOC macro-command) for the interactive goal manager (see :DOC proof-checker) o partially-defined functions (see :DOC encapsulate) and, mimicking second-order logic, functional instantiation o capabilities supporting fancy custom verification environments: see :DOC table, see :DOC state (applicative semantics), and see :DOC make-event for an extended macro capability useful in defining templates o see :DOC guard -- may be viewed as a general, semantic replacement for types o many modes and switches (see :DOC switches-parameters-and-modes) o hooks to external tools (see :DOC clause-processor), either to be verified or else ``tagged'' (see :DOC defttag) with careful logical story o experimental extensions others have initiated, to support: - (Gamboa) Real numbers via non-standard analysis - (Boyer, Hunt) Hash cons, function memoization, and applicative hash tables - (Rager) Parallel evaluation o more debugging tools, e.g. see :DOC trace and see :DOC wet (in tomorrow's talk) o diverse tools for querying the logical database (see :DOC history) ============================================================ [end]