The von Neumannesque ACL2 state object
Note: If you are interested in programming with state, see programming-with-state after reading the information below.
The ACL2 state object is used extensively in programming the ACL2 system, and has been used in other ACL2 programs as well. However, most users, especially those interested in specification and verification (as opposed to programming per se), need not be aware of the role of the state object in ACL2, and will not write functions that use it explicitly. We say more about this point at the end of this documentation topic.
The ACL2 state object is an example of a single-threaded object or stobj. ACL2 allows the user to define new single-threaded objects. Generally, ACL2 may need to access the ACL2 state but should not (cannot) change it except via a certain set of approved functions such as defun and defthm. If you need a state-like object to which you have complete rights, you may want a stobj.
Key to the idea of our
The global table is perhaps the most visible portion of the state
object. Using the interface functions
ACL2 supports several facilities of a truly von Neumannesque state machine
character, including file io and global variables. Logically speaking,
the state is a true list of the 14 components described below. There is a
``current'' state object at the top-level of the ACL2 command loop.
This object is understood to be the value of what would otherwise be the free
Every routine that uses the state facilities (e.g. does io, or calls
a routine that does io), must be passed a ``state object.'' And a
routine must return a state object if the routine modifies the state in any
way. Rigid syntactic rules governing the use of state objects are enforced by
Logically speaking, a state object is a true list whose members are as follows:
Open-input-channels, an alist with keys that are symbols in package "ACL2-INPUT-CHANNEL". The value (cdr) of each pair has the form ((:header type file-name open-time) . elements), where typeis one of :character, :byte, or :objectand elementsis a list of things of the corresponding type, i.e. characters, integers of type (mod 255), or lisp objects in our theory. File-nameis a string. Open-timeis an integer. See io.
Open-output-channels, an alist with keys that are symbols in package "ACL2-OUTPUT-CHANNEL". The value of a pair has the form ((:header type file-name open-time) . current-contents). See io.
T-stack, a list of arbitrary objects accessed and changed by the functions aref-t-stackand aset-t-stack.
32-bit-integer-stack, a list of arbitrary 32-bit-integers accessed and changed by the functions aref-32-bit-integer-stackand aset-32-bit-integer-stack.
Big-clock-entry, an integer, that is used logically to bound the amount of effort spent to evaluate a quoted form.
Idates, a list of dates and times, used to implement the function print-current-idate, which prints the date and time.
Acl2-oracle, a list of objects, used for example to implement the functions that let ACL2 report how much time was used, but inaccessible to the user. See read-ACL2-oracle and also see with-prover-time-limit.
File-clock, an integer that is increased on every file opening and closing, and is used to maintain the consistency of the io primitives.
Readable-files, an alist whose keys have the form (string type time), where string is a file name and timeis an integer. The value associated with such a key is a list of characters, bytes, or objects, according to type. The timefield is used in the following way: when it comes time to open a file for input, we will only look for a file of the specified name and typewhose time field is that of file-clock. This permits us to have a ``probe-file'' aspect to open-file: one can ask for a file, find it does not exist, but come back later and find that it does now exist.
Written-files, an alist whose keys have the form (string type time1 time2), where string is a file name, typeis one of :character, :byteor :object, and time1and time2are integers. Time1and time2correspond to the file-clocktime at which the channel for the file was opened and closed. This field is write-only; the only operation that affects this field is close-output-channel, which conses a new entry on the front.
Writeable-files, an alist whose keys have the form (string type time). To open a file for output, we require that the name, type, and time be on this list.
List-all-package-names-lst, a list of true-listps. Roughly speaking, the car of this list is the list of all package names known to this Common Lisp right now and the cdr of this list is the value of this statevariable after you look at its car. The function, list-all-package-names, which takes the state as an argument, returns the car and cdrs the list (returning a new state too). This essentially gives ACL2 access to what is provided by CLTL's list-all-packages. Defpkg uses this feature to ensure that the about-to-be-created package is new in this lisp. Thus, for example, in akclit is impossible to create the package "COMPILER"with defpkg because it is on the list, while in Lucid that package name is not initially on the list. User-stobj-alist, an alist which associates user-defined single-threaded objects (see stobj) with their values.
We recommend avoiding the use of the state object when writing ACL2 code intended to be used as a formal model of some system, for several reasons. First, the state object is complicated and contains many components that are oriented toward implementation and are likely to be irrelevant to the model in question. Second, there is currently not much support for reasoning about ACL2 functions that manipulate the state object, beyond their logical definitions. Third, the documentation about state is not as complete as one might wish.
User-defined single-threaded objects offer the speed of
Again, if you are interested in programming with state see programming-with-state.