首页 | 本学科首页   官方微博 | 高级检索  
     

多区间上非线性程序的终止性判定
引用本文:牟琳,李轶,李玲娜,刘栋.多区间上非线性程序的终止性判定[J].四川大学学报(工程科学版),2011,43(3):76-80.
作者姓名:牟琳  李轶  李玲娜  刘栋
作者单位:1. 中国科学院成都计算机应用研究所,四川成都,610041
2. 电子科技大学计算科学与工程学院,四川成都,610054
基金项目:国家自然科学基金(90718041)
摘    要:主要解决了如下形式的程序的终止性判定的问题:while(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).

关 键 词:程序验证  计算机代数  非线性程序  不动点
收稿时间:4/15/2010 4:37:44 PM
修稿时间:7/16/2010 1:34:46 PM

Termination of Non-linear Programs over the Set of Intervals
Mou Lin,Li Yi,Li Lingna and Liu Dong.Termination of Non-linear Programs over the Set of Intervals[J].Journal of Sichuan University (Engineering Science Edition),2011,43(3):76-80.
Authors:Mou Lin  Li Yi  Li Lingna and Liu Dong
Affiliation:Chengdu Inst. of Computer Applications,Chinese Academy of Sci.;School of Computer Sci. and Eng.,Univ. of Electronic Sci. and Technol. of China;Chengdu Inst. of Computer Applications,Chinese Academy of Sci.;Chengdu Inst. of Computer Applications,Chinese Academy of Sci.
Abstract: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.
Keywords:Program Verification  Computer Algebra  Nonlinear Program  Fixed Point
本文献已被 CNKI 万方数据 等数据库收录!
点击此处可从《四川大学学报(工程科学版)》浏览原始摘要信息
点击此处可从《四川大学学报(工程科学版)》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号