A Proof Technique for Communicating Sequential Processes(With an Example)
Gary Marc Levin · eCommons (Cornell University) · 1979
We present proof rules for an extension of the Communicating Sequential Processes proposed by Hoare. The send and receive statements are treated symmetrically, simplifying the rules and allowing send to appear in guards. An example is given to explain the use of the technique. This is an outline of a substantial part of a PhD thesis that is expected to be completed in June 1980.