Hoare logic for Java in Isabelle/HOL
β
David von Oheimb
π
Article
π
2001
π
John Wiley and Sons
π
English
β 386 KB
## Abstract This article presents a Hoareβstyle calculus for a substantial subset of Java Card, which we call Java$^{\ell ight}$. In particular, the language includes sideβeffecting expressions, mutual recursion, dynamic method binding, full exception handling, and static class initialization. The