Hoare Logic for NanoJava:
Auxiliary Variables, Side Effects and Virtual Methods revisited
David von Oheimb, Tobias Nipkow
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 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.
pdf
BibTeX:
@inproceedings{OheimbN-FME02,
author={Oheimb, David von and Tobias Nipkow},
title={Hoare Logic for {NanoJava}: Auxiliary Variables, Side Effects and
Virtual Methods Revisited},
booktitle={Formal Methods Europe (FME 2002)},
editor={L.-H. Eriksson and P. Lindsay},
publisher=Springer,series=LNCS,
volume=2391,pages={89-105},year=2002}