|
|
|---|
|
|
|
|---|
Examples of ACL2 scripts
Beginning users may find these annotated scripts useful. We suggest that you read these in the following order:
Tutorial1-Towers-of-Hanoi Tutorial2-Eights-Problem Tutorial3-Phonebook-Example Tutorial4-Defun-Sk-Example Tutorial5-Miscellaneous-Examples
You can also find useful demos in the community-books directory,
The web page Brief ACL2 Tutorial contains a script that illustrates how it feels to use The Method to prove an unusual list reverse function correct. The screen shots of ACL2's proof output are outdated — in the version shown, ACL2 does not print Key Checkpoints, but the concept of key checkpoint is clear in the discussion and the behavior of the user.
See Polishing Proofs Tutorial for a tutorial on becoming successful at approaching a formalization and proof problem in ACL2. That tutorial, written by Shilpi Goel and Sandip Ray, has two parts: it illustrates how to guide the theorem prover to a successful proof, and it shows how to clean up the proof in order to facilitate maintenance and extension of the resulting book (see books).
The ACL2 Demo Given at TPHOLs 2008 by Matt Kaufmann includes scripts and a gzipped tar file containing the entire contents of the demos.
The sort
equivalence demo is a collection of scripts illustrating both high-level
strategy and lower-level tactics dealing with the functional equivalence of
various list sorting algorithms. Start with the
When you feel you have read enough examples, you might want to try the following very simple example on your own. (See solution-to-simple-example for a solution, after you work on this example.) First define the notion of the ``fringe'' of a tree, where we identify trees simply as cons structures, with atoms at the leaves. For example:
ACL2 !>(fringe '((a . b) c . d)) (A B C D)
Next, define the notion of a ``leaf'' of a tree, i.e., a predicate
(defthm leaf-p-iff-member-fringe (iff (leaf-p atm x) (member-equal atm (fringe x))))