Conference: ICT&Applications and Collocated Events

The greatest site in all the land!

Generation Method for Correct Parallel Programs Based on Equivalent Transformation

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

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: