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
|
This directory contains the definition of one of the more elaborate JVM
models, M5. To get a sense of M5 without understanding anything else, you
might look at the comment at the top of demo.lisp which shows a Java program,
its bytecode, and the M5 counterpart.
Here is a brief summary of the files:
m5.lisp
definition of the M5 machine
utilities.lisp
some handy lemmas when reasoning about M5 programs
demo.lisp
a proof of recursive JVM factorial
idemo.lisp
a proof of iterative JVM factorial
jvm-fact-setup.lisp
the prelude to the proof of recursive factorial, for demo purposes when all
I want to show is the final proof
apprentice-state.lisp
state setting up the Apprentice challenge
apprentice.lisp
the Apprentice Challenge: a growing number of JVM threads competing for a
shared object (not certified with "make" by default; see Makefile)
partial.lisp
inductive invariant approach to partial correctness of three JVM programs
(half, sum, recursive factorial)
perm.lisp
some standard properties of the permutation predicate
isort.lisp
correctness of JVM insertion sort
universal.lisp
a ``universal'' JVM program, proved to compute the value of every numeric
function (!), if one misunderstands how to use ``clock functions'' in the
correctness statement
universal-never-returns.lisp
proof that the universal program does not terminate, (to demonstrate that we
can deal with non-termination proofs) This is complicated by the presence
and creation of threads.
infinite-fair-schedule.lisp
definition of a function that is an infinite fair schedule (irrelevant to M5
except that it takes as input a (finite) schedule and this shows how we
could define a ``fair M5'')
script.lisp
a file that will re-certify all these books
Demo.java
a recursive factorial method written in Java.
Demo.class
the result of running the Sun java compiler:
% javac Demo.java
demo.script
a description of how to give a demo of M5 (a quick display of real
Java and Sun's compiled bytecode, running the bytecode and the M5 model,
proving a correctness theorem)
|
