A Formal Specification of Javaℳ Virtual Machine Instructions for Objects, Methods and Subroutines

Abstract

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.