Compositionality, Concurrency and Partial Correctness. Proof Theories for Networks of Processes, and their Relationship (Q1187626)

This research monograph deals with the specification and compositional verification of parallel programs, in connection with their hierarchical structure. Communicating processes are specified by the language TNP (Theoretical Networks of Processes), a simpler but more powerful variant of DNP (Dynamic Networks of Processes). The proofs of program specifications are intended to be compositional, that is, syntax directed. The first proof systems for parallel programs did not adhere to the syntax directed style. One of the first publications containing a proof rule for parallel programs without reference to the inner structure of the constituent components was by Misra and Chandy. This rule formed the basis for a compositional proof system for the language DNP by Zwiers, de Bruin and de Roever. On this direction, three methods for specifying the observable behavior of communicating processes, and their associated proof systems are considered. The first four chapters deal with the programming language TNP, the assertion language and the mixed terms language. The fifth chapter introduces the three proof systems: the SAT system, the Hoare system and the Invariant system. Their soundness is proven also here. The sixth and seventh chapter addresses the completeness question. The notion of completeness is considered in compositional, modular and adaptation sense. It is shown that the SAT system is complete in all the senses. The Hoare system is compositional complete; it is also adaptation complete if it includes a so called strong adaptation rule. Finally, the compositional completeness of the Invariant system is proved. The text is largely selfcontaining and the proofs are clear. The book is a valuable reference for computer scientist involved in formal semantics of parallel programs.