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:
<![CDATA[
@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