趙曉燕

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

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

中圖分類(lèi)號(hào)：TP391文獻(xiàn)標(biāo)識(shí)碼：A文章編號(hào)：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)空間映射到到一個(gè)良基域上[1]。一個(gè)程序沒(méi)有秩函數(shù)，卻可能是一個(gè)可終止的程序,因此，秩函數(shù)的存在僅僅是程序終止的充分條件。即使一個(gè)程序有秩函數(shù),但是也可能沒(méi)有線性秩函數(shù)。因此,很多研究人員開(kāi)始采用各種非秩函數(shù)的方法來(lái)研究程序的終止性問(wèn)題。

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

在文獻(xiàn)[2]中, Tiwari研究了一類(lèi)形如：

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

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

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