Inductive proof outlines for monitors in java

Abstract. The research concerning Java’s semantics and proof theory has mainly focussed on various aspects of sequential sub-languages. Java, however, integrates features of a class-based object-oriented language with the notion of multi-threading, where multiple threads can concur-rently execute exchanging information via shared instance variables. Fur-thermore, each object can act as a monitor to assure mutual exclusion or to coordinate between threads. In this paper we present a sound and relatively complete assertional proof system for Java’s monitor concept, which generates verification condi-tions for a concurrent sublanguage JavaMT of Java. This work extends previous results by incorporating Java’s monitor methods