Tutorial Description. ACL2 (“A Computational Logic for Applicative Common Lisp”) is both a programming language in which you can model computer systems. ACL2’s logic is constructed on top of a real programming language, Common Lisp, and supports a wide variety of. David Hardin’s current a liation: Ajile Systems. PDF | We describe a tutorial that demonstrates the use of the ACL2 theorem prover. We have three goals: to enable a motivated reader to start.

Author: Tuzilkree Akit
Country: Malta
Language: English (Spanish)
Genre: Marketing
Published (Last): 23 March 2007
Pages: 385
PDF File Size: 9.38 Mb
ePub File Size: 8.21 Mb
ISBN: 625-2-63484-851-8
Downloads: 91613
Price: Free* [*Free Regsitration Required]
Uploader: Yozshura

You instantly see the result, which is 5 4 3 2 1. As you hover over the proof bar, it will show you a preview of what’s going to be done; in particular, if you want to admit an expression, you have to first admit all the expressions above it. The name of the test is rev-rev-test. Try admitting your sum function from before.

You also need ACL2 version 3. On Windows, this utility is in the directory where Racket is installed; on Mac or Unix, tuorial is in the bin subdirectory. When a test fails, it shows you which cases it failed on.

You can see that this makes the test fail. Now, what if xs is not empty? Proof bar The proof bar is the normally white bar to the left of the definitions panel that allows you to view and manipulate the status of ACL2 with respect to your code. There are a couple of things to note at this point. To run the test, just paste it into the definitions area.

First, the ‘3’ has a checkmark with a green background next to it. Keep reading below for installation instructions, and check out the links on the left for tutorials, examples, and bug report instructions. To run your program, click on Run. If everything has been entered correctly, ACL2 will succeed, and the bar will turn dark green with a checkmarkindicating that the property has been proven correct. You need DrRacket version 5. You will probably want to admit these functions to ACL2’s: This way, ACL2 will know to only concern itself with values that satisfy true-listp — values that are lists.


Dracula has been used to teach a first-year undergraduate logic course at Northeastern University. A test passes when the two arguments to check-expect evaluate to the same thing in this case, the list 5 4 3 2 1.

The proof bar handles this for you. The simplest automatic test provided by Tutorail Pad is check-expect. We don’t recommend this, but it is not an uncommon practice for Lisp development.

This means that the function call executed without errors. This test has one generator.

In order to define a recursive function in ACL2, we need to think about what it would return in a couple of different cases. We want to take these parts and assemble a new, reversed list. You can see what kinds of values this generator returns by typing it in the REPL. To install Dracula using this utility, execute: Define reverse reverse xs is a built-in function that takes a list and returns a list with all of the elements in the opposite order.

Aspects of ACL2 User Interaction

Thanks to Rex Page for the inspiration for this project, Dale Adl2 for the initial implementation, and Matthias Felleisen for his constant support. We can automate this ack2 to make sure that rev continues to match our expectations, even if we change or rewrite it. Upgrading To upgrade Dracula, run the following at the command line: This page provides instructions for downloading the software, working in Racket’s ACL2 language, writing interactive graphical programs, and for reporting bugs.


Ttutorial To uninstall Dracula, run the following at the command line: Try typing some math into the REPL now: Test reverse Now that we have a good working definition for reverse, we need to test it to see that it works. It generates values called xsusing the random-integer-list generator. You may also copy and paste such expressions into the Definitions Window.

Proof Pad: Introduction

This has to do with how ACL2 processes events; the ACL2 “world” must be logically consistent after each and every event, so if you used “foo” before defining it, ACL2 might be accepting something that won’t actually work.

Finally, we have the body: Here’s a definition for ‘sum’ that you can either retype or copy and paste: We can just use rev rest xs to reverse the rest of the list, but what do we do with first xs? In this case, it fails all cases, but it might help you to diagnose the problem if only some of the cases fail too. The whole file so far is: DrRacket will then evaluate them next time you click Run.

The intent of this is to let you test your functions in the REPL, even if they aren’t carefully written enough in the way ACL2 expects to be used in: If a single case fails, the test fails.