[Prev][Next][Index][Thread]
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
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.
The paper is available under
http://www.informatik.uni-bremen.de/~qian/abs-fsjvm.html
Comments are most welcome.
Zhenyu Qian