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

Termination of Non-linear Programs over the Set of Intervals

作　　者：牟琳[1] 李轶[2] 李玲娜[1] 刘栋[1] 

机构地区：[1]中国科学院成都计算机应用研究所,四川成都610041 [2]电子科技大学计算科学与工程学院,四川成都610054

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

基　　金：国家重点基础研究发展计划资助项目(2004CB318003)

摘　　要：主要解决了如下形式的程序的终止性判定的问题:wh ile(x∈Ω)do{x:=f(x)}end,其中,x为程序变元,Ω(Ω=(a1,b1‖∪‖a2,b2‖∪…∪‖an,bn),其中,‖∈{(,),[,]},n∈N*)是间段并集,f是一个多项式函数。证明了:当φ(b1)φ(a2)>0,…,φ(bn-1)φ(an)>0(其中,φ(x)=f(x)-x)时,这类区间上的非线性程序不终止的必要条件是:在Ω内部或者边界上存在不动点。如果不动点仅仅在Ω内部,则上述结果是充要条件。通过添加一定的约束条件,对于仅区间边界有不动点的情况,也给出了判定的方法。对一类多项式函数的终止性给出了完备性的算法(TNPSI)。The solution of the following programs：while（x∈Ω） do {x：=f（x）} end,which was called as Non-linear Programs over intervals,was presented,where x was a program variable,Ω（Ω=（a1,b1‖∪‖a2,b2‖∪…∪‖an,bn）,while ‖∈{（,）,[,]},n∈N） was a set of intervals,and f was a polynomial function.It was proved that,whenφ（b1）φ（a2）0,…,φ（bn-1）φ（an）0（φ（x）=f（x）-x）,the necessary condition for non-termination of the above program was that there existed fixed point within Ω or on the boundaries of Ω.Furthermore,if there were fixed points within Ω,the above condition was not only necessary but also sufficient.When all fixed points were on the boundaries of Ω,the corresponding necessary and sufficient condition of nontermination was established by introducing more constraints,and a decision algorithm for continuous polynomial function was presented.

关 键 词：程序验证 计算机代数 非线性程序 不动点 

分 类 号：TP181[自动化与计算机技术—控制理论与控制工程] TP301[自动化与计算机技术—控制科学与工程]