中圖網小程序
一鍵登錄
更方便
本類五星書更多>
-
>
全國計算機等級考試最新真考題庫模擬考場及詳解·二級MSOffice高級應用
-
>
決戰行測5000題(言語理解與表達)
-
>
軟件性能測試.分析與調優實踐之路
-
>
第一行代碼Android
-
>
JAVA持續交付
-
>
EXCEL最強教科書(完全版)(全彩印刷)
-
>
深度學習
高級語言程序變換的機械化證明導論/信息科學技術學術著作叢書 版權信息
- ISBN：9787030731678
- 條形碼：9787030731678 ; 978-7-03-073167-8
- 裝幀：一般膠版紙
- 冊數：暫無
- 重量：暫無
- 所屬分類：>
高級語言程序變換的機械化證明導論/信息科學技術學術著作叢書 內容簡介
隨著現代社會信息化程度的提高，與計算機相關的各種系統故障足以造成巨大的經濟損失。機械化的定理證明能夠建立更為嚴格的正確性，從而奠定系統的高可信性。本書闡述機械化定理證明的邏輯基礎和關鍵技術，分析比較各類主流證明助手的設計特點，重點討論在編譯器驗證領域取得的重要研究成果，并以實例詳述驗證編譯器的開發和實現。本書可供計算機科學與技術、信息安全、軟件工程、計算機應用技術等相關專業的高年級本科生和研究生學習，也可供從事機械化定理證明、可信軟件及相關領域的研究人員參考。
高級語言程序變換的機械化證明導論/信息科學技術學術著作叢書 目錄
目錄
《信息科學技術學術著作叢書》序
前言
第1章 機械化定理證明的原理和邏輯基礎 1
1.1 基于消解的一階邏輯自動定理證明 2
1.1.1 消解規則和證明 2
1.1.2 置換和合一 5
1.1.3 可滿足性 6
1.1.4 消解證明技術的影響 6
1.2 自然演繹和Curry-Howard同構 7
1.2.1 自然演繹 7
1.2.2 類型化的？ 演算 10
1.2.3 Curry-Howard同構 13
1.2.4 Curry-Howard同構的擴展 14
1.3 編程邏輯 15
1.3.1 編程語言的語義 16
1.3.2 一階編程邏輯及變體 21
1.3.3 弗洛伊德-霍爾邏輯 25
1.3.4 可計算函數邏輯 26
1.4 基于高階邏輯的硬件設計驗證 27
1.4.1 高階邏輯的硬件設計 29
1.4.2 高階邏輯的硬件設計驗證機制 31
1.5 程序構造和求精 32
1.5.1 算法和數據求精及基于不變式的程序構造 32
1.5.2 求精映射和行為時序邏輯 35
1.6 本章小結 36
參考文獻 37
第2章 證明助手的開發和實現 46
2.1 證明助手的設計特點比較 47
2.2 Isabelle的開發和實現 49
2.2.1 Isabelle開發背景 50
2.2.2 Isabelle/Pure啟動 51
2.2.3 Isabelle/Pure元邏輯 52
2.2.4 內部語法分析和變換 59
2.2.5 外部語法分析和Isar/VM解釋器 66
2.3 Isabelle/HOL的開發和實現 73
2.3.1 Isabelle/HOL核心邏輯 73
2.3.2 Isabelle/HOL推理規則 76
2.3.3 Isabelle/HOL高級定義性機制 77
2.3.4 Isabelle/HOL證明工具 82
2.4 其他證明助手的設計和開發 84
2.4.1 Coq 84
2.4.2 NuPRL 85
2.4.3 ACL2 85
2.4.4 PVS 86
2.5 本章小結 86
參考文獻 87
第3章 機械化定理證明的應用研究 89
3.1 數學證明的機械化 89
3.1.1 開普勒猜想 91
3.1.2 四色定理 92
3.1.3 質數定理 92
3.2 編譯器驗證 93
3.2.1 可信編譯概述 93
3.2.2 編譯器自身的正確性驗證 95
3.2.3 編譯后代碼的正確性驗證 101
3.2.4 Jinja編譯器分析 103
3.2.5 CompCert編譯器后端分析 133
3.3 操作系統微內核驗證 143
3.3.1 安全的操作系統微內核源程序 144
3.3.2 微內核源程序到ARM機器碼的翻譯確認 145
3.4 硬件設計驗證 147
3.4.1 基于Boyer-Moore計算邏輯的硬件設計驗證 148
3.4.2 基于高階邏輯的硬件設計驗證 148
3.5 本章小結 149
參考文獻 149
第4章 驗證編譯器的開發和實現 155
4.1 簡單算術表達式編譯器的正確性 155
4.1.1 單遍編譯算術表達式 155
4.1.2 兩遍編譯算術表達式 158
4.2 簡單命令式語言IMP的驗證編譯器 160
4.2.1 IMP的抽象語法 160
4.2.2 IMP的大步操作語義 161
4.2.3 IMP的編譯目標語言 163
4.2.4 編譯及正確性證明 165
4.3 IMP程序優化變換的正確性 172
4.3.1 等同和條件等同 172
4.3.2 常量折疊和傳播 173
4.3.3 改進的常量折疊和傳播 178
4.3.4 活性分析和消除冗余賦值語句 181
4.3.5 改進的活性分析 185
4.4 基于寄存器傳輸語言優化變換的正確性 187
4.4.1 構建控制流圖 187
4.4.2 常量傳播 197
4.4.3 公共子表達式消除 202
4.5 本章小結 207
參考文獻 207
第5章 總結和展望 208
5.1 總結 208
5.2 展望 209
5.2.1 編程語言的設計和實現 209
5.2.2 并發程序的機械化證明 214
5.2.3 面向對象語言的編譯器驗證 217
5.2.4 更加強大的證明助手的開發 218
參考文獻 219
《信息科學技術學術著作叢書》序
前言
第1章 機械化定理證明的原理和邏輯基礎 1
1.1 基于消解的一階邏輯自動定理證明 2
1.1.1 消解規則和證明 2
1.1.2 置換和合一 5
1.1.3 可滿足性 6
1.1.4 消解證明技術的影響 6
1.2 自然演繹和Curry-Howard同構 7
1.2.1 自然演繹 7
1.2.2 類型化的？ 演算 10
1.2.3 Curry-Howard同構 13
1.2.4 Curry-Howard同構的擴展 14
1.3 編程邏輯 15
1.3.1 編程語言的語義 16
1.3.2 一階編程邏輯及變體 21
1.3.3 弗洛伊德-霍爾邏輯 25
1.3.4 可計算函數邏輯 26
1.4 基于高階邏輯的硬件設計驗證 27
1.4.1 高階邏輯的硬件設計 29
1.4.2 高階邏輯的硬件設計驗證機制 31
1.5 程序構造和求精 32
1.5.1 算法和數據求精及基于不變式的程序構造 32
1.5.2 求精映射和行為時序邏輯 35
1.6 本章小結 36
參考文獻 37
第2章 證明助手的開發和實現 46
2.1 證明助手的設計特點比較 47
2.2 Isabelle的開發和實現 49
2.2.1 Isabelle開發背景 50
2.2.2 Isabelle/Pure啟動 51
2.2.3 Isabelle/Pure元邏輯 52
2.2.4 內部語法分析和變換 59
2.2.5 外部語法分析和Isar/VM解釋器 66
2.3 Isabelle/HOL的開發和實現 73
2.3.1 Isabelle/HOL核心邏輯 73
2.3.2 Isabelle/HOL推理規則 76
2.3.3 Isabelle/HOL高級定義性機制 77
2.3.4 Isabelle/HOL證明工具 82
2.4 其他證明助手的設計和開發 84
2.4.1 Coq 84
2.4.2 NuPRL 85
2.4.3 ACL2 85
2.4.4 PVS 86
2.5 本章小結 86
參考文獻 87
第3章 機械化定理證明的應用研究 89
3.1 數學證明的機械化 89
3.1.1 開普勒猜想 91
3.1.2 四色定理 92
3.1.3 質數定理 92
3.2 編譯器驗證 93
3.2.1 可信編譯概述 93
3.2.2 編譯器自身的正確性驗證 95
3.2.3 編譯后代碼的正確性驗證 101
3.2.4 Jinja編譯器分析 103
3.2.5 CompCert編譯器后端分析 133
3.3 操作系統微內核驗證 143
3.3.1 安全的操作系統微內核源程序 144
3.3.2 微內核源程序到ARM機器碼的翻譯確認 145
3.4 硬件設計驗證 147
3.4.1 基于Boyer-Moore計算邏輯的硬件設計驗證 148
3.4.2 基于高階邏輯的硬件設計驗證 148
3.5 本章小結 149
參考文獻 149
第4章 驗證編譯器的開發和實現 155
4.1 簡單算術表達式編譯器的正確性 155
4.1.1 單遍編譯算術表達式 155
4.1.2 兩遍編譯算術表達式 158
4.2 簡單命令式語言IMP的驗證編譯器 160
4.2.1 IMP的抽象語法 160
4.2.2 IMP的大步操作語義 161
4.2.3 IMP的編譯目標語言 163
4.2.4 編譯及正確性證明 165
4.3 IMP程序優化變換的正確性 172
4.3.1 等同和條件等同 172
4.3.2 常量折疊和傳播 173
4.3.3 改進的常量折疊和傳播 178
4.3.4 活性分析和消除冗余賦值語句 181
4.3.5 改進的活性分析 185
4.4 基于寄存器傳輸語言優化變換的正確性 187
4.4.1 構建控制流圖 187
4.4.2 常量傳播 197
4.4.3 公共子表達式消除 202
4.5 本章小結 207
參考文獻 207
第5章 總結和展望 208
5.1 總結 208
5.2 展望 209
5.2.1 編程語言的設計和實現 209
5.2.2 并發程序的機械化證明 214
5.2.3 面向對象語言的編譯器驗證 217
5.2.4 更加強大的證明助手的開發 218
參考文獻 219
展開全部
高級語言程序變換的機械化證明導論/信息科學技術學術著作叢書 節選
第1章 機械化定理證明的原理和邏輯基礎 機械化定理證明是指使用計算機，以定理證明的方式對數學定理、計算機軟硬件系統進行形式驗證。這種機器智能的獲得可歸功于20世紀下半葉形式推理系統在計算機上的實現。20世紀50年代，機械化的定理證明圍繞計算機如何高度自動化地完成證明展開，旨在證明數學定理。完全自動定理證明的局限性，以及來自數學領域之外，特別是計算機領域程序和硬件設計驗證的需求，催生了60年代晚期交互式定理證明技術的出現。交互式定理證明工具應該盡可能地提供強大的自動證明能力。因此，我們從一階邏輯（first-order logic）和基于消解（resolution-based）的證明技術展開論述。 相比基于消解的證明技術，自然演繹風格的推理更加自然。大多數交互式定理證明工具可以實現自然演繹形式的推理規則。自然演繹推理與類型化.演算之間的對應關系，以及Curry-Howard同構的發現，使邏輯學家和計算機科學家基于證明和程序之間的對應關系開發了一類強大的、以類型理論為基礎的交互式定理證明工具。因此，本章接下來討論自然演繹和Curry-Howard同構。 程序驗證的巨大需求極大地推動了編程邏輯的研究，以及相應工具的實現。三種具有重要影響力的編程邏輯包括一階編程邏輯、弗洛伊德-霍爾邏輯（Floyd-Hoare logic）和可計算函數邏輯（logic for computable functions，LCF）。對程序進行推理可以直接作用在編程語言的語義上，也可以使用特定的針對程序驗證而開發的邏輯，如弗洛伊德-霍爾邏輯。因此，本章還討論編程語言的語義和編程邏輯。 Gordon曾開發了一種相當激進，卻很成功的基于高階邏輯（higher order logic，HOL）的硬件驗證技術。由此產生的各種工具在硬件驗證領域，甚至軟件驗證和數學領域都發揮了重要作用。因此，本章還討論基于高階邏輯的硬件設計驗證。 相比程序驗證的后驗方式，程序構造是一種構造即正確的技術。早期機械化程序構造采用基于消解的技術，之后許多研究者探索了逐步求精的程序構造，在并發程序驗證領域結合時序邏輯進行深入研究，以尋求更好的機械化支持。因此，本章*后討論這些技術。 1.1基于消解的一階邏輯自動定理證明 自動定理證明要解決的主要問題如下。 （1）知識如何展現，即用什么語言表述定理。 （2）如何由已有的知識推導得到新的知識，即由已有定理（公理）推導新定理的推理規則。 （3）如何找到證明，即控制推理規則的使用。 自動定理證明*初使用相對簡單的命題邏輯語言，但是命題邏輯所能表述的定理具有很大的限制性。相比而言，一階謂詞邏輯（簡稱一階邏輯）具有更強的表述力和理論上的完備性，因此自動定理證明轉而采用一階邏輯。 后兩個問題的解決相對更困難一些。通常，經驗、洞察力，甚至直覺對定理的證明都會起到很大的作用。開發自動定理證明工具需要找到適合機器推理的方法。20世紀50年代中期，Quine[1]、Beth[2]、Hintikka[3]、Schütte[4]、Kanger[5]等獨立發表了他們的研究成果。這些成果直接影響定理證明工具的設計。1957年，Prawitz使用自己設計的語言編寫了用于證明一階公式的程序。其基本思想是反駁證明法，即為了證明公式F，先假定F為假，然后推出矛盾。之后，他的父親將該程序翻譯為機器碼，并在計算機上進行測試[7]。幾乎同一時期，Gilmore加入國際商業機器公司（International Business Machines Corporation，IBM）的歐氏幾何定理證明項目。他使用匯編語言，在IBM704上實現了Beth的semantic tableaux證明過程[8]。Prawitz[9]進一步提出合一的方法，改進了常量置換的方式。此后，許多合一算法都使用類似的計算方式。Davis等[10]考慮Skolem函數，使算法可以直接處理函數符號和Herbrand域。同時，他們提出待反駁公式的子句形式。這些子句形式成為反駁證明法的標準。Davis等提出的反駁法和單文字子句的消除規則，稱為單元消解法。這是一種比Gilmore程序更有效的證明技術。在這些研究成果的推動下，Robinson[11]重新發現合一和消解規則（resolution rule/principle），并以優雅的方式將這兩種功能強大的技術在IBM704上實現，稱為基于消解的證明技術。 1.1.1消解規則和證明 消解規則形如下式，即 該規則表示如果兩個子句都為真，那么可以推出為真。Robinson證明了僅具有這樣一條消解規則的一階邏輯系統的完備性。 基于消解技術的證明基于以下事實，即是合法的，當且僅當是不可滿足的。因此，基于消解技術的證明算法是一種反駁法，首先否定待證明結論，與所有前提條件用邏輯與聯結，得到一個新公式，然后運用消解規則進行推導，*后證明該公式的不可滿足性。 為了運用消解規則，需要將待證明不可滿足的公式轉換為合取范式（conjunctive normal form，CNF）。該范式的所有合取分量形成子句集。在該集合中，對所有可能的具有互補文字的子句運用消解規則，將得到的新子句（消解子）加入子句集中。該過程被重復進行，直到不能再運用消解規則產生新子句，或者運用消解規則產生空子句。空子句表示初始推測的否是矛盾式，因此初始推測就是定理。如果不能得到空子句，那么初始推測就不是定理。例如，采用基于消解的技術證明以下命題邏輯公式，即 首先對該公式取否，然后將命題演算等值式轉換為CNF。轉換過程如圖1.1所示。為了方便，我們將CNF的9個合取分量從左至右編號為①～⑨。然后，運用消解規則進行證明。證明時，首先在子句①和⑦上運用消解規則，消去互補文字對S和.S，得到消解子P R Q，然后在消解子和子句⑥上運用消解規則，消去互補文字對R和.R，得到消解子P Q，繼續運用消解規則，*后推出空子句。因此，該命題邏輯公式是永真式，證明結束。命題邏輯公式的消解證明如圖1.2所示。 圖1.1命題邏輯公式轉換為CNF 圖1.2命題邏輯公式的消解證明 基于消解的證明技術適合機器推理，但是需要開發更多的控制技術來加速空子句的產生，提高證明效率。 由于量詞和變量的出現，運用消解規則證明一階邏輯公式比命題邏輯公式更為復雜。在運用消解規則之前，為了消除量詞，一般將公式轉換成前束范式（prenex normal form，PNF）。消去存在量詞后的PNF稱為Skolem標準形。為了消除存在量詞，考慮以下兩種情況。 （1）獨立存在量詞的消除。如果存在量詞不出現在任何全稱量詞之后，那么用某個Skolem常量替換該存在量詞所量化的變量，并消除該存在量詞。例如，.x （x）轉換為.（a），其中a是引入的Skolem常量。 （2）依賴存在量詞的消除。如果存在量詞出現在i個全稱量詞之后，設這些全稱量詞量化的變量分別為，則用Skolem函數替換該存在量詞量化的變量，消除該存在量詞。例如，轉換為，其中量化變量y1和y2出現在一個全稱量詞之后。該全稱量詞量化的變量是x1，因此引入兩個Skolem函數f（x1）和g（x1），消除這兩個存在量詞。量化變量y3的存在量詞出現在兩個全稱量詞之后。這兩個全稱量詞量化的變量是x1和x2，因此再引入Skolem函數h（x1，x2），消除量化在y3上的存在量詞。 1.1.2置換和合一 消解規則運用到一階邏輯公式上時，需要考慮變量的置換問題。例如，假設子句集是。為了運用消解規則，需要匹配P（x）和.P（a），因此可將x置換為a，記為。置換后，得到的新子句集為。運用消解規則消除互補謂詞公式對P（a）和.P（a），可以得到新的子句集。Robinson提出的合一算法雖然被成功地實現，但是效率很低。從計算復雜度的角度考慮，一種線性時間復雜度的合一算法由Martelli等[12]于1976年提出。Paterson等[13]于1978年提出更有效的算法。Martelli等[14]針對一階謂詞演算的合一問題，于1982年提出找到*一般合一子（most general unifier），即*一般置換（most general substitution）算法，并用Pascal語言編程實現該算法。下面對該算法簡單介紹。 設有一系列表達式，θ是一個置換，記Eiθ是按照θ進行置換的結果表達式，稱為Ei的實例。如果，則稱是的合一子。如果存在合一子，則稱是可合一的。例如，令，則，因此E1和E2是可合一的。 合一子不一定唯一。例如，令，因此θ2也是一個合一子。事實上，E1和E2的合一子還可以是和等。當有多個合一子時，需要具有唯一性的*一般合一子。 為了找到*一般合一子，首先需要定義作用在兩個置換上的一個運算，即置換復合。設有兩個置換θ1和θ2，記θ1°θ2為置換復合，令，則。如果，則刪除；如果，則刪除。如果對于的每個合一子，都存在一個置換，使，則稱合一子的*一般合一子。例如，和的*一般合一子，其解釋都是E1和E1合一子；對于θ1，存在一個置換，存在一個置換。對于θ3和θ4等，都可以類似推出。 下面給出利用消解規則證明一階謂詞公式的簡單例子。假定待證明的公式是。首先，將待證明的公式取否，得到。然后，使用命題演算等值式進行替換，可依次得到和。繼續使用量詞否定等值式，得到。 利用獨立存在量詞消除規則，引入常量替換為，因此可得。*后，進行變量置換，得到。運用消解規則進行推理，產生空子句，因此得證。 1.1.3可滿足性 消解規則圍繞公式的可滿足性進行。Davis等在1960年的論文中定義了命題邏輯公式是否可滿足（satisfiable），即布爾可滿足性問題，也稱SAT。SAT是首*被證明的NP完全問題，因其在理論和工業應用的重要意義受到廣泛關注。之后，Davis等[15]進一步提出著名的DPLL算法，成為當前許多SAT求解器的基礎算法。 在SAT基礎之上，可滿足性模理論（satisfiability modulo theories，SMT）集成SAT求解器和邏輯理論的判定過程，可以處理具有相等的一階邏輯公式。在實際應用中，程序驗證可能需要組合多個邏輯理論，如算術理論、實數理論、各種數據結構等。Nelson等[16]于1979年提出組合多個理論的判定方法，簡稱N.O.方法。他們使用該方法開發了工具Simplifer，用在斯坦福的Pascal程序驗證器中。N.O.方法也是許多組合理論判定方法的基礎。Bozzano等[17]于2006年提出一種新的組合理論判定方法，稱為延遲理論組合（delayed theory combination，DTC）。N.O.方法將多個理論的判定過程組合成一個求解器，再與SAT求解器進行交互。不同于這種處理方式，DTC方法將每個理論都直接與SAT交互，并且只與SAT交互。 當前許多成熟的SMT求解器在組合理論的判定方法上大多基于N.O.和DTC方法[18]，并做了進一步改進。微軟公司開發的SMT求解器Z3是一個強大的自動定理證明工具[19]。SRIInternational研發的SMT求解器Yices已經集成在PVS定理證明工具中。Alt-Ergo求解器由法國國家信息與自動化研究所研發，CamlPro公司維護。劉堯等[20]開發了NuTL2PFG工具，用來判定線性μ演算（vTL）公式的可滿足性。 SMT求解器常用于程序驗證，即將程序需要滿足的前后置條件、循環條件，以及斷言翻譯成SMT公式，然后用SMT求解器判定這些公式的可滿足性，確定程序的性質是存在的。一個基于Z3的程序驗證器是，也稱為靜態程序驗證器。Alt-Ergo求解器用于Why3、SPARK，以及Atel
書友推薦
- >
有舍有得是人生
- >
新文學天穹兩巨星--魯迅與胡適/紅燭學術叢書(紅燭學術叢書)
- >
【精裝繪本】畫給孩子的中國神話
- >
羅庸西南聯大授課錄
- >
名家帶你讀魯迅:朝花夕拾
- >
伯納黛特,你要去哪(2021新版)
- >
伊索寓言-世界文學名著典藏-全譯本
- >
回憶愛瑪儂
本類暢銷
