非线性循环及R^m上线性循环的终止性判定  

Termination Analysis of Nonlinear Loops and Linear Loops in R^m

作　　者：陈敬敏[1,2] 

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

出　　处：《四川大学学报（工程科学版）》2013年第2期110-116,共7页Journal of Sichuan University (Engineering Science Edition)

基　　金：国家自然科学基金资助项目(11101295);国家自然科学基金资助项目(N61103110);重庆市科技攻关项目(cstc2012ggB40004)

摘　　要：为了研究程序设计中的软件可信性问题,分析了非线性单重循环程序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.

关 键 词：非线性循环 线性循环 终止性分析 周期轨道 

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