ACL2s
ACL2s
The ACL2 Sedan theorem prover (ACL2s) is a system based on the ACL2 theorem prover and the Lisp language. ACL2s is an Eclipse plug-in that offers a development environment, supports a number of interaction modes, and a termination analysis engine, and seamlessly combines semi-automated bug-finding techniques with interactive theorem proving.
Overview
ACL2 is a software system made up of a programming language, an extendable first-order logic theory, and an automated theorem prover. ACL2s is an extension of ACL2. Inductive logical theories are supported by ACL2 in order to facilitate automated reasoning, primarily for hardware and software verification. ACL2 is implemented and has input syntax written in Common Lisp.
Powerful capabilities in ACL2s give users additional automation and assistance when defining conjectures and proving theorems. This features automatic Counterexample creation and CCG termination analysis. ACL2s is also "safer" since it builds and enforces abstractions depending on what meaningful interaction with ACL2 is. For instance, in contrast to the standard ACL2 development environment (the command-line theorem prover and Emacs), In ACL2s, pressing Return before finishing a single, well-formed input expression does not transmit any input to ACL2. In contrast to Emacs, if something goes wrong, ACL2s stops automatically delivering input to ACL2.[1].
User Interface
Script Management
In order to communicate with an interactive, extendable theorem prover, one common and natural idiom is script management. The source code editor, often known as the "proof script," essentially keeps track of two "lines": the finished line and the to-do line. These result in three (possibly empty) regions in the following order: the completed region, which holds all information that has been accepted by the theorem prover; the todo region, which holds all information that is currently being processed or that is scheduled to be processed; and the working region, which is for free-form editing. In ACL2s, the editable working zone has no highlight but the to-do region and finished region both have read-only, gray highlighted areas[2].
The todo line may be freely modified by the user, who can then designate how much of his job he wants the theorem prover to handle. The completed line must move with the todo line if the user wants to move the todo line above the completed line's present location. In the theorem prover, this is accomplished by redoing the forms that are no longer in the completed area. If the input's abstract syntax corresponds to the sequence of undone forms, ACL2s also permits immediate redoing of those forms. There are too many problems with line manipulation in a script management interface to list them all here, but ACL2s neatly and effectively solves them[3]
Command Line Arguments
When a user needs to know why ACL2 rejects a certain input form, the script management interface in the source editor is insufficient. In such instances, the session editor displays ACL2's textual output as well as the whole input/output history for that session.[4]. Input can come through the script management interface's todo section, or it can be written straight into the session editor's bottom, making it a command-line interface to the same session. Some ACL2 input, such as queries or stateless function calls, does not make sense from a script management interface, which is why a command line interface is retained. Similarly, "stateful" input belongs in the script management interface so that it may be included in the finished region. Instead of limiting the types of input that may be utilized from the two interfaces, ACL2s copies command-line input that is "stateful" input if and only if it is to the finished area[3]
ACL2s Extensions
CCG Termination Analysis
ACL2 contains improved termination analysis based on "Context Calling Graphs" (or CCGs), which considerably improves ACL2's ability to detect ending function definitions without user intervention. CCG analysis, for example, automatically confirms 98.7 percent of the 10,000 functions terminating when compared to the ACL2 regression suite, which encompasses issues ranging from set theory to processor verification.[5]. This includes 68.2 percent of those that previously required explicit user guidance[3]
Session Modes
ACL2s has numerous "session modes" that configure ACL2 for development at a specific depth of comprehension, similar to "language levels" in DrScheme. This starts with Programming mode, which ignores anything relating to proofs, soundness, or efficient implementation.[6]. Recursion and Induction mode offers proof capabilities without much consideration for constructing cohesive proof rules. ACL2s mode is similar to ACL2, except it includes CCG termination analysis. Compatible mode maintains compatibility with official ACL2 versions[3]
Automatic Counter-Example Generation
Counter Example Generation (Cgen) is a powerful debugging tool that can be used to automatically test and check counterexample formulations. Cgen can be turned off and the number of automatic tests can be adjusted. If on, every function and property passed into ACL2s will undergo automatic counter-example checking.
History
Version 1.2.0.0
1.2.0.0 was released January of 2018 and saw the addition of a TODO feature and support for interactive disproving via fixers in Counter Example Generation. It also dropped support for 32 bit platforms.[1]
References
- ↑ 1.0 1.1 "ACL2s Home page/Documentation". acl2s.ccs.neu.edu. Retrieved 2022-06-27.
- ↑ "Getting Started with ACL2 Programming". www.cs.utexas.edu. Retrieved 2022-06-27.
- ↑ 3.0 3.1 3.2 3.3 Dillinger, Peter C.; Manolios, Panagiotis; Vroon, Daron; Moore, J. Strother (May 2007). "ACL2s: "The ACL2 Sedan"". 29th International Conference on Software Engineering (ICSE'07 Companion): 59–60. doi:10.1109/ICSECOMPANION.2007.14.
- ↑ "Command-line". 2022-06-25. Retrieved 2022-06-25. Unknown parameter
|url-status=ignored (help);|Authors list=missing|1=(help) - ↑ Manolios, Panagiotis; Vroon, Daron (2006). Ball, Thomas; Jones, Robert B., eds. "Termination Analysis with Calling Context Graphs". Computer Aided Verification. Berlin, Heidelberg: Springer: 401–414. doi:10.1007/11817963_36. ISBN 978-3-540-37411-4.
- ↑ "How to Use ACL2s". www.cs.utexas.edu. Retrieved 2022-06-27.
This article "ACL2s" is from Wikipedia. The list of its authors can be seen in its historical and/or the page Edithistory:ACL2s. Articles copied from Draft Namespace on Wikipedia could be seen on the Draft Namespace of Wikipedia and not main one.
