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.


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

To Play

To Check the Theorems

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

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!