Generation Method for Correct Parallel Programs Based on Equivalent Transformation
November 8, 2012
Posted by on
Hidekatsu Koike,Kiyoshi Akama and Katsunori Miura
In the equivalent transformation computation model (ETCM), a set of correct programs is mathematically defined by a formal specification, and a correct program can be generated by selecting a program that is efficient with respect to a desired run-time environment from the set. In the ETCM, a program is a set of rewriting procedures which preserve the meaning of a formal specification |and are thus called equivalent transformation (ET) rules. In the model, computation is regarded as the rewriting of a state that is represented by a set of clauses, and is repeated until a set of answers is obvious, e.g., a set of ground unit clauses is typically obtained. The computation is intrinsically nondeterministic, and hence parallelism is also inherent. We have proposed a sufficient condition for correctness of parallel programs based on the ETCM. In this paper, we present a parallel program generation method and show how the correctness of the programs generated can be guaranteed.
Full Paper in PDF Document