Besides the features of a class-based object-oriented language,
Java integrates concurrency via its thread-classes, allowing for a
multithreaded flow of control. The concurrency model offers
coordination via lock-synchronization, and
communication by synchronous message passing, including re-entrant method calls, and by instance variables shared amongthreads.
To reason about multithreaded programs, we introduce in this paper an assertional proof method for Java MT (“Multi-Threaded Java”), a small concurrent sublanguage of Java, coveringthe mentioned concurrency issues as well as the object-based core of Java, i.e., object creation, side effects, and aliasing, but leaving aside inheritance and subtyping.