串行線性賦值循環(huán)程序的終止性判定

趙曉燕

摘要：對于并行賦值的線性循環(huán)程序，已有文獻通過矩陣特征值方法來判定其終止性,但該方法并不適用于常見的串行賦值程序。該文通過把串行賦值程序轉(zhuǎn)換為并行賦值的程序，再利用矩陣特征值和特征向量來對程序的終止性作出判定，從而擴大了該方法的應用范圍。

關(guān)鍵詞：線性程序；終止性；并行賦值；串行賦值

中圖分類號：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 cant 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

證明程序終止性的主流方法是綜合循環(huán)程序的秩函數(shù),該函數(shù)將程序狀態(tài)變量從狀態(tài)空間映射到到一個良基域上[1]。一個程序沒有秩函數(shù)，卻可能是一個可終止的程序,因此，秩函數(shù)的存在僅僅是程序終止的充分條件。即使一個程序有秩函數(shù),但是也可能沒有線性秩函數(shù)。因此,很多研究人員開始采用各種非秩函數(shù)的方法來研究程序的終止性問題。

對于一個形如：while(循環(huán)條件) {語句組}的普通程序的終止性是不可判定的,即使是所有的循環(huán)條件和變量更新都是仿射的,因為這種程序可以用計數(shù)器機器來模擬[2]，而一個計數(shù)器機器對所有的輸入是否都終止是不可判定的[3]。

在文獻[2]中, Tiwari研究了一類形如：

P1：While ( Bx>b ) { x=Ax+c；}

的線性循環(huán)程序的終止性問題,并通過計算系數(shù)矩陣A的特征值和特征向量來判定這類循環(huán)程序的終止性。其中，x=Ax+c表示對每個變量進行線性同時賦值，Bx>b表示在變量x的狀態(tài)空間上的線性不等式的邏輯與。這種線性并行賦值程序比普通文獻中考慮的那些程序要簡單一些[4-6]。

由于目前的程序大多數(shù)都是串行賦值，因此直接使用Tiwari的方法是不可行的。在實際分析程序的過程中，我們首先需要將這種線性程序的串行賦值轉(zhuǎn)換成并行賦值，再計算轉(zhuǎn)換后的線性程序的系數(shù)矩陣的特征值，通過其特征向量來判定此類線性循環(huán)程序的終止性。