Formal Syntax and Semantics of Java
Author(s): David von Oheimb and Tobias Nipkow
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.
Copyright © 1999 Springer-Verlag
Preprint version available as
gzipped PS file and
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
See also the Springer LNCS 1523 entry.