Home

A Machine-Checked Model for a Java-Like Language, Virtual Machine, and Compiler

G. Klein and T. Nipkow, A Machine-Checked Model for a Java-Like Language, Virtual Machine, and Compiler, ACM TOPLAS, vol. 28, no. 4, 2006.

We introduce Jinja, a Java-like programming language with a formal semantics designed to exhibit core features of the Java language architecture. Jinja is a compromise between realism of the language and tractability and clarity of the formal semantics. The following aspects are formalised: a big and a small step operational semantics for Jinja and a proof of their equivalence; a type system and a definite initialization analysis; a type safety proof of the small step semantics; a virtual machine (JVM), its operational semantics and its type system; a type safety proof for the JVM; a bytecode verifier, i.e. dataflow analyzer for the JVM; a correctness proof of the bytecode verifiers w.r.t. the type system; a compiler and a proof that it preseves semantics and well-typedness.

The emphasis of this work is not on particular language features but on providing a unified model of the source language, the virtual machine and the compiler. The whole development has been carried out in the theorem prover Isabelle/HOL.

This is a fairly lengthy article (clocking in at 77 pages), in part because it presents a wealth of technical detail. The authors state that the aim of the article "is to demonstrate the state-of-the-art in machine-checked language definitions."

For those who are curious, the Isabelle theories are available in the Archive of Formal Proofs.

By Allan McInnes at 2009-02-12 23:16 | Semantics | other blogs | 8892 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

See also

Subsequent work Jinja with Threads, also in the archive.

By shap at Fri, 2009-02-13 14:19 | login or register to post comments

Java-like language

Does anyone know of a Jinja program, just so that we can get a feel of the language? The document describes it but gives no example.

By Denis Bredelet -jido at Mon, 2009-02-16 15:05 | login or register to post comments

From glancing at the paper

From glancing at the paper it looks just like Java, but without many operators.(trivial to add however). It also is missing the enormous libraries. For loops are also missing. This is based on reading the big-step semantics looking for keywords.
(Edit: I also don't see any floating point. Or classes)

By Watson Ladd at Mon, 2009-02-16 15:44 | login or register to post comments