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:
- .project - a file used by Eclipse to store project-specific
settings.
- test.lisp or whatever you called it. This will contain ACL2
code your write.
- test.lisp.a2s - a file created automatically when you opened
test.lisp. This file will store the history of ACL2 sessions
you open to develop test.lisp.
Open test.lisp.a2s by double-clicking it in the
Project Explorer. Alternatively, hit Ctrl+Shift+o
(Mac: 
+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
icon in the toolbar.
First-time ACL2s initialization process
The first time you start a session, there is some
bookkeeping that ACL2s must take care of. This will
happen automatically (except for a couple confirmation
dialogs), but the process could take several minutes
(5-10).
First, the ACL2 Image for Eclipse will need to fix .cert
files for the absolute path of Eclipse on your computer. If
you move Eclipse, this step will automatically be repeated. Be
patient and let it finish this one-time bookkeeping task, it
might take around 5 minutes.
Second, the ACL2s system books, our visible and invisible
extensions to ACL2, need to be certified and compiled by ACL2.
This step could be required again if you change your ACL2
version or when you update ACL2s to a new version.
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
+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.
The plugin models two "lines" in a .lisp file: the "completed
line" and the "todo line". These "lines" are only visible as the
boundary between regions with different highlighting. The
"completed line" is at the last point of gray (or blue)
highlighting. The "todo line" is at the last point of any
highlighting: gray, blue or green.
Above the "completed line" is the (potentially empty) "completed
region," which has forms that ACL2 has--get this--completed.
Between the two lines are forms that we want ACL2 to work on
completing (hence "todo"). This (potentially empty) region, the
"todo region", has green highlighting. We can call the rest of
the buffer the "working region", which is the freely editable
part.
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.
) and Pete Manolios(
) with bugs and other questions.