A Compositional Operational Semantics

Abstract. Besides the features of a class-based object-oriented lan-guage, Java integrates concurrency via its thread-classes, allowing for a multithreaded flow of control. The concurrency model includes shared-variable concurrency via instance variables, coordination via reentrant synchronization monitors, synchronous message passing, and dynamic thread creation. In this paper we propose a class-based compositional operational seman-tics for multithreaded Java which provides a semantic characterization and a formal basis for further semantic investigations involving inheri-tance, subtyping, and full abstraction, and a compositional proof system. From its inception, Java [10] attracted interest from the formal methods community: The widespread use of Java across platforms made the need for formal studies and verification support more urgent, the grown awareness and advances of formal methods for real-life applications and languages made it more acceptable, and last but not least the array of non-trivial language feature