Systematic development of an SPMD implementation schema for mutually recursive divide-and-conquer specifications

An SPMD parallel implementation schema for divide-and-conquer specifications as proposed and derived by formal refinement (transformation) of the specification. The specification is in the form of a mutually recursive functional definition. In a first phase, a parallel functional program schema is constructed which consists of a communication tree and a functional program that is shared by all nodes of the tree. The fact that this phase proceeds by semantics-preserving transformations in the Bird-Meertens formalism of higher-order functions guarantees the correctness of the resulting functional implementation. A second phase yields an imperative distributed SPMD implementation of this schema. The derivation process is illustrated with an example: a two-dimensional numerical integration algorithm