Besides the features of a class-based object-oriented language, Java integrates concurrency via its thread classes. The concurrency model includes shared-variable concurrency via instance variables, coordination via reentrant synchronization monitors, synchronous message passing, and dynamic thread creation. To reason about safety properties of multithreaded Java programs, we introduce an assertional proof method for a multithreaded sublanguage of Java, covering the mentioned concurrency issues as well as the object-based core of Java. The verification method is formulated in terms of proof-outlines, where the assertions are layered into local ones specifying the behavior of a single instance, and global ones taking care of the connections between objects. Prom the annotated program, a translator tool generates a number of verification conditions which are handed over to the interactive theorem prover PVS.
展开▼
