摘要
为了研究程序设计中的软件可信性问题,分析了非线性单重循环程序While x∈Ωdo{x:=f(x)}end当Ω为有限个互不相交的闭区间之并时的终止性,证明该终止性在一定条件下可以由周期轨道的存在性加以判别,给出了确定条件下此类程序不终止的充分必要条件,并建立了相应的判定程序。进一步,利用Brower不动点定理及凸分析的理论,在Rm上建立了当循环条件Ω是有限个互不相交的闭凸集之并时线性循环程序终止性判定的方法。
To study the problem of reliability of software in program design,the termination of program was discussed While x∈Ω do {x： =f（x）} end under the condition that Ω is union of finite mutually disjoint closed intervals.It was proven that the termination of such loops under some definite conditions can be determined by the existence of period orbits.The necessary and sufficient condition of the non-termination for such programs under definite conditions was discussed and corresponding algorithms were given.In addition,applying Brower fixed point theorem and the theory of convex analysis,the conclusion of termination of linear loops when loop condition Ω is union of finite mutually disjoint closed convex sets in Rm was given.
出处
《四川大学学报（工程科学版）》
EI
CAS
CSCD
北大核心
2013年第2期110-116,共7页
Journal of Sichuan University (Engineering Science Edition)
基金
国家自然科学基金资助项目(11101295)
国家自然科学基金资助项目(N61103110)
重庆市科技攻关项目(cstc2012ggB40004)
关键词
非线性循环
线性循环
终止性分析
周期轨道
nonlinear loops
linear loops
termination analysis
periodic orbit
