(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

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.