1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171
|
<html>
<head><title>STATE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>STATE</h2>the von Neumannesque ACL2 state object
<pre>Major Section: <a href="MISCELLANEOUS.html">MISCELLANEOUS</a>
</pre><p>
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 <i>per se</i>), 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.<p>
The ACL2 state object is an example of a single-threaded object or
<a href="STOBJ.html">stobj</a>. 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 <code><a href="DEFUN.html">defun</a></code> and <code><a href="DEFTHM.html">defthm</a></code>. If you need a state-like object
to which you have complete rights, you may want a <a href="STOBJ.html">stobj</a>.<p>
Key to the idea of our <code>state</code> is the notion of single-threadedness.
For an explanation, see <a href="STOBJ.html">stobj</a>. The upshot of it is that <code>state</code>
is a variable symbol with severe restrictions on its use, so that it
can be passed into only certain functions in certain slots, and must be
returned by those functions that ``modify'' it. Henceforth, we do not
discuss single-threaded objects in general (which the user can introduce
with <code><a href="DEFSTOBJ.html">defstobj</a></code>) but one in particular, namely ACL2's <code>state</code> object.<p>
The <i>global table</i> is perhaps the most visible portion of the state
object. Using the interface functions <code>@</code> and <code>assign</code>, a user
may bind global variables to the results of function evaluations
(much as an Nqthm user exploits the Nqthm utility <code>r-loop</code>).
See <a href="_at_.html">@</a>, and see <a href="ASSIGN.html">assign</a>.
<p>
ACL2 supports several facilities of a truly von Neumannesque state
machine character, including file <a href="IO.html">io</a> 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 <a href="COMMAND.html">command</a> loop. This object is understood to be
the value of what would otherwise be the free variable <code>state</code>
appearing in top-level input. When any <a href="COMMAND.html">command</a> returns a state
object as one of its values, that object becomes the new current
state. But ACL2 provides von Neumann style speed for state
operations by maintaining only one physical (as opposed to logical)
state object. Operations on the state are in fact destructive.
This implementation does not violate the applicative semantics
because we enforce certain draconian syntactic rules regarding the
use of state objects. For example, one cannot ``hold on'' to an old
state, access the components of a state arbitrarily, or ``modify'' a
state object without passing it on to subsequent state-sensitive
functions.<p>
Every routine that uses the state facilities (e.g. does <a href="IO.html">io</a>, or calls
a routine that does <a href="IO.html">io</a>), 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 the function <code>translate</code>, through which all
ACL2 user input first passes. State objects can only be ``held'' in
the formal parameter <code>state</code>, never in any other formal parameter and
never in any structure (excepting a multiple-value return list
field which is always a state object). State objects can only be
accessed with the primitives we specifically permit. Thus, for
example, one cannot ask, in code to be executed, for the length of
<code>state</code> or the <code><a href="CAR.html">car</a></code> of <code>state</code>. In the statement and proof of theorems,
there are no syntactic rules prohibiting arbitrary treatment of
state objects.<p>
Logically speaking, a state object is a true list whose members
are as follows:
<blockquote><p>
<code>Open-input-channels</code>, an alist with keys that are symbols in
package <code>"ACL2-INPUT-CHANNEL"</code>. The value (<code><a href="CDR.html">cdr</a></code>) of each pair has
the form <code>((:header type file-name open-time) . elements)</code>, where
<code>type</code> is one of <code>:character</code>, <code>:byte</code>, or <code>:object</code> and <code>elements</code> is a
list of things of the corresponding <code>type</code>, i.e. characters,
integers of type <code>(mod 255)</code>, or lisp objects in our theory.
<code>File-name</code> is a string. <code>Open-time</code> is an integer. See <a href="IO.html">io</a>.<p>
<code>Open-output-channels</code>, an alist with keys that are symbols in
package <code>"ACL2-OUTPUT-CHANNEL"</code>. The value of a pair has the form
<code>((:header type file-name open-time) . current-contents)</code>.
See <a href="IO.html">io</a>.<p>
<code>Global-table</code>, an alist associating symbols (to be used as ``global
variables'') with values. See <a href="_at_.html">@</a>, and see <a href="ASSIGN.html">assign</a>.<p>
<code>T-stack</code>, a list of arbitrary objects accessed and changed by the
functions <code>aref-t-stack</code> and <code>aset-t-stack</code>.<p>
<code>32-bit-integer-stack</code>, a list of arbitrary 32-bit-integers accessed
and changed by the functions <code>aref-32-bit-integer-stack</code> and
<code>aset-32-bit-integer-stack</code>.<p>
<code>Big-clock-entry</code>, an integer, that is used logically to bound the
amount of effort spent to evaluate a quoted form.<p>
<code>Idates</code>, a list of dates and times, used to implement the function
<code>print-current-idate</code>, which prints the date and time.<p>
<code>Acl2-oracle</code>, 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. Also see <a href="WITH-PROVER-TIME-LIMIT.html">with-prover-time-limit</a>.<p>
<code>File-clock</code>, an integer that is increased on every file opening and
closing, and on each call of <code><a href="SYS-CALL.html">sys-call</a></code>, and is used to maintain the
consistency of the <code><a href="IO.html">io</a></code> primitives.<p>
<code>Readable-files</code>, an alist whose keys have the form
<code>(string type time)</code>, where <code><a href="STRING.html">string</a></code> is a file name and <code>time</code> is
an integer. The value associated with such a key is a list of
characters, bytes, or objects, according to <code>type</code>. The <code>time</code> field
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 <code>type</code>
whose time field is that of <code>file-clock</code>. This permits us to have
a ``probe-file'' aspect to <code>open-file</code>: one can ask for a file,
find it does not exist, but come back later and find that it does
now exist.<p>
<code>Written-files</code>, an alist whose keys have the form
<code>(string type time1 time2)</code>, where <code><a href="STRING.html">string</a></code> is a file name,
<code>type</code> is one of <code>:character</code>, <code>:byte</code> or <code>:object</code>, and
<code>time1</code> and <code>time2</code> are integers. <code>Time1</code> and <code>time2</code>
correspond to the <code>file-clock</code> time at which the channel for the
file was opened and closed. This field is write-only; the only
operation that affects this field is <code>close-output-channel</code>, which
<code><a href="CONS.html">cons</a></code>es a new entry on the front.<p>
<code>Read-files</code>, a list of the form <code>(string type time1 time2)</code>, where
<code><a href="STRING.html">string</a></code> is a file name and <code>time1</code> and <code>time2</code> were the times at which
the file was opened for reading and closed. This field is write
only.<p>
<code>Writeable-files</code>, an alist whose keys have the form
<code>(string type time)</code>. To open a file for output, we require that
the name, type, and time be on this list.<p>
<code>List-all-package-names-lst</code>, a list of <code>true-listps</code>. Roughly
speaking, the <code><a href="CAR.html">car</a></code> of this list is the list of all package names
known to this Common Lisp right now and the <code><a href="CDR.html">cdr</a></code> of this list is
the value of this <code>state</code> variable after you look at its <code><a href="CAR.html">car</a></code>.
The function, <code>list-all-package-names</code>, which takes the state as an
argument, returns the <code><a href="CAR.html">car</a></code> and <code><a href="CDR.html">cdr</a></code>s the list (returning a new state
too). This essentially gives ACL2 access to what is provided by
CLTL's <code>list-all-packages</code>. <code><a href="DEFPKG.html">Defpkg</a></code> uses this feature to ensure that
the about-to-be-created package is new in this lisp. Thus, for
example, in <code>akcl</code> it is impossible to create the package
<code>"COMPILER"</code> with <code><a href="DEFPKG.html">defpkg</a></code> because it is on the list, while in Lucid
that package name is not initially on the list.<p>
<code>User-stobj-alist</code>, an alist which associates user-defined single-threaded
objects (see <a href="STOBJ.html">stobj</a>) with their values.
</blockquote>
<p>
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.<p>
User-defined single-threaded objects offer the speed of <code>state</code> while
giving the user complete access to all the fields. See <a href="STOBJ.html">stobj</a>.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|