A dozen instructions make Java bytecode

Prerun przed Bytecode 2010.

Abstrakt pracy:

  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.