Book Chapter

Machine-checking the Java Specification: Proving Type-Safety

Formal Syntax and Semantics of Java

Author(s): David von Oheimb and Tobias Nipkow
Year: 1999
Publisher: Springer
Editor: Jim Alves-Foss
CR Classification: D.3.1, F.3.2
CR General Terms: Languages, Security, Verification
Keywords: Java, Semantics, Theorem Proving, Type-Safety, Isabelle
Abstract: In this article we present Bali, the formalization of a large (hitherto sequential) sublanguage of Java. We give its abstract syntax, type system, well-formedness conditions, and an operational evaluation semantics. Based on these definitions, we can express soundness of the type system, an important design goal claimed to be reached by the designers of Java, and prove that Bali is indeed type-safe.
All definitions and proofs have been done formally in the theorem prover Isabelle/HOL. Thus this article demonstrates that machine-checking the design of non-trivial programming languages has become a reality.

Preprint version available as gzipped PS file and PDF file.
A roughly corresponding formalization as DVI or PS file (with graphical symbols) and as html pages (ASCII version)

A PDF version should be available from LNCS Online.
See also the Springer LNCS 1523 entry.

BibTeX Entry:

@incollection{Oheimb-Nipkow-Java-LNCS, author = {Oheimb, David von and Nipkow, Tobias}, title = {Machine-checking the {J}ava Specification: Proving Type-Safety}, booktitle = {Formal Syntax and Semantics of {J}ava}, editor = {Jim Alves-Foss}, note = {\url{http://isabelle.in.tum.de/Bali/papers/Springer98.html}}, publisher = {Springer}, series = {LNCS}, volume = {1523}, pages = {119--156}, year = {1999}, abstract = {In this article we present Bali, the formalization of a large (hitherto sequential) sublanguage of Java. We give its abstract syntax, type system, well-formedness conditions, and an operational evaluation semantics. Based on these definitions, we can express soundness of the type system, an important design goal claimed to be reached by the designers of Java, and prove that Bali is indeed type-safe. All definitions and proofs have been done formally in the theorem prover Isabelle/HOL. Thus this article demonstrates that machine-checking the design of non-trivial programming languages has become a reality.}, CRClassification = {D.3.1, F.3.2}, CRGenTerms = {Languages, Security, Verification} }