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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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