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

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

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

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

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

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