A formal spec of JVM instructions

I am very glad to announce the availability of a draft paper on
formally specifying a subset of JVM instructions:

Title: 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 

The paper is available under


Comments are most welcome.

Zhenyu Qian