A proof system for distributed processes
type: Item
instance of: scholarly article
title: A proof system for distributed processes
zbMATH Open document ID: 0649.68016
DOI: 10.1007/BF02737106
author: A. E. K. Sobel
author: N. Soundararajan
published in: Acta Informatica
publication date: 1988-01-01T00:00:00Z
review text: The paper describes and illustrates a proof technique for partial correctness assertions for the programming language Distributed processes as designed by Brinch Hansen. The specific properties of the system are 1) compositionality: proofs of programs are composed from proofs of its parts, and 2) characterization by external behavior only: the specification of some part involves actions visible on the external interface of that part only; there are no assumption commitment pairs like in the Misra \&\( Chandy\) proposal [\textit{J. Misra} and \textit{K. M. Chandy}, IEEE Trans. Software Eng. SE-7, 417-426 (1981; Zbl 0468.68030)] or a global cooperation test as in Gerth's work [\textit{R. Gerth}, \textit{W. P. de Roever} and \textit{M. Roncken}, Lect. Notes Comput. Sci. 137, 132-163 (1982; Zbl 0493.68019)]. The proof system makes visible the interface between a process and its internal procedures; both the process and its internal procedures are described using invariants where the invariants of the local procedures can invoke the values of the local variables in the process (they are external as seen from these procedures). Although it is stated in the conclusion that the system is sound and complete no proofs for these crucial results are to be found in the paper. The reader is referred to a ph. d. thesis and an unpublished report by the authors. One has to satisfy itself with an exemplary proof of a well known sorting procedure which uses a pipeline of processors.
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68Q55
Mathematics Subject Classification ID: 68N25
Mathematics Subject Classification ID: 68Q65
zbMATH DE Number: 4060689
zbMATH Keywords: partial correctness
zbMATH Keywords: programming language Distributed processes
zbMATH Keywords: compositionality
zbMATH Keywords: proofs of programs
zbMATH Keywords: external behavior
reviewed by: Peter van Emde Boas
MaRDI profile type: Publication
cites work: A Proof System for Communicating Sequential Processes
cites work: Distributed processes
cites work: Guarded commands, nondeterminacy and formal derivation of programs
cites work: Q3956375
cites work: An axiomatic basis for computer programming
cites work: The ``Hoare Logic'' of CSP, and All That
cites work: A proof technique for communicating sequential processes
cites work: Q3681905
full work available at URL: https://doi.org/10.1007/bf02737106
OpenAlex ID: W4250818063
Recommended article: Q3678655
Recommended article: Q3731019
Recommended article: Formal verification of a programming logic for a distributed programming language
Recommended article: Q3350772
Recommended article: Q3678654
Recommended article: Verification of distributed programs using representative interleaving sequences
Recommended article: A survey of verification techniques for parallel programs
Recommended article: Using the causal domain to specify and verify distributed programs
Recommended article: P-A logic - a compositional proof system for distributed programs
description: scientific article; zbMATH DE number 4060689