Reus, Bernhard and Hein, Tatjana (2000) Towards a Machine-Checked Java Specification Book. In: Aagaard, Mark and Harrison, John (eds.) Theorem Proving in Higher Order Logics: Proceedings of the 13th International Conference, TPHOLs 2000 Portland, OR, USA. Lecture Notes in Computer Science, 1869 . Springer-Verlag, pp. 480-497. ISBN 9783540678632Full text not available from this repository.
The semantics of the object-oriented, multi-threaded language Java is informally described in the Java Specification Book  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  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 Isabelle's austerity some tacit assumptions and few minor mistakes were revealed.
|Item Type:||Book Section|
|Keywords:||Computer theory ; Theorem proving ; Object oriented programming ; Logical programming ; Formal specification ; Operational semantics ;|
|Schools and Departments:||School of Engineering and Informatics > Informatics|
|Subjects:||Q Science > QA Mathematics > QA0075 Electronic computers. Computer science|
|Depositing User:||Chris Keene|
|Date Deposited:||03 Mar 2008|
|Last Modified:||30 Nov 2012 16:51|
|Google Scholar:||4 Citations|