|
| 摘要: |
| 分析了如下类型程序的终止性:While x∈Ω do {x:=f(x)} end.其中,x是程序变量,Ω是一个区间,f是一个连续函数.这类程序被称为区间上非线性程序.证明了上面程序不终止的必要条件是函数在区间内部或边界上有不动点.如果不动点不在区间的边界,则上述结果是充要条件.仅仅在区间边界上有不动点的情况下,对函数略加限制,也建立了相应结果.特别地,对逐段多项式连续函数程序的终止性给出了完备判定算法. |
| 关键词: 程序验证 终止性分析 非线性程序 不动点 周期轨 |
| DOI： |
| 分类号: |
| 基金项目:Supported by the National Natural Science Foundation of China under Grant Nos.90718041, 10901116, 11001228 (国家自然科学基金); the National Basic Research Program of China under Grant No.2004CB318003 (国家重点基础研究发展计划(973)); the Knowledge Innovation Program of the Chinese Academy of Sciences under Grant No.KJCX2-YW-S02 (中国科学院知识创新工程); the Open Project of Shanghai Key Laboratory of Trustworthy Computing of China under Grant No.07dz22304200801 (上海市高可信计算重点实验室开放课题) |
|
| Termination Decision of Nonlinear Programs over Intervals |
|
YAO Yong
|
| Abstract: |
| 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 of f, 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. |
| Key words: program verification termination analysis nonlinear program fixed point periodic orbit |
