Termination analysis of nonlinear loops and linear loops in m

To study the problem of reliability of software in program design, the termination of program was discussed While x∈Ω do {x:=f(x)} end under the condition that Ω is union of finite mutually disjoint closed intervals. It was proven that the termination of such loops under some definite conditions can be determined by the existence of period orbits. The necessary and sufficient condition of the non-termination for such programs under definite conditions was discussed and corresponding algorithms were given. In addition, applying Brower fixed point theorem and the theory of convex analysis, the conclusion of termination of linear loops when loop condition Ω is union of finite mutually disjoint closed convex sets in m was given.