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 9783540678632

Full text not available from this repository.

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 Isabelle's austerity some tacit assumptions and few minor mistakes were revealed.

Item Type:	Book Section
Keywords:	Computer theory, 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:	24 Sep 2019 12:55
URI:	http://sro.sussex.ac.uk/id/eprint/1434
Google Scholar:	4 Citations

📧 Request an update