一类循环条件非线性的程序终止性

针对Tiwari提出的线性循环程序的终止性判定问题,提出了循环条件为齐次多项式的非线性程序的不可中止性判定的理论证明,然后将程序终止性判定问题转化为参数半代数系统的求解。在求解中,借助强有力的代数符号工具DISCOVERER,解决了计算机浮点计算所造成的近似误差,精确地判定这类程序的不可终止性。最后,通过计算代数理论,把循环条件推广到了非齐次多项式,并且进行了验证。通过理论的证明和实验的验证,解决循环条件是非线性的一类循环程序的方法是高效合理的。

Termination of a Class of Nonlinear Loop Programs

For termination of linear loop programs proposed by Tiwari,the proof that the non-linear programs of cycle conditions is the homogeneous polynomial and can not be terminated was put forward.Then the program termination was transformed as the solution of a system of semi-algebra.A powerful algebraic symbols tool DISCOVERER was used to solve the approximate error caused by floating-point calculations,and accurately determinate that such programs can not be terminated.Finally,by the computation algebra theory,the cycle conditions was extended to non-homogeneous polynomial.Through theoretical and experimental proof,for a kind of cycle programs that cycle condition is non-linear,these solutions is efficient and reasonable.