In this section we summarize some of the features of ACL2. We rely to a large extent on the reader's assumed familiarity with Common Lisp. An ACL2 script is a file of forms which is processed in the order presented. This summary describes some of the forms which can appear in a script.
Defun.
The defun form defines a function. In the example below, the function foo is defined. foo has two arguments, x and y. Assumptions about the arguments are declared (optionally) in the guard. In this example, x and y are declared to be integers (i.e., satisfy the predicate integerp). The guard is evaluated at run time, and causes an error if it is not satisfied. Following the declaration is the function body. A termination proof must be completed before a function is accepted as a logical extension of ACL2.
(defun foo (x y)
(declare (xargs :guard (and (integerp x) (integerp y))))
(* (+ x y) 2))
Guard Verification.
One can avoid the run-time cost of the checking guards by verifying guards with the theorem prover. Verifying the guards of a function f demonstrates that the guards to all functions that f calls are satisfied at the call sites within f.
The ACL2 system can be set to attempt guard proofs automatically whenever a function definition is submitted. This is the mode in which the dJVM model has been processed. This setting can be overridden by an explicit hint of the form
(declare (xargs :verify-guards nil))
in the function definition. In the dJVM model the guard proofs have
been done for all executable portions of the model.The
guards for some functions used to expand macros have not been
verified. But the guards for all the expanded macro calls in
executable functions have been verified.Defthm.
A defthm form proposes a (putative) theorem about previously introduced functions. The mechanical proof checker within ACL2 attempts a proof of the proposed theorem. In this example, we propose the theorem that the function foo returns an even number. The theorem will be named evenp-foo.
(defthm evenp-foo
(implies (and (integerp x)
(integerp y))
(evenp (foo x y))))
The defthm form is also used to introduce rewrite rules for the ACL2 proof system. The example above tells the proof system that the boolean expression (evenp (foo x y)) can be rewritten to t (i.e., true) if x and y are known to be integers. The proof system has a number of other types of rules, including type-prescription rules and linear rules.Type-prescription rules augment the primitive type-reasoning of the ACL2 theorem prover to handle user-defined functions. Linear rules augment the prover's handling of arithmetic proofs. A defthm form may introduce a different class of rule by explicitly identifying the rule class. The example below introduces a type-prescription rule.
(defthm booleanp-evenp
(booleanp (evenp x))
:rule-classes :type-prescription)
The defthm form can also have hints to the theorem
prover to help it complete the proof. If present, these appear after
the :hints keyword after the name and body of the
defthm form.
Case-Match.
case-match is a control-flow and pattern matching construct. The first argument of case-match is a variable. The remaining arguments, called case clauses, are pairs of patterns and expressions. The patterns are attempted in order, and when a match is found, the corresponding expression is evaluated. A pattern match dynamically binds variables from the pattern to values from the form. The pattern \& matches anything, and is used as the default.
In the example below, the first case-clause is evaluated if form is a list of three elements, whose first element is the symbol and. If so, when (foo x y) is evaluated, the variable x will be bound to the second element of form, and y will be bound to the third element. The second clause is evaluated if form is a list of three elements, whose first element is the symbol or. Otherwise, the last clause is evaluated.
(case-match form
(('and x y) (foo x y))
(('or x y) (bar x y))
(& nil))
Deflist.
deflist is a macro that generates a recursive function which recognizes a list, all of whose elements satisfy a given unary predicate. Additionally, it automatically generates a large number of defthm forms that inform the theorem prover of important properties of the new function. The following example introduces a function integer-listp that recognizes a list if integers.The predicate integer-listp is included as part of standard ACL2. Submitting this form to ACL2 would fail because that function name is already in use, and ACL2 normally only allows a function name to be defined once.
(deflist integer-listp (l) integerp)
Defalist.
defalist is a macro that generates a function that recognizes a list, all of whose elements are pairs. The list represents a finite mapping with the first element of each pair being in the domain of the function and the second element being in the range of the function. The domain and range are given by predicates. The macro also generates a large number of defthm forms that inform the theorem prover of important properties of lists accepted by this recognizer.
The following example introduces a function symbol-table-p that recognizes a mapping from symbols to integers. If symtab is a variable whose value is accepted by symbol-table-p, then the value of the expression (domain symtab) is a list satisfying symbol-listp, and the value of (range symtab) is a list satisfying integer-listp.
(defalist symbol-table-p (l)
(symbolp . integerp)
(:options (:domain-type symbol-listp)
(:range-type integer-listp)
The two properties of domain and range mentioned above could be expressed as the following theorem to ACL2:
(defthm domain-and-range-of-symbol-table
(implies (symbol-table-p symtab)
(and (symbol-listp (domain symtab))
(integer-listp (range symtab)))))
The defalist macro generates a number of theorems (including
this one) about the recognizer function and related terms.defstructure is a macro that provides a capability similar to Common Lisp's defstruct. It allows one to define a record structure, including its accessor, constructor and update functions. The following example defines a person record structure consisting of height and weight fields. The fields are required to be numbers. This is enforced by a guard on the constructor function.
(defstructure person
(height (:assert (numberp height)))
(weight (:assert (numberp weight))))
After this form as been introduced to ACL2, the predicate person-p will recognize values that have the required structural form and whose fields satisfy the assertions. The predicate weak-person-p will recognize values that have the required structural form, but does not require the field assertions to be satisfied. This weaker predicate is sometimes useful within the ACL2 proof system, because it is easier to prove than the stronger predicate person-p.
The example above will also generate the following functions.
| (make-person :height h :weight w) | construct a person structure |
| (person-height p) | access the height field of a person p |
| Sometimes called an accessor or getter | |
| function. | |
| (person-weight p) | access the weight field of p |
| (update-person p :weight new-wgt) | ``update'' the weight field of p |
| (set-person-weight new-wgt p) | ``update'' the weight field of p |
| The existing structure is not altered. | |
| A new structure is returned. | |
| Sometimes called a setter function. | |
| (person-p p) | a predicate that recognizes a person |
| structure, including the assertions and type | |
| constraints on the fields | |
| This is called the strong recognizer. | |
| (weak-person-p p) | a predicate that recognizes a person |
| structure without regard for the assertions | |
| and type constaints on the fields. | |
| This is called the weak recognizer. | |
The defstructure macro has a number of other options. We will briefly describe the options used in the dJVM model.
The defstructure macro accepts a number of options that affect how the structure is defined in ACL2.
:options ... :guards :options (:verify-guards t) :keyword-constructor
:assert identifies an assertion about the value of the field. This assertion is checked by the strong structure recognizer.
:rewrite indicates that a rewrite rule should be generated from this assertion. This is the default. It must be specified if there is a separate type-prescription assertion.
:type-prescription indicates that a type-prescription lemma should be generated from this assertion. Type-prescription rules are one of the classes of rules in the ACL2 theorem prover, and provide additional information about the field value that can be used by the theorem prover.
:struct identifies a structural assertion about the value of the field. This assertion is typically the weak structure recognizer corresponding to the assertion given for the field.
:default provides a default value if none is specified in a constructor expression.
:read-only indicates that no ``setter'' function should be generated.
Here's an example taken from page [instance] containing these options.
(defstructure instance
(class (:assert (tv-ref-p class) :rewrite))
(data (:assert (instance-data-p data) :rewrite
(:type-prescription (true-listp data))))
(lock (:assert (null lock) :rewrite)
(:default nil))
(loader (:assert (or (tv-ref-p loader)
(null loader)))
(:default nil)
:read-only)
(fields (:assert (field-listp fields) :rewrite
(:type-prescription (true-listp fields)))
(:struct (weak-field-listp fields)))
(methods (:assert (java-method-listp methods) :rewrite
(:type-prescription (true-listp methods)))
(:struct (weak-java-method-listp methods)))
(:options :guards
(:verify-guards t)
(:keyword-constructor make-an-instance)
))
Observe.
Often during the definition we expect our functions to satisfy some simple properties. For example, that if we alter a field in an object and then immediately fetch that field, we get the altered value. We can use the observe form to state such a property and request that the ACL2 theorem prover verify when it processes the model. This is a way of checking that the model does not violate our expectations. For example
(observe state-2790
(implies (heap-p heap)
(naturalp-listp (domain heap))))
is the statement that if heap is a heap (i.e., satisfies the
predicate heap-p), then it is a mapping whose domain is
natural numbers. Observe is a macro that expands into a
special use of defthm.
The book alist-defthms includes theorems about bind and bound?. They will be useful as we prove theorems about new states with new bindings, produced either by binding new values to local variables or creating new instances in the heap (and associating them with heap addresses).
Other things to explain about ACL2: