Cooperation Test: A Syntax-Directed Verification Method

摘要

The cooperation test, conceived to capture the proof theoretical analog of a distributed message passing between disjoint processes, as opposed to the interference test, the proof theoretical analog of concurrency based on interference by jointly shared variables, is reviewed. The cooperation test was 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. 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, is given.