Abstract
The semantics of communication in a distributed computing environment without shared objects are investigated from the viewpoint of modularity and hierarchical system structure. Communicating Sequential Processes (CSP), Hoare's language for parallel programming, is modified and expanded to support process modularity and hierarchical structure using a port construction. A formal axiomatic 'verification methodology for partial correctness is developed that extends the Hoare axiomatic proof methodology for sequential (nonparallel) programs to CSP-like programs, without resort to global invariants. Hierarchical structure and modularity are fully supported within the proof system. Processes are verified against an abstract entity, the interface, thereby achieving a formal notion of process specification and plug-compatibility. Alongside maintenance to a system is maintenance to its correctness proof, the two evolving side by side in an isomorphic fashion. The formalism is broadened further to include shared ports by the introduction of a universal assertion termed Kirchhoff's Law. Several examples are provided that demonstrate the methodology, including a modular proof of the generic single-entry, multiple-user CSP subroutine process.