The Cooperation Test : a syntax-directed verification method

The cooperation test was originally conceived to capture the proof theoretical analogue of distributed message passing between disjoint processes, as opposed to the interference test, being the proof theoretical analogue of concurrency based on interference by jointly shared variables. Since then the cooperation test has been applied to characterize concurrent communication in Hoare’s Communicating Sequential Processes, Ichbiah’s ADA, and Brinch Hansen’s Distributed Processes, supported by soundness and completeness proofs. An overview is given of the rationale underlying this characterization, culminating in the development of proof systems for monitor based programming languages for concurrency which combine distributed message passing between processes with interference through local variables of a process which are shared between its subprocesses.