Publication Workshop

Axiomatic Semantics for Javalight in Isabelle/HOL

Formal Techniques for Java Programs

Author(s): David von Oheimb
Year: 2000
Publisher: Fernuniversität Hagen
Editor: S. Drossopoulou, S. Eisenbach, B. Jacobs, and G.T. Leavens, P. Müller, A. Poetzsch-Heffter
Organization: Technical Report 269, 5/2000, Fernuniversität Hagen
CR Classification: D.2.4, D.3.1, F.3.1
CR General Terms: Languages, Verification, Theory
Keywords: axiomatic semantics, Hoare logic, soundness, relative completeness, dynamic binding, static initialization, Isabelle/HOL
Abstract:We introduce a Hoare-style calculus for a nearly full subset of sequential Java, which we call Java_light. In particular, we present solutions to challenging features like exception handling, static initialization of classes and dynamic binding of methods. This axiomatic semantics has been proved sound and complete w.r.t. our operational semantics of Java_light, described in earlier papers. To our knowledge, our Hoare logic is the first one for an object-oriented language that has been proved complete. The proofs also give new insights into the role of type-safety. All the formalization and proofs have been done with the theorem prover Isabelle/HOL.

Available as [ps.gz], [pdf] and [dvi] file.
Extended version [ps.gz], [pdf] and [dvi] (as contained in TPHOLs 2000 Supplemental Proceedings, OGI Technical Report CSE 00-009)
Workshop slides and TPHOLs'00 posters as gzipped PS files.
Corresponding Isabelle sources

BibTeX entry:

@inproceedings{DvO-ECOOP00, author = {David von Oheimb}, title = {Axiomatic Semantics for {J}ava$^{\ell{}ight}$ in {Isabelle/HOL}}, booktitle = {Formal Techniques for {J}ava Programs}, year = {2000}, publisher = {Fernuniversit{\"at} Hagen}, editor = {Drossopoulou, S. and Eisenbach, S. and Jacobs, B. and Leavens, G. T. and M{\"u}ller, P. and Poetzsch-Heffter, A.}, organization = {Technical Report 269, 5/2000, Fernuniversit{\"at} Hagen}, abstract = {We introduce a Hoare-style calculus for a nearly full subset of sequential Java, which we call Java_light. In particular, we present solutions to challenging features like exception handling, static initialization of classes and dynamic binding of methods. This axiomatic semantics has been proved sound and complete w.r.t. our operational semantics of Java_light, described in earlier papers. To our knowledge, our Hoare logic is the first one for an object-oriented language that has been proved complete. The proofs also give new insights into the role of type-safety. All the formalization and proofs have been done with the theorem prover Isabelle/HOL.}, CRClassification = {D.2.4, D.3.1, F.3.1}, CRGenTerms = {Languages, Verification, Theory}, note = {\url{http://isabelle.in.tum.de/Bali/papers/ECOOP00.html}} }