On the Equivalence of Programs

In this paper, we construct a logical system to derive the equivalence of while programs directly. The system is irrelevant to the correctness and its foundation is Lw??o. By decomposing while-sentences we give axioms to describe the equivalence of programs. At last, the completeness of the logical system is proved.