Worm in Dracula

This is an implementation of the well-known Worm video game (aka Snake). The object is to maneuver the worm around the board to eat the food (the green dots). When the worm eats a piece of food, it grows longer by one segment. The game is over when either the worm runs into itself, or the worm attempts to move outside the bounds of the playing area. The distinctive feature of this implementation is that we have verified some interesting safety properties using the theorem prover ACL2.

Requirements

If you wish to play the game, you must have the following three items:

• PLT Scheme version 370 or up.

• Dracula for PLT Scheme.

• The source code for the game.

To Play

• Start DrScheme and select the ACL2 Language Level.

• Open the source code in the editor.

• Click DrScheme's Run button to start the game. Use the arrow keys to control the worm's direction. To quit playing, just close the window.

To Check the Theorems

Be sure you have the requisite software installed (refer to Requirements above).

• Open the Worm source code in DrScheme. Be sure you have selected the ACL2 language level.

• Click Start ACL2 and a console window will pop up. In the DrScheme window, click Admit Next to send the next unprocessed expression to ACL2, or click Admit All to send all the expressions to ACL2. Green highlighting indicates that an expression was admitted, and red highlighting indicates that an expression was rejected. Users that are familiar with reading ACL2's output may do so in the console window if desired.

Detailed Documentation

We have included detailed documentation in the comments of the source code. It is meant to be read in a linear fashion. It covers the structure of the game, necessary parts of the GUI framework, and the theorems that we have proved about the game. If anything is unclear or confusing, please submit a bug report!