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.
|Published (Last):||16 January 2007|
|PDF File Size:||10.20 Mb|
|ePub File Size:||6.47 Mb|
|Price:||Free* [*Free Regsitration Required]|
— ACL2 Version
The reverse of an empty list is just an empty list:. After we split it up into two parts, 1 and list 2 3 4 5we can reverse the list part to get list 5 4 3 2. We could write some more check-expect style tests, but they can only get us acl22 far.
The intent of this is to let you test cal2 functions in the REPL, even if they aren’t carefully written enough in the way ACL2 expects to be used in: If the automatic admission succeeds, the proof bar turns light green next to the admitted code. If everything has been entered correctly, ACL2 will succeed, and the bar will turn dark green with a checkmarkindicating that the property has been tutroial correct. You need DrRacket version 5. You also need ACL2 version 3.
On Windows, this utility is in the directory where Racket is installed; futorial Mac or Unix, it is in the bin subdirectory. The name of the test is rev-rev-test. You may also enter definitions into the Interactions Window if you want to test something on the fly. When a test fails, it shows you which cases it failed on.
The definitions area is where you write your functions, theorems, and other state-altering expressions. Finally, we have the body: This simply means that the code was executed by ACL2 without any problems.
Download and install from the Racket site. 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. DrRacket will then evaluate them next time you click Run.
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. Running Dracula Start DrRacket.
Once you’ve admitted some code to the ACL2 logic which can take some time for complex functions or theoremsthe proof bar turns green next to the form or forms that were admitted. Ac,2 can see that this makes the test fail. 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.
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. In order to correct this, we need to add a hypothesis to our property: It generates values called xsusing the random-integer-list generator.
One property we can test with DoubleCheck is that reversing a list twice gives you the same list you started with. In order to define a recursive function in ACL2, we need to ac2l about what it would return in a couple of different cases.
First, the ‘3’ has a checkmark with a green background next to it. This automatic admission occurs in: We can automate this process to make sure that rev continues to match our expectations, even if we change or rewrite it.
Aspects of ACL2 User Interaction
We’ll talk more about the proof bar in the next section Definitions occur in an ordered way in the file; if you want to use the function “foo” within the function “bar”, you must put the definition of “foo” above the definition of “bar”. Try admitting your sum function from before. The proof bar handles this for you.
In this case, it fails all cases, but it might help you to diagnose the problem if only some of the cases fail too. To install Dracula using this utility, execute: To run the test, just paste it into the definitions area. 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.
A doublecheck test has three parts: In this case, our test as written will fail. And what we want for the whole list is list 5 4 3 2 1.
Aspects of ACL2 User Interaction
For put-at-end x xswe can use append:. Upgrading To upgrade Dracula, run the following at the command line: You can see what kinds of values this generator returns by typing it in the REPL. This way, ACL2 will know to only concern itself with values that satisfy true-listp — values that are lists. You will probably want to admit these functions to ACL2’s: Acknowledgements Thanks to Rex Page for the inspiration for this project, Dale Vaillancourt for the initial implementation, and Matthias Felleisen for his constant support.
Essentially, the REPL will execute any code you type in the text field on bottom the “prompt” and show the result in the log above. If it fails, it instead turns red, an ‘x’ is shown, and the details pane opens up to show you the error message you received. This page provides instructions for downloading the software, working in Racket’s ACL2 language, writing interactive tutorlal programs, and for reporting bugs.
Guards are restrictions on what values a function will take; in this case, endp xs expects a list, and we gave it tutorual number. It would be even better if we could write a test that will check several types of lists to see that our function does what we want. Try typing some math into the REPL now: Here’s a definition for ‘sum’ that you can either retype or copy and paste: