Formal Techniques for Java Programs
Author(s): David von Oheimb
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
Note: ECOOP2000 Workshop proceedings available from http://www.informatik.fernuni-hagen.de/pi5/publications.html
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.
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