CoJaq: a hierarchical view on the Java bytecode formalised in Coq
Patryk Czarnik, Jacek Chrza̧szcz, Aleksy Schubert · 2013
One of the biggest obstacles in the formalisation of the Java bytecode is that the language consists of around 200 instructions. However, a rigorous handling of metatheoretic properties of a programming language 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 a design of formalisation that provides a concise set of abstract, generic instructions that can be specialised to obtain any particular bytecode instruction. In this way one can work with a manageable set of instructions to prove general facts about the Java bytecode, but at the same time all the bytecode instructions are available to enable direct verification of actual bytecode programs. A considerable part of the design has been realised in Coq.