Towards a machine-checked java specification book

Abstract

The semantics of the object-oriented, multi-threaded language Java is informally described in the Java Specification Book [5] where the memory model for concurrent threads is explained abstractly by means of asynchronous events and informal rules relating their occurrences. A formalization has been presented in [3] using certain posets of events (called event spaces) and a structural operational (small-step) semantics. Such an exact formal counterpart of the informal axiomatization of the Specification Book may not only serve as a reference semantics for different, possibly simplified, semantics, but also as a basis for language analysis. In this paper we present a machine-checked version of the formalization using Isabelle/HOL. Some proofs showing the redundancy of axioms in the Java Specification Book are discussed. As usual, by Isa-belle's austerity some tacit assumptions and few minor mistakes were revealed.