面向方面程序設(shè)計(Aspect-Oriented Programming,AOP)是一種新的程序方法學(xué),代表程序方法學(xué)的發(fā)展趨勢。面向方面程序設(shè)計減少由于軟件項目重建而帶來的代碼重構(gòu),大大提高軟件系統(tǒng)的模塊化和可重用性。作為一種新的程序方法學(xué),面向方面程序設(shè)計的應(yīng)用和研究發(fā)展十分迅速。 由于面向方面語言(Aspect-Oriented Language,AOL)的不知覺性和多量化特點,面向方面程序設(shè)計更容易引起行為干擾問題,使得面向方面程序的程序驗證和模塊推理比傳統(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)的形式邏輯進(jìn)行面向方面程序的形式化驗證和模塊推理十分困難。本研究提出一種具有非對稱行為模型的新時態(tài)邏輯——開放時態(tài)邏輯(Open TemporalLogic,OTL),基于開放時態(tài)邏輯可以有效的解決面向方面程序的形式化驗...

【文章頁數(shù)】：115 頁

【學(xué)位級別】：博士

【文章目錄】：
致謝
摘要
Abstract
第1章 緒論
    1.1 研究背景
        1.1.1 面向方面方法學(xué)的興起
        1.1.2 方面干擾問題的陰影
        1.1.3 軟件工程和形式化方法
    1.2 研究動機(jī)和研究意義
        1.2.1 研究動機(jī)
        1.2.2 研究意義
    1.3 研究內(nèi)容
        1.3.1 研究基礎(chǔ)
        1.3.2 創(chuàng)新和特色
        1.3.3 研究約束
    1.4 文章結(jié)構(gòu)
第2章 面向方面方法學(xué)研究
    2.1 面向方面方法學(xué)的哲學(xué)基礎(chǔ)
        2.1.1 傳統(tǒng)程序方法學(xué)的主客觀認(rèn)知論
        2.1.2 康德的認(rèn)識論
        2.1.3 Dooyeweerd的認(rèn)知觀和方面哲學(xué)
    2.2 面向方面語言研究
        2.2.1 基本概念和結(jié)構(gòu)
        2.2.2 多量化和不知覺性
        2.2.3 Aspect J
    2.3 面向方面程序設(shè)計研究
        2.3.1 設(shè)計過程
        2.3.2 程序行為的非對稱性
        2.3.3 方面行為分類
        2.3.4 方面干擾例子
    2.4 本章小結(jié)
第3章 開放時態(tài)邏輯和面向方面程序形式化規(guī)約
    3.1 現(xiàn)有時態(tài)邏輯研究
        3.1.1 線性時態(tài)邏輯
        3.1.2 計算樹邏輯
        3.1.3 現(xiàn)有時態(tài)邏輯分析
    3.2 開放時態(tài)邏輯
        3.2.1 開放時態(tài)邏輯語法
        3.2.2 開放時態(tài)邏輯的非對稱行為模型
    3.3 現(xiàn)有程序規(guī)約研究
        3.3.1 Hoare三元組
        3.3.2 信賴條件和保證條件
        3.3.3 假設(shè)規(guī)約和保證規(guī)約
    3.4 基于開放時態(tài)邏輯的面向方面程序規(guī)約
        3.4.1 可橫切依賴條件
        3.4.2 三條件的面向方面程序規(guī)約
        3.4.3 例子
    3.5 本章小結(jié)
第4章 基于開放時態(tài)邏輯的面向方面程序形式化驗證
    4.1 現(xiàn)有程序驗證方法研究
        4.1.1 模型檢查
        4.1.2 程序證明
        4.1.3 順序程序驗證
        4.1.4 并發(fā)程序驗證
        4.1.5 現(xiàn)有的面向方面程序驗證方法
    4.2 基于Dijkstra順序命令語言的核心語言
        4.2.1 核心語言語法
        4.2.2 核心語言操作語義
        4.2.3 核心語言計算模型
    4.3 基于核心語言的證明系統(tǒng)
        4.3.1 賦值公理
        4.3.2 蘊(yùn)含規(guī)則
        4.3.3 順序規(guī)則
        4.3.4 橫切規(guī)則
        4.3.5 條件規(guī)則
        4.3.6 循環(huán)規(guī)則
        4.3.7 有效性證明
    4.4 本章小結(jié)
第5章 基于開放時態(tài)邏輯的面向方面程序模塊推理
    5.1 程序模塊化內(nèi)涵研究
        5.1.1 傳統(tǒng)程序方法學(xué)的模塊化
        5.1.2 面向方面程序的模塊化內(nèi)涵
    5.2 基于開放時態(tài)邏輯的模塊規(guī)約
    5.3 現(xiàn)有的面向方面程序模塊推理研究
        5.3.1 無害通知
        5.3.2 現(xiàn)有的方面正確性概念
        5.3.3 行為子類型和契約式設(shè)計
    5.4 基于開放時態(tài)邏輯的面向方面程序模塊推理
        5.4.1 可橫切不變性
        5.4.2 非橫切不變性
        5.4.3 可橫切正確性
        5.4.4 非橫切正確性
    5.5 本章小結(jié)
第6章 橫切范式
    6.1 橫切不變性范式
        6.1.1 問題提出
        6.1.2 直接判定方法
    6.2 非橫切不變性范式
        6.2.1 問題提出
        6.2.2 直接判定方法
    6.3 橫切正確性范式
        6.3.1 問題提出
        6.3.2 增量式判定方法
    6.4 非橫切正確性范式
        6.4.1 問題提出
        6.4.2 增量式判定方法
    6.5 本章小結(jié)
第7章 總結(jié)及其展望
    7.1 研究工作總結(jié)
    7.2 未來工作展望
參考文獻(xiàn)
攻讀博士學(xué)位期間主要的研究成果
個人簡介



本文編號：3779121