Stepwise Derivation of a Parallel Matrix Multiplication Algorithm

A standard multiplication algorithm for square matrices is transformed into a distributed algorithm. Every transformation step is verified within the refinement calculus. Some high-level rules of refinement that are used in the derivation are proved. 1 Introduction This report is a case study, intended to show how the refinement calculus, combined with the action system formalism gives a powerful and uniform method for constructing parallel and distributed algorithms by stepwise refinement. The refinement calculus is a formalization of the stepwise refinement approach to program construction. The refinement calculus, based on the weakest precondition technique of [Dijkstra76], was first described in [Back78, Back80] and has been further elaborated in [Back87, Back88a, Back88b, MoRoGa88, Morris87]. A statement S is said to be (correctly) refined by a statement S', denoted S S 0 , if 8 P; Q:(P [S]Q ) P [S 0 ]Q) where P [S]Q stands for the total correctness of S w.r.t. precondition..