A Purely Logical Approach to the Termination of Imperative Loops

We present and illustrate a method for the generation of the termination conditions for nested loops with abrupt termination statements. The conditions are (first-order) formulae obtained by certain transformations of the program text. The loops are treated similarly to calls of recursively defined functions. The program text is analyzed on all possible execution paths by forward symbolic execution using certain meta-level functions which define the syntax, the semantics, the verification conditions for the partial correctness, and the termination conditions. The termination conditions are expressed as induction principles, however, still in first-order logic. Our approach is simpler than others because we use neither an additional model for program execution, nor a fix point theory for the definition of program semantics. Because the meta-level functions are fully formalized in predicate logic, it is possible to prove in a purely logical way and at object level that the verification conditions are necessary and sufficient for the existence and uniqueness of the function implemented by the program.