Concurrency: Practice and Experience
Author(s): David von Oheimb
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.
Corresponding Slides and Isabelle sources