A proof system for distributed processes

DOI10.1007/BF02737106MaRDI QIDQ1106014zbMATH OpenOpenAlexFDO

Authors A. E. K. Sobel, N. Soundararajan

Publication date 1988

Published in Acta Informatica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf02737106

zbMATH Keywords

compositionalityexternal behaviorpartial correctnessprogramming language Distributed processesproofs of programs

Mathematics Subject Classification ID

Theory of operating systems (68N25) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

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.

Recommendations

• scientific article; zbMATH DE number 3900140
• scientific article; zbMATH DE number 3963180
• Formal verification of a programming logic for a distributed programming language
• scientific article; zbMATH DE number 4201637
• scientific article; zbMATH DE number 3900139
• Verification of distributed programs using representative interleaving sequences
• A survey of verification techniques for parallel programs
• Using the causal domain to specify and verify distributed programs
• P-A logic - a compositional proof system for distributed programs

Cites work

• A Proof System for Communicating Sequential Processes
• A proof technique for communicating sequential processes
• An axiomatic basis for computer programming
• Distributed processes
• Guarded commands, nondeterminacy and formal derivation of programs
• scientific article; zbMATH DE number 3903940 (Why is no real title available?)
• scientific article; zbMATH DE number 3776836 (Why is no real title available?)
• The ``Hoare Logic of CSP, and All That

Cited in

(6)

• A trace-based compositional proof theory for fault tolerant distributed systems
• scientific article; zbMATH DE number 3900139 (Why is no real title available?)
• scientific article; zbMATH DE number 3900140 (Why is no real title available?)
• scientific article; zbMATH DE number 3963180 (Why is no real title available?)
• A compositional proof system for distributed programs
• P-A logic - a compositional proof system for distributed programs

This page was built for publication: A proof system for distributed processes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1106014)