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.