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
|
<html>
<head><title>A_Typical_State.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>A Typical State</h2>
<p>
<img src=state-object.gif><p>
Observe that the states in typical models talk about
<pre>
<b>booleans</B> <b>integers</B> <b>vectors</B> <b>records</B> <b>caches</B>
<b>bits</B> <b>symbols</B> <b>arrays</B> <b>stacks</B> <b>files</B>
<b>characters</B> <b>strings</B> <b>sequences</B> <b>tables</B> <b>directories</B>
</pre>
<p>
These objects are <b>discrete</B> rather than <b>continuous</B>;
furthermore they are built incrementally or <b>inductively</B> by
repeatedly using primitive operations to put together smaller pieces.<p>
The functions we need to manipulate these objects do things like
<b>concatenate</B>, <b>reverse</B>, <b>sort</B>, <b>search</B>, <b>count</B>, etc.<p>
<a href="Functions_for_Manipulating_these_Objects.html"><img src=flying.gif></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>
|
