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

Infinite Loop Detection Based on Chains of Recurrence Algebra and Convergence of Iterative Sequence

该文针对两大类循环分别给出了非终止性判定的数学方法.首先,针对基本迭代关系为线性或几何性的循环提出了基于递推链代数的分析方法.通过递推链代数将循环变量进行统一表示,根据运算规则推导出循环条件关于迭代次数的闭形式函数,然后通过约束求解以及单调性判断循环的非终止性.其次,针对一元非线性循环提出了基于迭代序列敛散性的分析方法.根据迭代函数以及不动点判断迭代函数产生的迭代序列的敛散性来判断循环的非终止性.实验部分采用Velroyen[20]的52组循环、文献[18-19,21-23]的23组循环、文献[3]以及自组的13组循环进行分析验证,结果表明该文所提出的方法能有效地判断循环的非终止性:若循环无法终止,可以推导出循环无法终止的变量约束;若循环可终止,则可以估算循环的迭代次数.

In this paper, two mathematical methods are proposed to detect the non-termination of two types of loop. The first method is based on chains of recurrence algebra. It is for detecting the non-termination of the loops in which the basic iterative relations of variables are linear or geometrical. All the variables in the loop are unified representation by the Chains of Recurrence Algebra （CR）. Then the closed-form function of the loop condition about the number of loop iter- a＇tion is deduced by the rules of CR. According to it the non-termination of loops can be decided through the monotonicity of the closed-form function and constraint solver. The second method is based on convergence of iterative sequence, which is {or detecting the non-termination of the non- linear loop. According to the convergence of iterative function and fixed-point we can determine the non-termination of the loops. In experiments, we analyzed 52 loops which were presented by Velroyen[20] and 23 loops which are from articles [18-19, 21-23] and 13 loops which are created by ourselves. The experimental results show that it can detect the non-termination of loop effec- tively. It can give the variable constraints which make the loop non-terminated. Meanwhile the number of loop iterations can be estimated when the loop is terminated.