A DECOMPOSITIONAL APPROACH TO THE DESIGN OF PARALLEL PROGRAMS

A methodology for the derivation of parallel implementations from prog ram specifications is developed. The goal of the methodology is to dec ompose a program specification into a collection of module specificati ons via property refinement, such that each module may be implemented independently by a subprogram. The correctness of the implementation i s then deduced from the correctness of the property refinement procedu re and the correctness of the individual subprograms. The control stru ctures such as sequential composition and iteration. The methodology i s developed in the context of the UNITY logic and the UC programming l anguage, and illustrated through the solution of diffusion aggregation in fluid flow simulations.