The ACL2 Sedan Theorem Prover

1.2.0.1 (compatible with ACL2 8.0.0)
The ACL2 Sedan theorem prover (ACL2s) is an Eclipse plug-in that provides a modern integrated development environment, supports several modes of interaction, provides a powerful termination analysis engine, includes a rich support for "types" and seamlessly integrates semi-automated bug-finding methods with interactive theorem proving.

Introduction

ACL2 is a powerful system for integrated modeling, simulation, and inductive reasoning. Under expert control, it has been used to verify some of the most complex theorems to have undergone mechanical verification. In addition to its maturity and stability, these qualifications make it a good platform for learning about industrial-strength theorem proving. Unfortunately, ACL2 has a steep learning curve and with its traditional tool support is analogous to a racecar: it is powerful, but it take expertise to operate properly.

We want to make tool support for the ACL2 platform that is more analogous to a family sedan; hence, the "ACL2s" or "ACL2 Sedan" name. With just a little training, a new user should be able to drive slowly on paved streets without worrying about oversteer, tire temperature, or even engine RPMs.

Pushing aside the analogies, ACL2s includes powerful features that provide users with more automation and support for specifying conjectures and proving theorems. This includes CCG termination analysis and automated Counterexample generation. In addition, ACL2s is "safer" by constructing and enforcing abstractions based on what is meaningful interaction with ACL2. For example, unlike the traditional ACL2 development environment (the command-line theorem prover and Emacs), pressing Return at the command prompt in ACL2s does not send any input to ACL2 until a single, well-formed input expression is completed. Unlike Emacs, ACL2s stops automatically sending input to ACL2 if something fails. Undoing in ACL2s is simple and natural; in other ACL2 environments, however, one has to figure out for oneself the command to undo to a particular point, while watching for critical commands that evade the traditional undo mechanism.

We have implemented our tool as a plugin for the Eclipse development environment (see What is Eclipse?). In addition, the plugin requires some extra functionality from ACL2 that is not included in the main distribution. This functionality is largely hidden from the user and shouldn't alter ACL2's behavior for all practical purposes. To be sure, though, users can certify their work in a clean ACL2 session (see Book development).

ACL2s is not completely mature in its capabilities, but industrial and academic users alike should find it stable enough, intuitive enough, and capable enough to meet their needs. Ideally, the tool will become even more intuitive, self-teaching, etc. in the future.

Get Started

Assuming you have downloaded ACL2s, we will now guide you through the process of creating a new ACL2s/Lisp file, typing definitions into that file, opening up an associated ACL2 session, sending definitions to the session, querying the session, etc.

Unpack..

Simply unpack/unzip (7z) the prepackaged Eclipse install tree that you downloaded. It includes all of ACL2 Sedan and works out of the box. Make sure you unpack it to a path which has no spaces and where you have write permissions (for example /Users/peterd/tools); do this as the user who will be running Eclipse (i.e. avoid sudo).

Note: The ACL2s/eclipse installation is (and should be) separate and disjoint from any other versions of Eclipse you have installed.

Once you have unpacked, navigate into the unpacked folder (remember this path). Now double-click on Eclipse icon or enter ./eclipse in the command line (on Linux); every time you run ACL2s, you need to repeat this step. You may find it useful to create a shortcut to it named "ACL2s" in your Desktop to make this more convenient.

Get Set..

The first time you run Eclipse, it will prompt you for a "workspace" location. This is where Eclipse will save your configuration and layout and is the default location for your ACL2s projects and their associated files. Please choose a fresh workspace (e.g. /Users/yourname/acl2s-workspace) that is different from the workspace you use for Java or other eclipse projects.

Note: ACL2 does not understand network share paths. If the default is on a network share path, you should "Map network drive" in Windows and use a path on that drive.

If you get a welcome window, you can click the "Go to workbench" icon to get to the Eclipse "workbench".

To familiarize yourself with some Eclipse vocabulary and navigating the workbench, we recommend going through the Basic Tutorial section of the Workbench User Guide.

Create a project: Select File | New | Project... and select Project from the group General. Give a name to the project that will contain your ACL2 developments and click Finish.

Open the "ACL2 Development" perspective: Select Window | Open Perspective | ACL2 Development. You could have instead clicked on the icon in the top-right corner. The new perspective will change the layout of your workbench.

Create a new Lisp file for getting the feel of Eclipse and our plugin. Select File | New | ACL2s/Lisp file. The "Directory" should already indicate the project you just created. If not, browse to the project you just created. Pick a file name like "test.lisp" or leave the default. Use "ACL2s" for the session mode and click Finish.

You can now type some ACL2 code in the editor. Type in this definition to get the feel of the auto-indenting, paren-matching, and syntax-based coloring:


; Computes the nth fibonacci number (maybe?)
(defun fib (n)
  (if (and (integerp n) 
           (< n 2))
      (+ (fib (- n 1)) (fib (- n 2)))
    1))

Upon creating the new file, an editor has now opened in the editor area of the workbench. Around the editor area are views, such as the Project Explorer view to the left and Outline view to the right. From their title areas, these can be dragged around, tiled, minimized, etc. You probably also noticed that (defun fib (n) showed up in the Outline view, which you can use to navigate the top-level forms of your file.

In the Project Explorer view, which is a tree view of projects and files, expand your project to reveal a few files:

Open test.lisp.a2s by double-clicking it in the Project Explorer. Alternatively, hit Ctrl+Shift+o (Mac: Command+Shift+o) in the editor for test.lisp. This is the key sequence for switching between corresponding .lisp and .lisp.a2s editors, opening the other if necessary. You should now be in an editor that has a little message "No session running" at the top and won't let you type anything. This editor is read-only when no session is running.

Go...

Start a session for testing our code in test.lisp by clicking the restart session icon in the toolbar.

Note: ACL2s initialization...

After this bookkeeping, you should be able to click the "restart session" icon on the toolbar and have ACL2 start up, resulting in the "ACL2 >" prompt.

Type an "immediate command" for ACL2, such as (* 21 2) in the session editor (.a2s editor). Notice that the editor is read-only except for the part after the last prompt. Hitting Enter (Return) at the end of this editor will submit the typed form to ACL2. Actually, it will only submit syntactically valid commands to ACL2, so if one tries to trick it by hitting Enter after just (* 21, the editor just goes to the next line.

Try submitting other types of input to ACL2. (* 21 2) was classified by the plugin as "VALUE" input, because it's just computation that returns a value. Another example is a "QUERY" such as :pe strip-cars, which prints out information about the current history or "world", in this case the definition of the function "strip-cars". (defun successor (x) (1+ x)) is an "EVENT" because it (potentially) changes the history. See Command Classifications in the guide for more detail. For "EVENT" inputs, ACL2s pops up a dialog asking what to do about the fact that we did something logically relevant from the command line rather than from our source code. Read the dialog and for now choose "Insert".

Try submitting something with an error such as (successor 1 2)--an error because the arity of the successor function we just defined is 1. The red (maroon, I guess) output indicates the command was not successful. ACL2 is back in the state it was in before you submitted the form that caused the error.

Line action

Switch back to the .lisp editor where you will discover the (defun successor (x) (1+ x)) form we submitted in the session editor has been "inserted" above what we had typed previously! Also, that form is "above the line" and read-only. This is part of the intrinsic linkage between somename.lisp and somename.lisp.a2s: the forms "above the line" in the .lisp editor are those used to get the ACL2 session in the .lisp.a2s editor in its current state. To maintain this invariant, we have to do one of two things in the case of executing something history-relevant in the session editor: insert it at the line in the lisp editor or undo it. These are the options the "Relevant input at command line" dialog gave us. Note that "QUERY"s and "VALUE"s do not modify the history, so we don't need to insert those above the line.

Try moving the line past the definition we gave for fib by pressing the "advance todo" button on the toolbar ( or Ctrl+Shift+I on PC or Command+Shift+I on Mac). Watch carefully and you will see the definition for fib flash green. Because it did not turn from green to gray, our definition of fib was rejected by ACL2. Also, if the "Proof Tree" view is open (probably left), it might show some information about a failed termination proof that caused ACL2 to reject the definition.

More Details: Meaning of green and gray highlighting?

So what was the meaning of the flash of green highlighting? Clicking "advance todo" moved the "todo line" from between (defun successor ...) and (defun fib ...) to after (defun fib ...). With at least one form in the "todo region", the session started processing the first (and only) one. If you look at the session output, you see that the attempt to admit our fib function failed. The attempt to prove termination failed. If the next "todo" form fails, the plugin moves the todo line back to the point of the completed line, "cancelling" the todo operations and prompting the user to fix the rejected form.

Fix our fib definition: the previous one had parameters to the < comparison swapped. ACL2 admits this one:


; Computes the nth fibonacci number
(defun fib (n)
  (if (and (integerp n) 
           (< 2 n))
      (+ (fib (- n 1)) (fib (- n 2)))
    1))
Now clicking "advance todo" should result in the definition flashing green while it is in the todo region and turning gray after being accepted.

Source code and Licensing for ACL2s

ACL2s is open-source software, and comes with ABSOLUTELY NO WARRANTY. Copyright 2008 Georgia Tech Research Corporation and Northeastern University.

All parts are available under the Eclipse Public License v1.0 with a GPL exception, and the "acl2s-hooks" and "acl2s-modes" parts are dual-licensed under the GNU General Public License v2.0 as well.

Here is the source code download directory, which contains source code for ACL2, for distributed Common Lisps, and for the ACL2s Eclipse plugin. The "ACL2s hooks" and "ACL2s modes" parts already includes source code, and are available from the update site plugins directory.

Contact info

Email Harsh Raju Chamarthi() and Pete Manolios() with bugs and other questions.

Up to version 0.97, the main developer has been Peter Dillinger, advised by Pete Manolios. Since then, ACL2s is maintained by Harsh Raju Chamarthi, advised by Pete Manolios. CCG termination analysis is by Pete Manolios and Daron Vroon.