We will illustrate how to use our software via this short walkthrough. It assumes that you have already installed the Dracula software. If you have not, please refer to the installation instructions.
If you have installed the software, start up DrScheme and read on! Note that clicking on the small images below will open up a full-sized version in a new window.
The first step is to set your language level in DrScheme. Under the Language menu, select Choose Language.... A dialog will pop up. Under the heading ACL2 Languages, choose ACL2 Beginner .... The first image to the right shows the Choose Language... dialog; click on it to see a blown-up version.
(note: this image is already full-sized)
The editing area in the DrScheme window is split into two sections. The top is the Definitions Window, and that is where we edit programs. Type in the definition of the factorial function:
(defun fact (n)
(if (zp n)
1
(* n (fact (1- n)))))Run. 
You may now test your function interactively by typing expressions at the prompt in the bottom half of the DrScheme Window. Try evaluating (fact 10) at the prompt by typing in the expression followed by a return. DrScheme will print out the answer 3628800.
Try making an error in the interactions window. For example, try to evaluate (fact -4). This is an error because the predicate zp only works on natural numbers, and you'll notice that DrScheme prints an error message to that effect. It has also highlighted zp in the definitions window to indicate which call received the invalid arguments.
The Check Syntax button analyzes the code in the definitions window to detect syntactic errors. When the program is error-free, the code is colored to represent the binding-structure. Names whose definitions occur in the program are colored light blue. Names of primitives are colored purple, and unbound names are colored red.
Mousing over light blue names causes an arrow to be drawn from the binding occurrence to the bound occurrence. You can right-click (control-click on a Mac) to pop up a context menu that allows you to tack the arrows in place, to navigate through various occurrences of the name, and to change the name throughout the program (α-conversion).
ACL2's documentation is searchable via DrScheme's Help Desk. Highlight the predicate zp in either the definitions or interactions window, and then press F1. Follow the links to read the documentation on zp or use the text field at the bottom of Help Desk to search for other documentation.
Save your code as fact.lisp and then click the Start ACL2 button. If you have not yet saved your code, DrScheme will prompt you to do so before starting ACL2. Another window will pop up: this is the ACL2 console (pictured at right - click to see full-sized version). The top half shows ACL2 proof trees, and the bottom half shows ACL2's output. The text here is read-only; ACL2 interaction will happen via the buttons in DrScheme. Click back to the DrScheme window, and ignore the console window for now.
Click Admit Next. This sends your definition of factorial to ACL2. ACL2 will attempt to prove that your function terminates on every input, and, if it can, your definition will be highlighted in green. If ACL2 rejects your definition, it will highlight it in red. If ACL2 rejects your code, edit it and try again (see the code above). If the next unhighlighted expression is ill-formed, DrScheme will not send it to ACL2.
In order to keep ACL2 and DrScheme in sync, code that is highlighted green cannot be edited. If you wish to edit a green expression, then click Undo Last until the expression is unhighlighted. You may also click Reset ACL2 to unhighlight all expressions in the definitions window.
Admit All will send all expressions in the definitions window to ACL2. If one of them is rejected, DrScheme will highlight it red and not attempt to admit the remaining expressions.
Now, prove that factorial always produces a positive number. Enter the following code after your definition of factorial:
(defthm fact-produces-positive
(posp (fact n)))
Admit Next to send the theorem to ACL2. The theorem should be highlighted in green. Now, look back at the console window. You'll see in the top it says Q.E.D. just below the theorem's name. When ACL2 fails to prove a conjecture, a proof tree will be displayed here. You can then use the Next Checkpoint and Previous Checkpoint buttons to navigate the proof text. For more information on using checkpoints to debug failed proof attempts, search for "proof-tree" in the ACL2 documentation.
You can provide your programs and proofs to other users as a book. Each book must start with the declaration (in-package "ACL2"). Add this line above your definition of fact. Now click the Save / Certify button. ACL2 will report success: you have certified this file as a book. It is guaranteed to contain only valid programs and theorems.
Now use the book. Close your existing ACL2 session by clicking Stop Prover. Open a new file and enter the following code:
(include-book "fact")
(equal (fact 3) 6)
The first line looks for fact.lisp in the current directory and makes all its definitions available for execution and theorem proving. Save this code in the same directory as fact.lisp and run it. The test case should produce t. If you start ACL2 for this file and click Admit All, ACL2 should accept this file.
If you include an uncertified book, ACL2 will issue a warning but proceed anyway. Proofs based on uncertified books may contain errors, and programs may run without terminating. Always certify books before you use or distribute them.
Use the Stop ACL2 button to shut down your ACL2 session. The console window will prompt you to save the transcript of the ACL2 output. Normally, this will not be needed, so just opt not to save it for now.
Once you do this, the ACL2 interaction buttons will disappear from DrScheme. If you click Start ACL2 again, they will reappear.
Now that you have a handle on the basics of using ACL2 via DrScheme, study the Sample Code to explore more in-depth examples.