Algorithm design and parallel program development through formal specifications

The authors describe two components of the Kestrel interactive development system (KIDS). The overall methodology is a top-down refinement of formal specifications; software design decisions are factored into logic steps along an extended `what-to-how´ spectrum. The algorithm design component is based upon reusing the structure common to a class of algorithms, such as local search. By formalizing this structure as an abstract theory, the system can then instantiate its parameters to domain-specific functions, thus obtaining a high-level program specification. The component dealing with parallel program development supports a generalized data flow model, in which a computation is broken down into a collection of distinct atomic units. These are then scheduled and assigned to individual processors through formalisms expressing resource allocation constraints. The authors illustrate algorithm design with the development of the simplex algorithm from a high-level specification and develop a parallel version of one suboperation, the dot product computation