利用符号动力学理论中有关一维离散映射的函数和区间的转换图方法及相关结论,证明一类非线性循环程序不终止的必要条件是在该程序循环区间上有不动点或者周期点存在,并给出相应的终止性验证算法。利用该算法可以验证一维有界闭区间上的非线性循环程序的终止性。最后,给出计算实例演示该算法的算法步骤。
By using the approach of transition diagram in regard to function and interval of onedimensional discrete mapping in symbolic dynamics theory and the correlated conclusion, we prove that the necessary condition for nontermination of one kind of nonlinear loop program is that there are the fixed points or periodic points on loop interval of the program, and present the corresponding algorithm of termination veri fication as well. The use of this algorithm can verify the termination property of nonlinear loop programs in onedimensional bounded closed in terval. At last, we use some computation examples to demonstrate the steps of this algorithm.