|
|
|---|
|
|
|
|---|
ATJ tutorial: Background on the Evaluation Semantics of ACL2.
In the context of translating from the ACL2 language to Java or any other programming language, it is important to consider not only ACL2's logical semantics, but also ACL2's evaluation semantics. This tutorial page provides some background on ACL2's evaluation semantics. This tutorial page may be perhaps skipped at first reading, especially if the reader is already deeply familiar with ACL2's evaluation semantics; but some of the concepts described in this page are referenced in subsequent pages, so the reader may need to come back to this page if those concepts are not clear.
ACL2 has a precisely defined logical semantics, expressed in terms of syntax, axioms, and inference rules, similarly to logic textbooks and other theorem provers. This logical semantics applies to logic-mode functions, not program-mode functions. Guards are not part of the logic, but engender proof obligations in the logic when guard verification is attempted.
ACL2 also has a documented evaluation semantics, which could be formalized in terms of syntax, values, states, steps, errors, etc., as is customary for programming languages. This evaluation semantics applies to both logic-mode and program-mode functions. Guards affect the evaluation semantics, based on guard-checking settings. Even non-executable functions (e.g. introduced via defchoose or defun-nx) degenerately have an evaluation semantics, because they do yield error results when called; however, the following discussion focuses on executable functions.
Most logic-mode functions have definitions that specify both their logical and their evaluation semantics: for the former, the definitions are logically conservative axioms; for the latter, the definitions provide ``instructions'' for evaluating calls of the function. For a defined logic-mode function, the relationship between the two semantics is that, roughly speaking, evaluating a call of the function yields, in a finite number of steps, the unique result value that, with the argument values, satisfies the function's defining axiom; the actual relationship is slightly more complicated, as it may involve guard checking.
The primitive functions are in logic mode and have no definitions; they are all built-in. Examples are equal, if, cons, car, and binary-+. Their logical semantics is specified by axioms of the ACL2 logic. Their evaluation semantics is specified by raw Lisp code (under the hood). The relationship between the two semantics is as in the above paragraph, with the slight complication that pkg-witness and pkg-imports yield error results when called on unknown package names. The evaluation of calls of if is non-strict, as is customary.
Most program-mode functions have definitions that specify their evaluation semantics, similarly to the non-primitive logic-mode functions discussed above. Their definitions specify no logical semantics.
The logic-mode functions
listed in the global variable
The program-mode functions
listed in the global variable
Since stobjs are destructively updated,
functions that manipulate stobjs may have side effects as well,
namely the destructive updates.
Because of single-threadedness,
these side effects are invisible
in the end-to-end input/output evaluation of these functions;
however, they may be visible
in some formulations of the evaluation semantics,
such as ones that comprehend interrupts,
for which updating a record field in place involves different steps
than constructing a new record value with a changed field.
The built-in state stobj
is ``linked'' to external entities,
e.g. the file system of the underlying machine.
Thus, functions that manipulate state
may have side effects on these external entities.
For example, princ$ (a member of
The fact that the side effects of the evaluation semantics
are not reflected in the logical semantics
is a design choice
that makes the language more practical for programming
while retaining the ability to prove theorems.
But when generating Java or other code,
these side effects should be taken into consideration:
for instance,
translating hard-error and fmt-to-comment-window
into Java code that returns (a representation of)
Macros are normally expanded
(the expansion being also according to ACL2's evaluation semantics),
and their expansion is then evaluated.
However, the macros listed in the global variable
Previous: Motivation for Generating Java Code from ACL2
Next: Relationship with AIJ