Article

Hoare Logic for Java in Isabelle/HOL

Concurrency: Practice and Experience

Author(s): David von Oheimb
Year: 2001
Publisher: Wiley
Editor: Susan Eisenbach and Gary T. Leavens
CR Classification: D.2.4, D.3.1, F.3.1
CR General Terms: Languages, Verification, Theory
Keywords: Hoare logic, axiomatic semantics, Java, Isabelle/HOL, verification, soundness, completeness, auxiliary variables, side effects, mutual recursion, dynamic binding, exception handling, type safety
Abstract: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.

Prepring version
Corresponding Slides and Isabelle sources

BibTeX entry:

@article{DvO-CPE01, author = {David von Oheimb}, title = {Hoare Logic for {J}ava in {Isabelle/HOL}}, journal = {Concurrency and Computation: Practice and Experience}, editor = {Eisenbach, S. and Leavens, G. T.}, year = {2001}, volume = 13, number = 13, pages = {1173--1214}, abstract = { 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.}, CRClassification = {D.2.4, D.3.1, F.3.1}, CRGenTerms = {Languages, Verification, Theory}, note = {\url{http://isabelle.in.tum.de/Bali/papers/CPE01.html}} }