A proof system for distributed processes (Q1106014)

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.