基于递推链代数与迭代序列敛散性的死循环检测.pdfVIP

第卷第期 计 算 机 学 报 ３６ １１ 　 　　　　　　　　 Ｖｏｌ．３６Ｎｏ．１１ 年月 ２０１３１１ ＣＨＩＮＥＳＥＪＯＵＲＮＡＬＯＦＣＯＭＰＵＴＥＲＳ Ｎｏｖ．２０１３ 　 基于递推链代数与迭代序列敛散性的死循环检测 姬秀娟杨巨峰许静李晓虹封磊 　 　　　 　　 （南开大学计算机与控制工程学院天津 ） ３０００７１ 　 　 摘要该文针对两大类循环分别给出了非终止性判定的数学方法首先，针对基本迭代关系为线性或几何性的 ． 　　 循环提出了基于递推链代数的分析方法通过递推链代数将循环变量进行统一表示，根据运算规则推导出循环条 ． 件关于迭代次数的闭形式函数，然后通过约束求解以及单调性判断循环的非终止性其次，针对一元非线性循环提 ． 出了基于迭代序列敛散性的分析方法根据迭代函数以及不动点判断迭代函数产生的迭代序列的敛散性来判断循 ． ［］ ２０ 、 ［ ， ］ 、 ［］ 环的非终止性实验部分采用 的组循环文献 的组循环文献 以及自组的组 ． Ｖｅｌｒｏｅｎ ５２ １８１９２１２３２３ ３ １３ ｙ ， ： ， 循环进行分析验证结果表明该文所提出的方法能有效地判断循环的非终止性若循环无法终止可以推导出循环 ； ， 无法终止的变量约束若循环可终止则可以估算循环的迭代次数． 关键词死循环检测静态分析递推链代数迭代函数收敛性软件工程 ； ； ； ； 　 中图法分类号 号 ／ ＴＰ３１１ 犇犗犐 １０．３７２４ＳＰ．Ｊ．１０１６．２０１３．０２２４５ 　　　 　 犐狀犳犻狀犻狋犲犔狅狅犇犲狋犲犮狋犻狅狀犅犪狊犲犱狅狀犆犺犪犻狀狊狅犳犚犲犮狌狉狉犲狀犮犲犃犾犲犫狉犪 狆 犵 犪狀犱犆狅狀狏犲狉犲狀犮犲狅犳犐狋犲狉犪狋犻狏犲犛犲狌犲狀犮犲 犵 狇 ＪＩＸｉｕＪｕａｎＹＡＮＧＪｕＦｅｎＸＵＪｉｎＬＩＸｉａｏＨｏｎＦＥＮＧＬｅｉ 　 　 　 　 ｇ ｇ ｇ