Some transformation rules of imperative concurrent programs,
based on congruence and refinement relations between statements,
are presented. They can be used to introduce and/or eliminate
synchronous communication statements and parallelism in these
programs. The development is made within a subset of SPL,
a good representative of imperative notations for concurrent
and reactive programs, explained in the books of Manna and Pnueli,
and used within the Stanford Temporal Prover (STeP).
As an important complement for the applications, a collection
of tactics, for the acceleration of broader transformations,
is described. Tactics apply a sequence of rules to a program
with a specific transformation objective. They can be used
either interactively or from within a program, guaranteeing that
the transformation always corresponds to the application of a
sequence of rules.
The transformation rules and the tactics could be used in formal
design. Also, in conjunction with program verifiers and model
checkers. They can derive new programs from verified
ones, preserving their properties, and avoiding
the repetition of verifications for the transformed
programs.
The paper shows that no finite set of transformation rules
suffices to eliminate synchronous communication statements from
programs involving the concatenation and parallelism operators only.
An infinite set is given to suit this purpose, which can be
applied recursively. One of the tactics serves this purpose.
As an example, the formal parallelization of a non-trivial
distributed fast Fourier transform algorithm is given.
