Compositionality, Concurrency and Partial Correctness. Proof Theories for Networks of Processes, and their Relationship
type: Item
instance of: scholarly article
title: Compositionality, Concurrency and Partial Correctness. Proof Theories for Networks of Processes, and their Relationship
zbMATH Open document ID: 0674.68011
author: Job Zwiers
published in: Lecture Notes in Computer Science
publication date: 1993-01-23T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68N25
Mathematics Subject Classification ID: 68-02
Mathematics Subject Classification ID: 68Q99
Mathematics Subject Classification ID: 68N01
zbMATH DE Number: 42460
zbMATH Keywords: specifying and verifying and reasoning about programs
zbMATH Keywords: proof system
zbMATH Keywords: process
zbMATH Keywords: modular completeness
zbMATH Keywords: adaptation completeness
zbMATH Keywords: Hoare specifications
zbMATH Keywords: invariant specifications
zbMATH Keywords: correctness formulae
zbMATH Keywords: expressiveness
zbMATH Keywords: freeze predicates
zbMATH Keywords: concurrency
zbMATH Keywords: modularity
zbMATH Keywords: proof systems
zbMATH Keywords: soundness
zbMATH Keywords: compositional completeness
reviewed by: Tudor Bălănescu
MaRDI profile type: Publication
description: scientific article; zbMATH DE number 42460