We apply a new method for the development of parallel programs to the problem of finding maximum flows in graphs. The method facilitates concurrent program design by separating the concerns of correctness from those of hardware and implementation. It uses predicate transformer semantics to define a set of basic operators for the specification and verification of programs. From an initial specification program development proceeds by a series of refinement steps, each of which constitutes a strengthening of the specification of the previous refinement. The method is completely formal in the sense that all reasoning steps are performed within predicate calculus. A program is viewed as a mathematical object enjoying certain properties, rather than in terms of its possible executions. We demonstrate the usefulness of the approach by deriving an efficient algorithm for the Maximum Flow Problem in a top-down manner.

We present an extensional semantics for parallel programs based on predicate transformers.We identify the meaning of a parallel program with three concepts: a set of initial conditions, a predicate transformer, called wlt, characterizing progress properties of the program, and a predicate transformer wsafe concerned with safety aspects.For a given program, these predicate transformers are defined in terms of fixpoints of recursive equations.