A Dozen Instructions Make Java Bytecode

One of the biggest obstacles in the formalisation of the Java bytecode is that the language consists of 200 instructions. However, a rigorous handling of a programming language in the context of program verification and error detection requires a formalism which is compact in size. Therefore, the actual Java bytecode instruction set is never used in the context. Instead, the existing formalisations usually cover a ‘representative’ set of instructions. This paper describes how to reduce the number of instructions in a systematic and rigorous way into a manageable set of more general operations that cover the full functionality of the Java bytecode. The factorisation of the instruction set is based on the use of the runtime structures such as operand stack, heap etc. This is achieved by presentation of a formal semantics for the Java Virtual Machine.