Decidability analysis on termination set of loop programs

摘要

For half a century, computer programs have been widely applied in all areas of industry and daily life. Given any program, whether it can terminate has direct impact on software safety. Many researchers have been working on the termination of programs. One definition of termination is as follows: a program is terminating if it terminates for any initial values; while it is non-terminating if at least one initial value makes it not terminates. Obviously, this definition does not consider program termination''s dependency on initial values, and actually presents two extreme situations of the complicated programs in reality. Different from these two situations, this paper discusses what kinds of initial values can guarantee a program to terminate and what kinds of initial values cannot. For some linear loop assignment programs, whose terminations are decidable, the paper proposes a method using “limit” and “backward iteration” to derive the initial value set that make programs terminate.