Dracula

The objective of the "Dracula" project is to provide a programming environment for the ACL2 language and theorem prover. ACL2, short for A Computational Logic for Applicative Common Lisp, is a programming language and theorem prover. DrRacket is a graphical programming environment for Racket, Scheme, ACL2, and other programming languages. This page provides instructions for downloading the software, working in Racket's ACL2 language, writing interactive graphical programs, and for reporting bugs.

Keep reading below for installation instructions, and check out the links on the left for tutorials, examples, and bug report instructions.

Dracula has been used to teach a first-year undergraduate logic course at Northeastern University. A report on this course was presented at the ACL2 Workshop in 2007, and can be found here.

Prerequisites:

• You need DrRacket version 5.92 or better for the latest release of Dracula. Download and install from the Racket site.
• You also need ACL2 version 3.1. Download and install from the ACL2 site at UT, Austin.

Installing Dracula:

• Dracula is available as a Racket package. It can be installed using the raco command line utility. On Windows, this utility is in the directory where Racket is installed; on Mac or Unix, it is in the bin subdirectory. To install Dracula using this utility, execute:

  raco pkg install dracula

• Read the Guide. To find it, start Help Desk via DrRacket's Help menu. The section titled "Other Languages in the Racket Environment" will include links to "Dracula: A Guide to ACL2 Theorem Proving in DrRacket" and "Dracula: Reference Manual".

• If the Dracula language or its documentation does not get installed correctly, try running the following command to fix it:

  raco setup

  If that does not work, you can uninstall Dracula using the instructions below and try to reinstall. Alternately, feel free to inquire on the Racket User's mailing list, file a bug report via DrRacket's Help menu, or contact the author.

• Start DrRacket.

• Select ACL2 in the Dracula category as your Language Level.

• You now see a Definitions Window, an Interactions Window, a Run button, and a Stop button (plus a few others). The right side of the screen shows a Proof Summary Window, proof control buttons including Start, Admit, and Undo, and a Proof Output Window.

• To define and edit functions, use the Definitions window.

• To run your program, click on Run. This adds the content of the Definitions Window to DrRacket's "knowledge base". Now you can evaluate expressions in the Interactions Window that refer to the definitions in the Definitions Window.

  You may also copy and paste such expressions into the Definitions Window. DrRacket will then evaluate them next time you click Run.

  You may also enter definitions into the Interactions Window (if you want to test something on the fly). We don't recommend this, but it is not an uncommon practice for Lisp development.

• To prove theorems, click on Start and use the Admit and/or All buttons to send the expressions in the definitions window to ACL2. Admitted expressions will be highlighted green, and rejected expressions will be highlighted red.

• To quit the theorem prover, click Stop (which replaces Start while ACL2 is running). You may now restart ACL2 if desired.

Thanks to Rex Page for the inspiration for this project, Dale Vaillancourt for the initial implementation, and Matthias Felleisen for his constant support. Thanks to Zoe Zhang, Carter Schonwald, and Ken McGrady for their contributions to Dracula. Thanks to J Moore, Matt Kaufmann, Pete Manolios, Ruben Gamboa, and the rest of the ACL2 community for their support and constructive suggestions.