|
|
|---|
|
|
|
|---|
A longer introduction to ACL2s
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.
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 the ACL2s-faq). 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.
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.