A structured approach for developing concurrent programs in Java']Java

A systematic and formal approach to develop concurrent programs is presented. This approach has many advantages. First, this is a formal approach that enables verification of programs being developed. Second, the most important activity in the programming process lies at a high level, namely, specifying global invariants. Once an appropriate global invariant is specified, much of the rest of the process is mechanical. Furthermore, global invariants and coarse-grained solutions are platform independent, thus, if the platform is switched from a semaphore-based to a monitor-based system, the existing coarse-grained solution to a monitor-based fine-grained program should only be translated.