基于開放時(shí)態(tài)邏輯的面向方面程序形式化驗(yàn)證和模塊推理研究.pdf

1、面向方面程序設(shè)計(jì)(Aspect-Oriented Programming，AOP)是一種新的程序方法學(xué)，代表程序方法學(xué)的發(fā)展趨勢(shì)。面向方面程序設(shè)計(jì)減少由于軟件項(xiàng)目重建而帶來的代碼重構(gòu)，大大提高軟件系統(tǒng)的模塊化和可重用性。作為一種新的程序方法學(xué)，面向方面程序設(shè)計(jì)的應(yīng)用和研究發(fā)展十分迅速。
　　 由于面向方面語(yǔ)言(Aspect-Oriented Language，AOL)的不知覺性和多量化特點(diǎn)，面向方面程序設(shè)計(jì)更容易引起行為干擾問題

2、，使得面向方面程序的程序驗(yàn)證和模塊推理比傳統(tǒng)程序方法學(xué)復(fù)雜的多。當(dāng)程序員實(shí)現(xiàn)若干個(gè)方面，必須確保每個(gè)方面與基本系統(tǒng)不產(chǎn)生行為干擾問題；如果多個(gè)方面橫切基本系統(tǒng)的同一個(gè)切入點(diǎn)，還要確保多個(gè)方面之間不產(chǎn)生行為干擾問題，面向方面程序的程序驗(yàn)證和模塊推理困難嚴(yán)重影響面向方面應(yīng)用的發(fā)展前景。
　　 傳統(tǒng)形式邏輯的語(yǔ)義模型與面向方面程序的非對(duì)稱行為模型存在失配，使用傳統(tǒng)的形式邏輯進(jìn)行面向方面程序的形式化驗(yàn)證和模塊推理十分困難。本研究提出一種

3、具有非對(duì)稱行為模型的新時(shí)態(tài)邏輯--開放時(shí)態(tài)邏輯(Open TemporalLogic，OTL)，基于開放時(shí)態(tài)邏輯可以有效的解決面向方面程序的形式化驗(yàn)證和模塊推理問題，本研究的主要工作與貢獻(xiàn)包括：
　　 (1)定義開放時(shí)態(tài)邏輯的語(yǔ)法和語(yǔ)義。開放時(shí)態(tài)邏輯引入新的路徑算子，描述系統(tǒng)的內(nèi)部路徑和外部路徑；引入新的時(shí)態(tài)算子，描述一些系統(tǒng)狀態(tài)在外部動(dòng)作影響下的某種不變性。開放時(shí)態(tài)邏輯的語(yǔ)義模型是具有非對(duì)稱性行為模型的開放系統(tǒng)，適合描述面向方

4、面程序的非對(duì)稱行為模型。
　　 (2)提出基于開放時(shí)態(tài)邏輯進(jìn)行面向方面程序的形式化規(guī)約和驗(yàn)證。方面干擾問題與并發(fā)程序的并發(fā)進(jìn)程干擾問題既存在相似性，也存在差異，本研究參考并發(fā)程序的規(guī)約和驗(yàn)證方法，引入可橫切依賴條件約束執(zhí)行過程中的可能方面橫切。本研究的程序規(guī)約包括三個(gè)條件：前置條件、可橫切依賴條件和后置條件。基于本研究的程序規(guī)約建立一個(gè)證明系統(tǒng)進(jìn)行面向方面程序的形式化驗(yàn)證，并證明證明系統(tǒng)的有效性。
　　 (3)提出面向方

5、面程序的模塊約束和模塊推理方法。根據(jù)面向方面程序的行為特點(diǎn)，研究面向方面程序的模塊化內(nèi)涵。與本研究的程序規(guī)約類似，本研究的模塊規(guī)約也由三個(gè)條件組成：前置條件、可橫切依賴條件和后置條件?；诒狙芯康哪K規(guī)約定義不同類型的模塊約束，支持面向方面程序的模塊推理和模塊組合。本研究定義了四種模塊約束：可橫切不變性、非橫切不變性、可橫切正確性和非橫切正確性，不同的模塊約束支持不同的模塊可靠性需求。
　　 (4)提出四種橫切范式。應(yīng)用本研究的