A Formal Specification of Java(tm) Virtual Machine Instructions
In this paper we formally specify a large subset of Java Virtual Machine
instructions based on the descriptions in the Java Virtual Machine
Specification by Lindholm and Yellin, in the Java Specification by
Gosling, Joy and Steele, and based on the behaviors of some test programs
on Sun's implementation of the Java Virtual Machine. The formal specification
describes the runtime behaviors of the instructions in related memory areas as
(runtime) state transitions and most structural constraints on instructions
as a compile-time (or link-time) type inference system. The latter part
corresponds to a core of the Bytecode Verifier and resembles dataflow analysis
and abstract interpretation. We prove properties based on the formal
specification. In particular, we prove that if the type inference system can
derive certain compile-time (or link-time) types for a program, then the
runtime data of the program will be type-correct with respect to these types
in a certain sense. Indeed, our formal specification clarifies some ambiguities
and incompleteness and removes some (in our view) unnecessary restrictions
in the description of the (informal) Java Virtual Machine Specification.
Revision history:
First draft: September 9, 1997
Revision: October 4, 1997
Revision: October 22, 1997
Revision: November 25, 1997
I am writing a new version now. If you are interested in obtaining a copy,
please send me a message.
I will inform you know when the new revision is available.
A short version is currently available as
PS file or DVI version.