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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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