串行线性赋值循环程序终止性判定.docVIP

串行线性赋值循环程序终止性判定摘要：对于并行赋值的线性循环程序，已有文献通过矩阵特征值方法来判定其终止性,但该方法并不适用于常见的串行赋值程序。该文通过把串行赋值程序转换为并行赋值的程序，再利用矩阵特征值和特征向量来对程序的终止性作出判定，从而扩大了该方法的应用范围。 关键词：线性程序；终止性；并行赋值；串行赋值 中图分类号：TP391文献标识码：A文章编号：1009-3044(2012)15-3737-02 Termination of Serial linear Assignment Loop Programs ZHAO Xiao-yan (Staff Room of Mathematics and Computer, North Sichuan Medical College, Nanchong 637007, China) Abstract: For linear loop programs with parallel assignment, the existing literature determined its termination through matrix eigenvalue method, but the method can’t apply to the daily programs with serial assignment. This paper converts programs with parallel assignment to programs with serial assignment, and then use the eigenvalues and eigenvectors method to determine the termination of the program, so the field of application of this method is expanded. Key words: linear programs; termination; parallel assignment; serial assignment 证明程序终止性的主流方法是综合循环程序的秩函数,该函数将程序状态变量从状态空间映射到到一个良基域上[1]。一个程序没有秩函数，却可能是一个可终止的程序,因此，秩函数的存在仅仅是程序终止的充分条件。即使一个程序有秩函数,但是也可能没有线性秩函数。因此,很多研究人员开始采用各种非秩函数的方法来研究程序的终止性问题。 对于一个形如：while(循环条件) {语句组}的普通程序的终止性是不可判定的,即使是所有的循环条件和变量更新都是仿射的,因为这种程序可以用计数器机器来模拟[2]，而一个计数器机器对所有的输入是否都终止是不可判定的[3]。 在文献[2]中, Tiwari研究了一类形如： P1：While ( Bxb ) { x=Ax+c；} 的线性循环程序的终止性问题,并通过计算系数矩阵A的特征值和特征向量来判定这类循环程序的终止性。其中，x=Ax+c表示对每个变量进行线性同时赋值，Bxb表示在变量x的状态空间上的线性不等式的逻辑与。这种线性并行赋值程序比普通文献中考虑的那些程序要简单一些[4-6]。 由于目前的程序大多数都是串行赋值，因此直接使用Tiwari的方法是不可行的。在实际分析程序的过程中，我们首先需要将这种线性程序的串行赋值转换成并行赋值，再计算转换后的线性程序的系数矩阵的特征值，通过其特征向量来判定此类线性循环程序的终止性。 1