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 among threads.
To reason about multithreaded programs, we introduce in this paper an
assertional proof method for JavaMT (``Multi-Threaded
Java''), a small concurrent sublanguage of Java, covering the
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.
