Two kinds of program transformations widely-used in optimizing compilation, statement exchange and variable substitution, are investigated and their soundness conditions are formally defined with CTL-FV, an extension of the temporal logic CTL (computation tree logic). Sound statement exchange T_exch and sound variable substitution T_sub are defined with conditioned rewriting rules and their soundness is proved under an inductive proof frame. In addition, based on T_exch, the soundess of another transformation, dependence-preserving statement reordering inside basic blocks of programs, is also proved with a constructive method.