Publication


Hoare Logic for NanoJava: Auxiliary Variables, Side Effects and Virtual Methods revisited


Author(s): David von Oheimb, Tobias Nipkow
Year: 2002
Publisher: Springer LNCS 2391
Editor: Lars-Henrik Eriksson, Peter Alexander Lindsay
CR Classification: D.3.1, F.3.2
CR General Terms: Languages, Reliability, Theory, Verification
Abstract: We define NanoJava, a kernel of Java tailored to the investigation of Hoare logics. We then introduce a Hoare logic for this language featuring an elegant new approach for expressing auxiliary variables: by universal quantification on the outer logical level. Furthermore, we give simple means of handling side-effecting expressions and dynamic binding within method calls. The logic is proved sound and (relatively) complete using Isabelle/HOL.
Keywords: Hoare logic, Java, Isabelle/HOL, auxiliary variables, side effects, dynamic binding


Copyright © 2002 Springer-Verlag.
This paper is being published by Springer LNCS.
Preprint version available as compressed Postscript and PDF file.  Slides


BibTeX entry:

@inproceedings{NanoJava-FME02, author = {Oheimb, David von and Tobias Nipkow}, title = {Hoare Logic for {NanoJava}: Auxiliary Variables, Side Effects and Virtual Methods revisited}, booktitle = {Formal Methods -- Getting {IT} Right (FME'02)}, editor = {Lars-Henrik Eriksson and Peter Alexander Lindsay}, conference = {International Symposium of Formal Methods Europe}, year = {2002}, publisher = {Springer}, series = {LNCS}, volume = {2391}, pages = {89--105}, abstract = { We define NanoJava, a kernel of Java tailored to the investigation of Hoare logics. We then introduce a Hoare logic for this language featuring an elegant new approach for expressing auxiliary variables: by universal quantification on the outer logical level. Furthermore, we give simple means of handling side-effecting expressions and dynamic binding within method calls. The logic is proved sound and (relatively) complete using Isabelle/HOL.}, CRClassification = {D.3.1, F.3.2}, CRGenTerms = {Languages, Reliability, Theory, Verification}, note = {\url{http://isabelle.in.tum.de/Bali/papers/NanoJava.html}} }

Isabelle sources