Z形式規(guī)約切片的研究.pdf

1、程序切片是由WeiserM.提出的一種重要的程序分析和理解的方法，用于從源程序P中抽取對程序中特定點p上的特定變量V有影響的語句和控制條件，組成新的程序(稱作切片)，然后通過分析切片來分析源程序的行為，其中〈p，V〉稱作切片標準。程序切片技術的研究、發(fā)展和應用已經(jīng)經(jīng)歷了二十多年，眾多學者對切片技術作過專門的研究和應用開發(fā)，并且取得了一些具有理論和應用價值的成果，使得它在程序分析、理解、優(yōu)化、調試、測試、度量、復用、程序變換、模型檢查、軟

2、件安全、軟件維護、軟件逆向工程、軟件再工程中得到了廣泛應用。 隨著人們對切片技術的進一步研究，切片的概念不斷延伸，切片應用范圍也在不斷擴大?，F(xiàn)在切片技術已經(jīng)不僅僅是對程序源代碼的分析，而是已經(jīng)應用到形式規(guī)約、UML和軟件體系結構等方面。OdaT.和ArakiK.最早于1993年把程序切片的思想引入到Z形式規(guī)約中去；隨后ChangJ.和RichardsonD.J.于1994年在此基礎上把形式規(guī)約切片劃分為靜態(tài)形式規(guī)約切片和動態(tài)形式

3、規(guī)約切片；緊接著LeminenJ.研究了數(shù)據(jù)切片，并在此基礎上把OttL.的基于程序切片的模塊內聚性度量方法應用到形式規(guī)約的內聚性度量中。 論文研究詳細討論了已有的程序切片和依賴性分析技術，結合國內外在形式規(guī)約切片及其應用方面的研究現(xiàn)狀，對形式規(guī)約切片及其應用的若干關鍵技術進行了深入研究，提出基于依賴性分析的Z形式規(guī)約切片和基于關系演算的Z形式規(guī)約切片，并在此基礎上把Z形式規(guī)約切片應用到提升、定理證明和度量上，在一定程度上幫助人

4、們對形式規(guī)約的分析與理解。論文主要工作有： 1.基于依賴性分析的Z形式規(guī)約切片 提出了一種基于依賴性分析的Z形式規(guī)約切片方法；該方法分析了傳統(tǒng)的數(shù)據(jù)依賴和控制依賴。數(shù)據(jù)依賴是變量的定義和使用的屬性；如果數(shù)據(jù)通過一系列的狀態(tài)變化可從謂詞p1傳播到謂詞p2，則稱謂詞p2數(shù)據(jù)依賴于謂詞p1。數(shù)據(jù)依賴可以發(fā)生在相同的謂詞之間，也可以發(fā)生在不同謂詞之間；如果數(shù)據(jù)依賴發(fā)生在相同的謂詞之間，則謂詞肯定在同一模式中出現(xiàn)；如果數(shù)據(jù)依賴發(fā)生

5、在不同的謂詞之間，則謂詞既可以出現(xiàn)在同一模式中，又可以出現(xiàn)在不同模式中。控制依賴是形式規(guī)約的控制結構的屬性；如果謂詞p1潛在地決定了謂詞p2適用與否，則稱謂詞p2控制依賴于謂詞p1。因為if-then-else是Z語言中的主要控制結構，所以控制依賴可以發(fā)生在if-then-else中。為了更好地描述Z形式規(guī)約和強調操作模式發(fā)生時應滿足的條件，除了分析傳統(tǒng)的數(shù)據(jù)依賴和控制依賴外，我們引入一種新的依賴關系——邏輯依賴，是由操作模式的前置條件

6、引起的，是控制依賴的一種特殊形式。直接邏輯依賴可以發(fā)生在模式內，不能發(fā)生在模式間；間接邏輯依賴發(fā)生在模式演算中。 雖然對Z形式規(guī)約的各種依賴情形進行了分析，但只有這些信息還不足以對Z形式規(guī)約進行切片分析，而且這些信息也是雜亂的，因此論文對于模式和形式規(guī)約分別引入模式依賴圖和形式規(guī)約依賴圖的概念把這些信息圖形化地表示出來以幫助理解。一個模式表示成一個模式依賴圖，含有一個入口節(jié)點表示模式的入口，節(jié)點表示謂詞，邊表示謂詞的各種依賴關系

7、。為了表示千差萬別的模式的使用方式，論文借鑒類的使用方式，使用一個框架來模擬所有可能的模式的使用情況?？蚣苁紫日{用初始狀態(tài)模式，然后進入一個循環(huán)，在該循環(huán)中對各種模式進行調用，在通過循環(huán)的每個重復中，控制能夠傳遞到任何地方的模式中。初始狀態(tài)模式、框架循環(huán)都控制依賴于框架入口節(jié)點，框架循環(huán)也控制依賴于自身，這樣就形成了形式規(guī)約依賴圖。在模式依賴圖和形式規(guī)約依賴圖的基礎上分別利用圖形可達性算法和兩階段圖形可達性算法就可以求解Z形式規(guī)約切片，

8、切片結果具有較高的精確度，沒有丟失必要的信息。 2.基于依賴性分析的Z形式規(guī)約切片的形式化描述 為了解決程序切片可能存在的語義不一致性和模糊性，幫助人們正確地理解程序切片的含義，從比較嚴格的意義上明確程序切片的應用領域，對基于依賴性分析的程序切片進行了形式化描述。首先對程序中的語句和變量進行形式化描述；其次對于目前流行的兩種程序切片的定義，即WeiserM程序切片和OttensteinKJ程序切片定義進行形式化描述；之后

9、對程序依賴圖和系統(tǒng)依賴圖的兩個重要組成部分，節(jié)點和邊按照不同類型和不同形狀進行形式化描述；最后對于基于程序依賴圖的圖形可達性算法和基于系統(tǒng)依賴圖的兩階段圖形可達性算法進行形式化描述。 依據(jù)SloaneAM提出的廣義程序切片的概念可知形式規(guī)約切片是程序切片的一種特殊形式，所以對于程序切片的形式化描述同樣也可以應用于形式規(guī)約切片，這樣就可以借助一些Z的輔助工具幫助解決切片問題。 3.基于關系演算的Z形式規(guī)約切片 提出

10、了一種基于關系演算的Z形式規(guī)約切片方法。對于Z形式規(guī)約中每個模式s引入三個關系，二元關系MOD(s)、三元關系USE(s)和二元關系CONTROL(s)來輔助切片的求解過程，主要利用關系代數(shù)的選擇、投影和連接等運算和Z語言自帶的關系運算，如，定義域限定、值域限定、求關系的定義域和值域等運算來計算模式前向切片和模式后向切片，把計算切片的過程演變成關系演算的過程。該切片方法避免了構造依賴圖的費時費力，降低了出錯的機率。 4.變量定義

11、和使用情況的探討 變量定義和使用情況的分析是論文第二章計算數(shù)據(jù)依賴與控制依賴和第四章計算數(shù)據(jù)依賴的基礎。鑒于Z語言基本的賦值運算符有：集合定義符“==”、關系定義符“==”、函數(shù)定義符“==”、枚舉型定義符“∷=”和標準定義符“=”等，而且Z語言使用一階謂詞邏輯、集合、關系、映射、序列和包等表示法來描述系統(tǒng)，所以我們首先借助已有的數(shù)學公式、定律和定理對表達式進行化簡，然后分別討論這些數(shù)學抽象對變量的定義和使用情況。變量定義分析的

12、任務是找出每個謂詞中形式上的賦值變量，使用變量分析就是要找出一個表達式到底依賴了哪些變量。論文采用一個遞歸分析的方法，逐層找出加在基對象上的操作類型，最后這些操作綜合起來就可以找出定義變量和使用變量的情況。 5.Z形式規(guī)約切片在提升和定理證明中的應用 把Z形式規(guī)約切片應用到提升中去，給出了一種求解提升模式Promote的公式，實現(xiàn)了形式規(guī)約的結構化，這樣就可以用局部操作模式和提升模式來描述全局操作模式，而不必把每一個全局

13、操作模式都羅列出來。 把Z形式規(guī)約切片應用到定理證明中去，把定理證明的過程轉化為以結論為切片標準的后向Z形式規(guī)約切片的過程。 6.基于依賴性分析的Z形式規(guī)約度量 在模式依賴性分析的基礎上提出一組針對Z形式規(guī)約的耦合性度量準則。該組度量準則考慮了模式修飾、模式包含、模式演算和模式作為類型等多個方面。為了驗證度量準則與人們經(jīng)驗的一致性，論文用交通車輛管理系統(tǒng)作為案例來討論。為了更好地說明提出的Z模式耦合性度量與其它度

14、量的聯(lián)系同時考察了著名的CK度量，并比較這兩種度量在評估系統(tǒng)時的優(yōu)劣。試驗結果表明該度量準則與人們廣泛接受的CK度量顯著相關，與人們的經(jīng)驗具有高度的相關性；根據(jù)這些度量準則可以發(fā)現(xiàn)一些問題，并把問題杜絕在軟件開發(fā)的早期階段，減少由于錯誤或不合理分析導致的浪費，并可對系統(tǒng)進行有效的評估。 論文主要的創(chuàng)新點有以下三個方面： 1.提出一種基于依賴性分析的Z形式規(guī)約切片方法。在該方法中，除了分析傳統(tǒng)的數(shù)據(jù)依賴和控制依賴外，為了強

15、調操作模式的前置條件，論文引入了一種新的依賴關系——邏輯依賴。之后，鑒于Z形式規(guī)約沒有類似程序代碼的“主程序”的原因，采用面向對象系統(tǒng)依賴圖的形式對其進行圖形化表示；對于模式和形式規(guī)約分別引入模式依賴圖和形式規(guī)約依賴圖的概念。在此基礎上給出了一種有效的基于依賴圖可達性分析的Z形式規(guī)約切片方法，該方法具有較高的精確度，沒有丟失必要的信息。 2.提出了一種基于關系演算的Z形式規(guī)約切片方法。該方法主要利用關系代數(shù)的選擇、投影和連接等運

16、算和Z語言自帶的關系運算，如，定義域限定、值域限定、求關系的定義域和值域等運算來計算切片。該方法避免了構造依賴圖的費時費力，降低了出錯的機率。 3.進一步拓寬了依賴性分析和Z形式規(guī)約切片的應用范圍，提出了一種求解提升模式Promote的公式；把定理證明的過程轉化為以結論為切片標準的計算一個或多個切片的過程；提出一組針對Z形式規(guī)約的耦合性度量準則，考慮了模式修飾、模式包含、模式演算和模式作為類型等多個方面。根據(jù)這些度量準則，可以將