On Improving Termination Preservability of Transformations from Procedural Programs into Rewrite Systems by Using Loop Invariants

ABSTRACT. Recently, to analyze procedural programs by using techniques in the field of term rewriting, several transformations of a program into a rewrite system have been developed. For the purpose, such transformations are basically complete in the sense of computation, and, e.g., termination of the rewrite system ensures termination of the program. However, in general, termination of the program is not preserved by the transformations, and thus, the preservation of termination is a common interesting problem. In this paper, we discuss the improvement of a transformation from a simple procedural program over integers into a constrained term rewriting systems by introducing loop invariants to branch conditions of "while" statements so as to preserve termination as much as possible.