Extended naming conventions for communicating processes

摘要

We present two extensions of Communicating Sequential Processes [HO78]: computed communication targets and unspecified communication targets, as well as corresponding extensions to the system of cooperating proofs [AFR80] for verifying distributed programs. These extensions are important for the natural expressibility of many distributed programs. Examples of the use of these extensions are discussed and verified.