Animating the Formalised Semantics of a Java-Like Language
Considerable effort has gone into the techniques of extracting executable code from formal specifications and animating them. The authors show how to apply these techniques to the large JinjaThreads formalisation. It models a substantial subset of multithreaded Java source and bytecode in Isabelle/HOL and focuses on proofs and modularity whereas code generation was of little concern in its design. Employing Isabelle's code generation facilities, they obtain a verified Java interpreter that is sufficiently efficient for running small Java programs. To this end, they present refined implementations for common notions such as the reflexive transitive closure and Russell's definite description operator.