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

Termination of a Class of Nonlinear Loop Programs

作　　者：李骏[1] 李轶[1] 冯勇[1] 

机构地区：[1]中国科学院成都计算机应用研究所,四川成都610041

出　　处：《四川大学学报（工程科学版）》2009年第1期129-133,共5页Journal of Sichuan University (Engineering Science Edition)

基　　金：国家科委973资助项目(2004CB318003);中国科学院知识创新重要方向资助项目(KJCX2-YW-S02);国家自然科学基金资助项目(10771205)

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

关 键 词：非线性程序 终止性 程序验证 JORDAN标准型 

分 类 号：TP311.11[自动化与计算机技术—计算机软件与理论]