Derivation of Distributed Programs in the Theory of Owicki and Gries: An Example

This paper describes the derivation of a program for the propagation of information over a network, with acknowledgement (feedback) when the computation is complete. The derivation is carried out in the theory of Owicki and Gries. The paper therefore illustrates the use of this theory for the derivation, as opposed merely to the verification, of distributed multiprograms. Notable is that the derivation, while calculational in style, is carried out with a minimum of formal machinery, e.g., there is no temporal logic. The derivation also serves as a concrete illustration of program reuse. A theory that is based on a shared variable model of communication is shown to manage the design of distributed multiprograms quite well.