基于算子分量矩陣模型的IMP程序診斷.pdf

1、本文致力于將基于模型的診斷方法應(yīng)用在程序診斷上，以一種簡單的命令式程序語言IMP編寫的程序?yàn)樵\斷對象，提出了一種以算子分量矩陣為模型的程序診斷方法。算子分量矩陣模型將一個(gè)程序表示為在特定的狀態(tài)空間下的若干個(gè)以算子分量來描述的狀態(tài)遷移矩陣的乘積形式，通過引入特征算子分量和形式算子分量，可以很方便地計(jì)算出程序中蘊(yùn)含的黑盒依賴和白盒依賴關(guān)系。通過對這些依賴關(guān)系的分析可以快速的得到關(guān)于某個(gè)輸出變量的程序分片。該模型表示方法不僅可以表示依賴關(guān)系，

2、還可以表示求值關(guān)系，有很強(qiáng)的表達(dá)能力，并且其表示形式統(tǒng)一、簡潔。在基于模型的診斷思想下，如果一個(gè)變量(出現(xiàn))的觀察值和期望值不一致，那么關(guān)于這個(gè)變量(出現(xiàn))的程序分片是一個(gè)沖突集，然后可以通過求解這些沖突集的碰集來得到診斷。很明顯我們利用矩陣運(yùn)算的數(shù)學(xué)方法比起用邏輯推理的方法能更快地求出沖突集。一般來講，僅通過依賴關(guān)系得到的分片較大，因此候選診斷也很多。本文提出了一種基于值域分析的方法來對候選診斷進(jìn)行鑒別，排除一些非溯因的診斷。本文最后

3、還提出了一種通過遺傳編程來自動(dòng)糾正程序錯(cuò)誤的方法，提出了對IMP程序的哥德爾二叉樹的編碼方式，用子樹交換的交叉算子和有限定的變異算子來實(shí)現(xiàn)進(jìn)化，并通過編制實(shí)驗(yàn)系統(tǒng)來驗(yàn)證該方法的收斂性。 遺傳編程基于模型的診斷最早是由Reiter在1987年提出的一種基于邏輯一致性的診斷方法，早期一般應(yīng)用在物理元件組成的系統(tǒng)的診斷上。利用模型診斷技術(shù)來進(jìn)行程序診斷卻是一個(gè)新課題，由于程序邏輯模型的復(fù)雜性和多樣性，使得將模型診斷技術(shù)應(yīng)用于程序診斷上

4、增加了很多難度?；谀Ｐ偷某绦蛟\斷與傳統(tǒng)的程序調(diào)試技術(shù)的不同在于模型診斷技術(shù)更多的利用了程序的邏輯模型的信息，更少的依賴于人工的干預(yù)，并且可以發(fā)現(xiàn)更多的隱藏的邏輯上的錯(cuò)誤。這對于程序正確性的保證有著傳統(tǒng)的調(diào)試方法不可替代的作用。 基于模型的診斷方法最核心的問題就是需要一個(gè)適合于診斷求解的模型，對于程序診斷也一樣。目前用于診斷目的的程序建模方法主要有依賴模型和基于值的模型，兩者的目的都是為了求程序分片，前者是靜態(tài)分片，后者是動(dòng)態(tài)分

5、片。這兩種模型都采用有向圖的形式來表示。然而，對于有復(fù)雜結(jié)構(gòu)的程序(比如多重分支和多重循環(huán))，圖示的方法顯得非常凌亂，需要用到超圖的形式，并不直觀。而且模型中只反映了程序的部分特性(如依賴關(guān)系和求值軌跡)，得到的診斷范圍很大。 本文提出了一種新的程序建模方法，即算子分量矩陣模型。該模型以一種簡單的的命令式程序語言-IMP語言(具有一定的代表性)為背景，本文的第二章給出了IMP語言的語法和語義。 第三章形式化地定義了算子分

6、量的概念及其運(yùn)算規(guī)則，討論了兩種特殊的算子分量即0算子分量和1算子分量的性質(zhì)，并引入了常變量的概念，使得任何個(gè)表達(dá)式都可以表示成算子分量形式。以IMP語言為討論對象，給出了IMP程序的算子分量矩陣的表示形式。在IMP程序的算子分量矩陣模型(簡稱OCM模型)中，每條語句都對應(yīng)著一個(gè)算子分量矩陣，整個(gè)程序可以轉(zhuǎn)化成若干個(gè)算子分量矩陣的乘積形式。此模型揭示了程序?qū)嶋H上是一個(gè)狀態(tài)空間的不斷遷移過程。 第四章討論了IMP程序在OCM模型表

7、示下的依賴關(guān)系。通過引入特征算子分量，建立程序的特征算子分量矩陣，可以很快地計(jì)算出變量的終值對變量的初值的依賴關(guān)系，即黑盒依賴關(guān)系；通過引入形式算子分量，建立程序的形式算子分量矩陣，可以很容易地求出變量的輸出對語句的依賴關(guān)系，即白盒依賴關(guān)系。而變量對語句的白盒依賴即是與該變量相關(guān)的程序分片。這是一種通過代數(shù)方法求程序分片的新的技術(shù)。第五章給出了基于OCM模型的程序診斷方法。給出了在同構(gòu)假定下的程序診斷問題的形式化描述，其中我們使用規(guī)范來

8、表達(dá)期望程序。并給出了程序診斷的概念和有關(guān)沖突集求解的一些定理。舉例說明了使用OCM模型來進(jìn)行程序診斷的方法，并給出了分段和分層的診斷方法。最后將基于OCM模型的診斷和基于兩種傳統(tǒng)的模型(依賴模型和基于值的模型)的診斷進(jìn)行了比較。 由于基于依賴關(guān)系得到的程序的候選診斷較多，需要進(jìn)一步的診斷鑒別，第六章提出了一種基于變量值域分析的診斷鑒別技術(shù)，在不增加觀測點(diǎn)的情況可以排除一些非溯因的診斷，即程序的觀察不能由這些被排除的診斷邏輯推出

9、。而值域分析過程實(shí)際上是一個(gè)歸謬的溯因過程。 第七章通過加入數(shù)組類型擴(kuò)充了IMP程序語言的語法，稱之為IMP-A，并給出了數(shù)組的OCM建模方法以及對于下標(biāo)變量求白盒依賴的技術(shù)，從而使OCM模型的表示能力更接近實(shí)際程序。 最后一章提出了一個(gè)新的遺傳編程方法來對程序自動(dòng)糾錯(cuò)。利用哥德爾的程序編碼思想，提出了用哥德爾二叉樹來表示命令式程序并對其進(jìn)行染色體編碼的技術(shù)。使用遺傳編程的方法，可以將一個(gè)待診斷的程序進(jìn)化為一個(gè)正確的程序