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
|
``Codewalker'' is a utility for exploring code in any programming language
specified by an ACL2 model to discover certain properties of the code.
Two main facilities are provided by Codewalker: the abstraction of a piece of
code into an ACL2 ``semantic function'' that returns the same machine state,
and the ``projection'' of such a function into another function that computes
the final value of a given state component using only the values of the
relevant initial state components. [Documentation continues as per below.]
CONTENTS:
This directory contains Codewalker (as of June, 2014), the demonstration file
discussed in the Codewalker documentation, and a file demonstrating how
Codewalker might be modified to handle programs that do not always terminate.
The files involved are
README this file
if-tracker.lisp used by simplify-under-hyps
simplify-under-hyps.lisp a utility to simplify a term[*]
terminatricks.lisp Terminatricks
codewalker.lisp Codewalker
m1-version-3.lisp like the distributed M1 book but stobj based
basic-demo.lsp demo of Codewalker on an m1-version-3 program
In addition, there are various files containing simple examples of Codewalker
applied to code in the M1 (``toy JVM'') model:
demo-fact.lisp
demo-fact-count-up.lisp
DOCUMENTATION:
The first 50 pages of codewalker.lisp is just a long comment documenting
Codewalker. The documentation consists of the following sections:
Here are the major sections of this file. We recommend they be read in this
order, by the audiences identified:
[For All Potential Users and Developers:]
A Friendly Introduction to Codewalker
a worked example of def-model-api, def-semantics, and def-projection for
a very simple machine, M1, including examples of output produced by
Codewalker
Reference Guide to Def-Model-API, Def-Semantics, and Def-Projection
a full explanation of the options available
Appendix A: More on Four Similiar Data Structures
:updater-drivers, :constructor-drivers, :state-comps-and-types, and
:var-names. an elaboration of several features; you may or may not be
interested in this material, depending on whether the explanations in
earlier sections suffice for your use
Limitations and Mitigations
what Codewalker cannot handle and a few suggestions that might permit
Codewalker to help you, some, anyway
[For Developers Only:]
Following Some Examples through the Implementation
the same examples as in the Friendly Introduction, but seen from the
``inside;'' examples of internal functions and data structures are
shown to give a sense of how Codewalker works
Guide to the Implementation of Codewalker
descriptions of the books upon which Codewalker is built, the basic data
structures driving Codewalker, and high level sketches of the individual
steps used by def-semantics and def-projection to derive their results;
following these high level descriptions are more detailed descriptions of
each step, including reference to the relevant function names in the Code
The Code for Codewalker
the definitions of all the functions and data structures in Codewalker,
interspersed with comments explaining many low-level details not covered
in the material above; these comments freely use the terminology
introduced above and may be hard to understand if you haven't read the
foregoing material
How to Certify Codewalker
instructions for how to rebuild all the books and replay the the simple
examples discussed in the Friendly Introduction
Search codewalker.lisp for the section headers above to find the beginning of
each section below.
|
