We introduce a Hoare-style calculus for a nearly full subset of sequential Java, which we call Java_light. In particular, we present solutions to challenging features like exception handling, static initialization of classes and dynamic binding of methods.

This axiomatic semantics has been proved sound and complete w.r.t. our operational semantics of Java_light, described in earlier papers. To our knowledge, our Hoare logic is the first one for an object-oriented language that has been proved complete. The proofs also give new insights into the role of type-safety.

All the formalization and proofs have been done with the theorem prover Isabelle/HOL.

This article presents a Hoare-style calculus for a substantial subset of Java Card, which we call Java_light. In particular, the language includes side-effecting expressions, mutual recursion, dynamic method binding, full exception handling, and static class initialization.

The Hoare logic of partial correctness is proved not only sound (w.r.t. our operational semantics of Java_light, described in detail elsewhere) but even complete. It is the first logic for an object-oriented language that is provably complete. The completeness proof uses a refinement of the Most General Formula approach. The proof of soundness gives new insights into the role of type safety. Further by-products of this work are a new general methodology for handling side-effecting expressions and their results, the discovery of the strongest possible rule of consequence, and a flexible Call rule for mutual recursion. We also give a small but non-trivial application example.

All definitions and proofs have been done formally with the interactive theorem prover Isabelle/HOL. This guarantees not only rigorous definitions, but also gives maximal confidence in the results obtained.