Considerable effort has gone into the techniques of extracting executable code from formal specifications and animating them. We 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, we obtain a verified Java interpreter that is sufficiently efficient for running small Java programs. To this end, we present refined implementations for common notions such as the reflexive transitive closure and Russell's definite description operator. From our experience, we distill simple guidelines on how to develop future formalisations with executability in mind. © 2011 Springer-Verlag.
CITATION STYLE
Lochbihler, A., & Bulwahn, L. (2011). Animating the formalised semantics of a Java-like language. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6898 LNCS, pp. 216–232). https://doi.org/10.1007/978-3-642-22863-6_17
Mendeley helps you to discover research relevant for your work.