区间上非线性程序的终止性判定  

Termination Decision of Nonlinear Programs over Intervals

作　　者：姚勇[1] 

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

出　　处：《软件学报》2010年第12期3116-3123,共8页Journal of Software

基　　金：国家自然科学基金Nos.90718041;10901116;11001228;国家重点基础研究发展计划(973)No.2004CB318003;中国科学院知识创新工程No.KJCX2-YW-S02;上海市高可信计算重点实验室开放课题No.07dz22304200801~~

摘　　要：分析了如下类型程序的终止性:While x∈Ωdo{x:=f(x)}end.其中,x是程序变量,Ω是一个区间,f是一个连续函数.这类程序被称为区间上非线性程序.证明了上面程序不终止的必要条件是函数在区间内部或边界上有不动点.如果不动点不在区间的边界,则上述结果是充要条件.仅仅在区间边界上有不动点的情况下,对函数略加限制,也建立了相应结果.特别地,对逐段多项式连续函数程序的终止性给出了完备判定算法.In this paper, the termination of the following programs is analized. While x∈Ωdo {x=f（x）} end. When x is. the only program variable, Ω is an interval and f is a continuous function. These are called the Nonlinear Programs over Intervals. This paper shows that the necessary condition for non-termination of the above program is that there is a fixed point off, either within the interval Ω, or on the boundary of Ω. Furthermore, if there is a fixed point within Ω, the above condition is not only necessary, but also sufficient. In the case that all fixed points are on the boundary of Ω it is also possible to construct the corresponding necessary and sufficient condition of non-termination by introducing more constraints for the continuous function f. A piecewise polynomial function meets these constraints, and a decision algorithm for continuous piecewise polynomial function is presented in the paper.

关 键 词：程序验证 终止性分析 非线性程序 不动点 周期轨 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]