@inproceedings{1a1f3318282840c780898afe46707944,
title = "Hoare logic for NanoJava: Auxiliary variables, side effects, and virtual methods revisited",
abstract = "We define NanoJava, a kernel of Java tailored to the investigation of Hoare logics. We then introduce a Hoare logic for this language featuringan elegant approach for expressingauxiliary variables: by universal quantification on the outer logical level. Furthermore, we give simple means of handlingside-effectingexpressions and dynamic bindingwithin method calls. The logic is proved sound and (relatively) complete usingIsab elle/HOL.",
keywords = "Auxiliary variables, Dynamic binding, Hoare logic, Isabelle/HOL, Java, Side effects",
author = "\{von Oheimb\}, David and Tobias Nipkow",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2002.; 11th International Symposium of Formal Methods Europe, FME 2002 ; Conference date: 22-07-2002 Through 24-07-2002",
year = "2002",
doi = "10.1007/3-540-45614-7\_6",
language = "English",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "89--105",
editor = "Lars-Henrik Eriksson and Lindsay, \{Peter Alexander\}",
booktitle = "FME 2002",
}