多分支单变量循环程序的终止性分析∗

摘要

对多分支单变量循环程序的终止性问题进行了研究。证明了在适定的条件下，该类循环程序不可终止性的充分必要条件是迭代映射在循环条件形成的区域中有不动点。特别地，当这类循环程序是多项式循环程序时，在给定条件下，其在实数域上的终止性问题是可判定的。%Termination of multipath loop programs with one variable is analyzed in this paper. It demonstrates that under proper conditions, this kind of loops is non-terminate if and only if there exist fixed points. Especially, if the class of programs are polynomial, then under proper conditions, the termination of the programs is decidable over the reals.