Dynamic semantics of Java bytecode

摘要

We give a formal specification of the dynamic semantics of Java bytecode, in the form of an operational semantics for the Java Virtual machine (JVM). For each JVM instruction we give a rule describing the instruction's effect on the machine state and the conditions under which the instruction will execute without error. This paper outlines the formalization of the JVM machine state and illustrates our approach for a few select JVM instructions. Our full specification, covering the entire JVM instruction set except for synchronization instructions, is available in the work of Bertelsen (Semantics of Java byte code, Technical Report, Department of Mathematics and Physics, Royal Veterinary and Agricultural University, Copenhagen, Denmark, April 1997).