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

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

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

【文章目錄】：
摘要
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)結(jié)構(gòu)
        2.2.2 Coq中的數(shù)據(jù)類型及語法
        2.2.3 Coq中的證明方法
    2.3 Coq標(biāo)準(zhǔn)庫及第三方庫
        2.3.1 Coq標(biāo)準(zhǔn)庫
        2.3.2 mathcomp庫
        2.3.3 Coquelicot庫
    2.4 Coq相關(guān)應(yīng)用
    2.5 本章小結(jié)
第三章 基于Record類型的矩陣實現(xiàn)
    3.1 向量的定義與驗證
        3.1.1 向量的定義
        3.1.2 向量運(yùn)算及基本性質(zhì)
    3.2 矩陣的定義與驗證
        3.2.1 矩陣的定義
        3.2.2 矩陣運(yùn)算及基本性質(zhì)
    3.3 本章小結(jié)
第四章 具體類型矩陣形式化
    4.1 實數(shù)矩陣
    4.2 復(fù)數(shù)矩陣
    4.3 實數(shù)函數(shù)矩陣
        4.3.1 函數(shù)域
        4.3.2 函數(shù)矩陣
        4.3.3 二重積分
        4.3.4 函數(shù)矩陣微積分
    4.4 本章小結(jié)
第五章 飛行控制系統(tǒng)中坐標(biāo)系轉(zhuǎn)換矩陣驗證實例
    5.1 轉(zhuǎn)換矩陣的驗證
    5.2 運(yùn)動學(xué)方程驗證
    5.3 本章小結(jié)
第六章 總結(jié)與展望
    6.1 研究工作總結(jié)
    6.2 未來工作展望
參考文獻(xiàn)
致謝
在學(xué)期間的研究成果及發(fā)表的學(xué)術(shù)論文



本文編號：3676894