File: Running_Models.html

package info (click to toggle)
acl2 3.1-1
  • links: PTS
  • area: main
  • in suites: etch, etch-m68k
  • size: 36,712 kB
  • ctags: 38,396
  • sloc: lisp: 464,023; makefile: 5,470; sh: 86; csh: 47; cpp: 25; ansic: 22
file content (38 lines) | stat: -rw-r--r-- 1,158 bytes parent folder | download 
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
 
<html>
<head><title>Running_Models.html  --  ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>Running Models</h2>
<p>
Suppose the machine being modeled is some kind of arithmetic unit.
Suppose the model can be initialized so as to <b>multiply</B> <b>x</B> times
<b>y</B> and leave the answer in <b>z</B>.  Then if we initialize <b>s</B> to
<b>multiply</B> with <b>x=5</B> and <b>y=7</B> and run the machine long enough, we can
read the answer <b>35</B> in the final state.<p>



<img src=computing-machine-5x7.gif><p>

<p>

Because ACL2 is a programming language, our
model can be <b>run</B> or <b>executed</B>.<p>

If you defined the model in ACL2 and then typed<p>


<pre>
&gt; (lookup 'z (mc (s 'mult 5 7) 29))
</pre>
<p>

then ACL2 would compute 35.  You can <b>emulate</B> or <b>test</B> the
model of your machine.<p>

This is <b>obvious</B> because ACL2 is Common Lisp; and Common Lisp is a
<b>programming language</B>.<p>

<a href="Symbolic_Execution_of_Models.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>