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.
Keywords Hoare logic - Java - Isabelle/HOL - auxiliary variables - side effects - dynamic binding