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

Proving Theorems About Java-Like Byte Code

J Strother Moore

Department of Computer Sciences
University of Texas at Austin
Austin, Texas 78712 USA
[e-mail] ,
WWW home page: http://www.cs.utexas.edu/users/moore

Abstract. We describe a formalization of an abstract machine very sim-
ilar to the Java Virtual Machine but far simpler. We develop techniques
for specifying the properties of classes and methods for this machine. We
develop techniques for mechanically proving theorems about classes and
methods. We discuss two such proofs, that of a static method implement-
ing the factorial function and of an instance method that destructively
manipulates objects in a way that takes advantage of inheritance. We
conclude with a brief discussion of the advantages and disadvantages of
this approach. The formalization and proofs are done with the ACL2
theorem proving system.

1 Specication of the TJVM

The Java Virtual Machine (JVM) [10] is a stack-based, object-oriented, type-safe
byte-code interpreter on which compiled Java programs are executed.
We develop a simplied JVM for the purpose of exploring verication is-
sues related to proofs about object-oriented byte code. We refer to our machine
as a \toy JVM" or \TJVM." Because we are interested in formal, mechani-
cally checked proofs, we formalize the TJVM in a formal, mechanized logic,
namely ACL2: A Computational Logic for Applicative Common Lisp. The tra-
dition of formalizing machines in ACL2, and its predecessor, Boyer and Moore's
Nqthm, is well established [1,14,11,3,5] and we follow in those well-trodden foot-
steps. Indeed, our TJVM is just a simplication of Rich Cohen's \defensive
JVM," [6], which was formalized at Computational Logic, Inc., in the standard
ACL2/Nqthm style. That style employs an operational semantics, in which the
state of the machine is represented as a Lisp object. An interpreter for the ma-
chine's programming language is dened as a Lisp function. The main purpose
of this paper is to illustrate how those established techniques can be applied in
an object-oriented setting.
This paper provides a brief sketch of our TJVM. The details may be obtained
at http://www.cs.utexas.edu/users/moore/publications/tjvm/index.html.
The state of the TJVM is a triple consisting of a call stack of \frames," a
heap ,anda class table .A frame contains four elds, a program counter , a variable
binding environment called the locals of the frame, an operand stack ,andthe