(defthm goldbach ...)

Sample Code

Dracula provides Teachpacks that allow you to write interactive graphical programs with low cognitive overhead. Here we provide sample code to illustrate how to use the Teachpacks. These examples are listed in order of increasing complexity.

Also, please be sure to go through the ACL2 Tours put together by the ACL2 developers!

Matrix Transposition

This is a short non-GUI example that shows how to prove the correctness of matrix transposition. We represent matrices with association lists, and we prove that the element in position (i,j) of a matrix M is at position (j,i) in (transpose M), for all (i,j).

Download Code: matrix-transpose.lisp

Responding to Key Events

This small program illustrates how to use our GUI framework to respond to key events.

Download Code: keypress-gui.lisp

Writing ACL2 books in Dracula

Dracula now gives programmers the ability to build and use books: reusable libraries of ACL2 proofs/programs.

The file lc.lisp demonstrates a simple book: it defines a datatype representing lambda calculus terms. Download this file, open it in Dracula, start ACL2, and press the Save / Certify button. Dracula will report success: the file is certified, guaranteeing it contains only valid programs and theorems.

The file eval.lisp imports the definitions from lc.lisp and defines a substitution program. It proves a simple theorem about substitution and runs some test cases. Download this file in the same folder as lc.lisp and open it in Dracula. Run it; all test cases will run and produce T. Start ACL2 and click Admit All; all forms will be accepted. Both Dracula and ACL2 successfully import the lc.lisp book.

Note that Save / Certify will report failure for eval.lisp: this file is not valid as a book. It does not start with an IN-PACKAGE declaration and it contains top-level expressions. Not all valid ACL2 programs are valid books.

Always remember to certify your ACL2 books. ACL2 will accept an uncertified book blindly but issue a warning; any proofs based on uncertified books may contain errors.

Download Code:

• lc.lisp
• eval.lisp

Worm Game

This is a full implementation of the classic Worm game. You control the worm with the arrow keys, and try to move around the board to eat the food. The worm grows by one segment each time it eats, and the goal is not to crash into the tail or the walls.

We prove an interesting safety property about the game: the function that updates the worm's position at each clock tick preserves the well-formedness of the worm. This involves several lemmas and a bit of numerical reasoning. This code is written as an extended tutorial.

Download Code: See the Worm Game page to download. You will also find instructions on how to play, to verify the theorems, and to learn how the program works.