矩陣在理論數(shù)學、工程數(shù)學以及計算機科學中都有著廣泛的應用。例如飛行控制系統(tǒng)的設計中,矩陣被用于飛行器受力狀況的描述,運動學方程的推導,以及飛行控制算法的設計。因此,矩陣算法和矩陣數(shù)學推導的正確性對這類安全關鍵系統(tǒng)的可靠性有著極大的影響。形式化方法是保障計算機系統(tǒng)安全可靠的一種重要方法,其中定理證明技術可用于數(shù)學公式和計算機算法的驗證,是最嚴格、最強力的驗證手段。Coq就是這樣一個交互式的高階定理證明器,它基于歸納構造演算的基本理論,具有很強的表達能力,支持豐富的邏輯系統(tǒng)。Coq可用于表達規(guī)范說明,構造滿足規(guī)范說明的程序模型,以及對可信性要求很高的程序進行形式化驗證。雖然Coq中有著豐富的定理庫,但是,現(xiàn)有的矩陣形式化方面的幾種方案卻不盡人意,基于List的方案表達能力受限,基于依賴類型List的方案復雜難驗證,基于函數(shù)的方案只是驗證了矩陣理論,不能構造出具有具體數(shù)據(jù)的矩陣,也不能用于實際矩陣的推導驗證,并且不利于從描述中提取可執(zhí)行程序。本文提出了一種基于Record類型的矩陣形式化方法,它具有描述上的簡明性、證明上的簡單性、使用上的簡便性以及程序抽取的可行性等諸方面的綜合性優(yōu)勢。本文主... 

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

【學位級別】：碩士

【文章目錄】：
摘要
abstract
注釋表
第一章 緒論
    1.1 研究背景
    1.2 研究現(xiàn)狀
        1.2.1 HOL中的矩陣形式化
        1.2.2 基于元組的矩陣形式化
        1.2.3 基于List的矩陣形式化
        1.2.4 基于依賴類型的List的矩陣形式化
        1.2.5 基于函數(shù)的矩陣形式化
    1.3 研究的工作和意義
    1.4 本文安排
第二章 背景知識
    2.1 形式化驗證工具
        2.1.1 模型檢測工具
        2.1.2 定理證明工具
    2.2 Coq定理證明器
        2.2.1 Coq系統(tǒng)結構
        2.2.2 Coq中的數(shù)據(jù)類型及語法
        2.2.3 Coq中的證明方法
    2.3 Coq標準庫及第三方庫
        2.3.1 Coq標準庫
        2.3.2 mathcomp庫
        2.3.3 Coquelicot庫
    2.4 Coq相關應用
    2.5 本章小結
第三章 基于Record類型的矩陣實現(xiàn)
    3.1 向量的定義與驗證
        3.1.1 向量的定義
        3.1.2 向量運算及基本性質(zhì)
    3.2 矩陣的定義與驗證
        3.2.1 矩陣的定義
        3.2.2 矩陣運算及基本性質(zhì)
    3.3 本章小結
第四章 具體類型矩陣形式化
    4.1 實數(shù)矩陣
    4.2 復數(shù)矩陣
    4.3 實數(shù)函數(shù)矩陣
        4.3.1 函數(shù)域
        4.3.2 函數(shù)矩陣
        4.3.3 二重積分
        4.3.4 函數(shù)矩陣微積分
    4.4 本章小結
第五章 飛行控制系統(tǒng)中坐標系轉換矩陣驗證實例
    5.1 轉換矩陣的驗證
    5.2 運動學方程驗證
    5.3 本章小結
第六章 總結與展望
    6.1 研究工作總結
    6.2 未來工作展望
參考文獻
致謝
在學期間的研究成果及發(fā)表的學術論文



本文編號：3676894