Proving Theorems About Java-Like Byte Code - Correct System Design: Recent Insights and Advances - page 154

function, dtjvm , which is like tjvm . But we modify every semantic function so
that before an instruction is executed we check that the state is acceptable. If
it is not, we set some \non-normal termination" flag in the state and halt. By
dening these defensive semantic functions explicitly in terms of the TJVM's
semantic functions | i.e., the defensive add performs the TJVM's execute-ADD
unless the check fails | it is easy to prove that dtjvm and tjvm return the
\same" results when the dtjvm 's non-normal termination flag is o.
Now suppose someone presents us with a \byte-code verier." We are in a
position to say what property it must have: when veried code is executed by the
dTJVM, the non-normal termination flag remains o. If that property is proved
of the verier and the verier, in turn, approves of a given byte-coded method,
then we can prove the correctness of the method using the full (and simple)
TJVM semantics, instead of having to reason about the dTJVM semantics and
all of its error conditions.
The most problematic aspect of our TJVM may appear to be the fact that
TJVM objects cannot be represented by (the non-circular) objects of applicative
Common Lisp, necessitating the \reference versus instance" debate summarized
here and the explicit provision of the heap in our specication functions. It can-
not be denied that this is a complication. Similar problems have been dealt with
in Flatau's dissertation [7], where pure Lisp is implemented on a von Neumann
machine in a way that is mechanically proved correct. However, we do not think
this can be avoided simply because it reflects the underlying reality of object
oriented programming, in which objects contain a von Neumann sense of state.

7 Acknowledgments

I am especially grateful to Rich Cohen, who patiently explained his ACL2 model
of his \defensive" Java Virtual Machine, upon which my TJVM is modeled. I
am also very grateful to the undergraduates at UT to whom I have taught the
TJVM, as well as my teaching assistant for that course last year, Pete Manolios.

References

1. W. R. Bevier, W. A. Hunt, J S. Moore, and W. D. Young. Special Issue on
System Verication. Journal of Automated Reasoning , 5(4):409{530, Decem-

ber, 1989.
2. R. S. Boyer and J S. Moore. A Computational Logic . Academic Press: New
York, 1979.
3. R. S. Boyer and J S. Moore. Mechanized Formal Reasoning about Programs
and Computing Machines. In R. Vero (ed.), Automated Reasoning and Its
Applications: Essays in Honor of Larry Wos, MIT Press, 1996.
4. R. S. Boyer and J S. Moore. A Computational Logic Handbook, Second Edition ,
Academic Press: London, 1997.
5. B. Brock, M. Kaufmann and J S. Moore, \ACL2 Theorems about Commercial
Microprocessors," in M. Srivas and A. Camilleri (eds.) Proceedings of Formal
Methods in Computer-Aided Design (FMCAD'96) , Springer-Verlag, pp. 275{
293, 1996.