高級語言程序變換的機械化證明導論

目錄
《信息科學技術(shù)學術(shù)著作叢書》序
前言
第1章　機械化定理證明的原理和邏輯基礎(chǔ)　1
1.1　基于消解的一階邏輯自動定理證明　2
1.1.1　消解規(guī)則和證明　2
1.1.2　置換和合一　5
1.1.3　可滿足性　6
1.1.4　消解證明技術(shù)的影響　6
1.2　自然演繹和Curry-Howard同構(gòu)　7
1.2.1　自然演繹　7
1.2.2　類型化的？　演算　10
1.2.3　Curry-Howard同構(gòu)　13
1.2.4　Curry-Howard同構(gòu)的擴展　14
1.3　編程邏輯　15
1.3.1　編程語言的語義　16
1.3.2　一階編程邏輯及變體　21
1.3.3　弗洛伊德-霍爾邏輯　25
1.3.4　可計算函數(shù)邏輯　26
1.4　基于高階邏輯的硬件設計驗證　27
1.4.1　高階邏輯的硬件設計　29
1.4.2　高階邏輯的硬件設計驗證機制　31
1.5　程序構(gòu)造和求精　32
1.5.1　算法和數(shù)據(jù)求精及基于不變式的程序構(gòu)造　32
1.5.2　求精映射和行為時序邏輯　35
1.6　本章小結(jié)　36
參考文獻　37
第2章　證明助手的開發(fā)和實現(xiàn)　46
2.1　證明助手的設計特點比較　47
2.2　Isabelle的開發(fā)和實現(xiàn)　49
2.2.1　Isabelle開發(fā)背景　50
2.2.2　Isabelle/Pure啟動　51
2.2.3　Isabelle/Pure元邏輯　52
2.2.4　內(nèi)部語法分析和變換　59
2.2.5　外部語法分析和Isar/VM解釋器　66
2.3　Isabelle/HOL的開發(fā)和實現(xiàn)　73
2.3.1　Isabelle/HOL核心邏輯　73
2.3.2　Isabelle/HOL推理規(guī)則　76
2.3.3　Isabelle/HOL高級定義性機制　77
2.3.4　Isabelle/HOL證明工具　82
2.4　其他證明助手的設計和開發(fā)　84
2.4.1　Coq　84
2.4.2　NuPRL　85
2.4.3　ACL2　85
2.4.4　PVS　86
2.5　本章小結(jié)　86
參考文獻　87
第3章　機械化定理證明的應用研究　89
3.1　數(shù)學證明的機械化　89
3.1.1　開普勒猜想　91
3.1.2　四色定理　92
3.1.3　質(zhì)數(shù)定理　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　操作系統(tǒng)微內(nèi)核驗證　143
3.3.1　安全的操作系統(tǒng)微內(nèi)核源程序　144
3.3.2　微內(nèi)核源程序到ARM機器碼的翻譯確認　145
3.4　硬件設計驗證　147
3.4.1　基于Boyer-Moore計算邏輯的硬件設計驗證　148
3.4.2　基于高階邏輯的硬件設計驗證　148
3.5　本章小結(jié)　149
參考文獻　149
第4章　驗證編譯器的開發(fā)和實現(xiàn)　155
4.1　簡單算術(shù)表達式編譯器的正確性　155
4.1.1　單遍編譯算術(shù)表達式　155
4.1.2　兩遍編譯算術(shù)表達式　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程序優(yōu)化變換的正確性　172
4.3.1　等同和條件等同　172
4.3.2　常量折疊和傳播　173
4.3.3　改進的常量折疊和傳播　178
4.3.4　活性分析和消除冗余賦值語句　181
4.3.5　改進的活性分析　185
4.4　基于寄存器傳輸語言優(yōu)化變換的正確性　187
4.4.1　構(gòu)建控制流圖　187
4.4.2　常量傳播　197
4.4.3　公共子表達式消除　202
4.5　本章小結(jié)　207
參考文獻　207
第5章　總結(jié)和展望　208
5.1　總結(jié)　208
5.2　展望　209
5.2.1　編程語言的設計和實現(xiàn)　209
5.2.2　并發(fā)程序的機械化證明　214
5.2.3　面向?qū)ο笳Z言的編譯器驗證　217
5.2.4　更加強大的證明助手的開發(fā)　218
參考文獻　219