高級(jí)語(yǔ)言程序變換的機(jī)械化證明導(dǎo)論

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