Correctness Proofs of Communicating Processes: Three Illustrative Examples From the Literature
Marty Ossefort · ACM Transactions on Programming Languages and Systems · 1983
The proof method for networks of processes proposed by Misra and Chandy is demonstrated on three examples from the literature.It is shown that this method is easy to use, preserves process autonomy in the network proof, and conforms naturally to the hierarchical structure of the network.Two very large-scale integration algorithms and a sorting network are presented in Hoare's communicating sequential processes model, specified completely, and formally proved.