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.

ps pdf


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},