B方法

第一部分 數(shù)學(xué)
第1章 數(shù)學(xué)推理
1.1 形式推理
1.1.1 相繼式和謂詞
1.1.2 推理規(guī)則
1.1.3 證明
1.1.4 基本規(guī)則
1.2 命題演算
1.2.1 基本斷言的記法形式
1.2.2 命題邏輯的推理規(guī)則
1.2.3 一些證明
1.2.4 一個(gè)證明過程
1.2.5 擴(kuò)充記法形式
1.2.6 一些經(jīng)典結(jié)果
1.3 謂詞演算
1.3.1 量化謂詞和代換的記法形式
1.3.2 全稱量化公式
1.3.3 非自由性
1.3.4 代換
1.3.5 謂詞演算的推理規(guī)則
1.3.6 若干證明
1.3.7 擴(kuò)充的證明過程
1.3.8 存在量化公式
1.3.9 一些經(jīng)典結(jié)果
1.4 等式
1.5 有序?qū)?br />1.6 練習(xí)
第2章 集合形式
2.1 基本集合結(jié)構(gòu)
2.1.1 語法
2.1.2 公理
2.1.3 性質(zhì)
2.2 類型檢查
2.3 派生結(jié)構(gòu)
2.3.1 定義
2.3.2 實(shí)例
2.3.3 類型檢查
2.3.4 性質(zhì)
2.4 二元關(guān)系
2.4.1 二元關(guān)系結(jié)構(gòu)：第一組
2.4.2 二元關(guān)系結(jié)構(gòu)：第二組
2.4.3 二元關(guān)系結(jié)構(gòu)的實(shí)例
2.4.4 二元關(guān)系結(jié)構(gòu)的類型檢查
2.5 函數(shù)
2.5.1 函數(shù)構(gòu)造：第一組
2.5.2 函數(shù)構(gòu)造：第二組
2.5.3 函數(shù)構(gòu)造的示例
2.5.4 函數(shù)求值的性質(zhì)
2.5.5 函數(shù)構(gòu)造的類型檢查
2.6 分類的性質(zhì)
2.6.1 有關(guān)成員關(guān)系的法則
2.6.2 單調(diào)性法則
2.6.3 包含法則
2.6.4 相等法則
2.7 例子
2.8 練習(xí)
參考文獻(xiàn)
第3章 數(shù)學(xué)對(duì)象
3.1 廣義的交和并
3.2 構(gòu)造數(shù)學(xué)對(duì)象
3.2.1 非形式的引言
3.2.2 不動(dòng)點(diǎn)
3.2.3 歸納原理
3.3 一個(gè)集合的有窮子集的集合
3.4 有窮集合和無窮集合
3.5 自然數(shù)
3.5.1 定義
3.5.2 皮阿諾“公理”
3.5.3 最小值
3.5.4 強(qiáng)歸納原理
3.5.5 最大值
3.5.6 自然數(shù)上的遞歸函數(shù)
3.5.7 算術(shù)
3.5.8 關(guān)系的迭代
3.5.9 有窮集的勢
3.5.10 關(guān)系的傳遞閉包
3.6 整數(shù)
3.7 有窮序列
3.7.1 歸納構(gòu)造
3.7.2 直接構(gòu)造
3.7.3 序列上的運(yùn)算
3.7.4 排序及相關(guān)問題
3.7.5 整數(shù)序列的字典序
3.8 有窮樹
3.8.1 非形式的介紹
3.8.2 形式化構(gòu)造
3.8.3 歸納
3.8.4 遞歸
3.8.5 運(yùn)算
3.8.6 樹的表達(dá)
3.9 標(biāo)記樹
3.9.1 直接定義
3.9.2 歸納定義
3.9.3 歸納
3.9.4 遞歸
3.9.5 遞歸定義的運(yùn)算
3.9.6 直接定義的運(yùn)算
3.10 二叉樹
3.10.1 直接的運(yùn)算
3.10.2 歸納
3.10.3 遞歸
3.10.4 遞歸定義的運(yùn)算
3.11 良構(gòu)關(guān)系
3.11.1 定義
3.11.2 在良構(gòu)集上通過歸納進(jìn)行證明
3.11.3 在良構(gòu)集上的遞歸
3.11.4 良構(gòu)性的證明
3.11.5 一個(gè)良構(gòu)關(guān)系實(shí)例
3.11.6 非經(jīng)典遞歸的其他實(shí)例
3.12 練習(xí)
第二部分 抽象機(jī)
第4章 抽象機(jī)引論
4.1 抽象機(jī)
4.2 靜態(tài)行為——描述狀態(tài)
4.3 動(dòng)態(tài)行為——描述操作
4.4 將前－后謂詞作為規(guī)范
4.5 證明義務(wù)
4.6 代換作為規(guī)范
4.7 前條件代換（終止性）
4.8 參數(shù)化和初始化
4.9 帶有輸入?yún)?shù)的操作
4.10 帶有輸出參數(shù)的操作
4.11 規(guī)范的寬松風(fēng)格和防御風(fēng)格
4.12 多重簡單代換
4.13 條件代換
4.14 約束選擇代換
4.15 衛(wèi)式代換（可行性）
4.16 沒有任何作用的代換
4.17 上下文信息——集合和常量
4.18 無約束選擇代換
4.19 顯式定義
4.20 斷言
4.21 具體變量和抽象常量
4.22 練習(xí)
參考文獻(xiàn)
第5章 抽象機(jī)的定義
5.1 廣義代換
5.1.1 語法
5.1.2 類型檢查
5.1.3 公理
5.2 抽象機(jī)
5.2.1 語法
5.2.2 可見性規(guī)則
5.2.3 類型檢查
5.2.4 關(guān)于常量
5.2.5 證明義務(wù)
5.2.6 關(guān)于給定集合和預(yù)定義常量
參考文獻(xiàn)
第6章 抽象機(jī)理論
6.1 規(guī)范型
6.2 兩個(gè)有用的性質(zhì)
6.3 終止性、可行性和前－后謂詞
6.3.1 終止性
6.3.2 可行性
6.3.3 前－后謂詞
6.4 集合論模型
6.4.1 第一個(gè)模型——一個(gè)集合和一個(gè)關(guān)系
6.4.2 第二個(gè)模型——集合變換器
6.4.3 各種結(jié)構(gòu)的集合論解釋
6.5 練習(xí)
第7章 大型抽象機(jī)
7.1 多重廣義代換
7.1.1 定義
7.1.2 基本性質(zhì)
7.1.3 主要結(jié)果
7.2 規(guī)范的遞增描述
7.2.1 非形式的介紹
7.2.2 操作調(diào)用
7.2.3 INCLUDES子句
7.2.4 可見性規(guī)則
7.2.5 傳遞性
7.2.6 機(jī)器的重命名
7.2.7 PROMOTES和EXTENDS子句
7.2.8 實(shí)例
7.3 遞增的規(guī)范描述和規(guī)范共享
7.3.1 非形式的介紹
7.3.2 USES子句
7.3.3 可見性規(guī)則
7.3.4 傳遞性
7.3.5 機(jī)器重命名
7.4 形式定義
7.4.1 語法
7.4.2 類型檢查
7.4.3 INCLUDES子句的證明義務(wù)
7.4.4 USES子句的證明義務(wù)
7.5 練習(xí)
第8章 抽象機(jī)的實(shí)例
8.1 一個(gè)貨單系統(tǒng)
8.1.1 非形式的規(guī)范
8.1.2 機(jī)器Client
8.1.3 機(jī)器Product
8.1.4 機(jī)器Invoice
8.1.5 機(jī)器Invoice_System
8.2 電話交換機(jī)
8.2.1 非形式的規(guī)范
8.2.2 機(jī)器Simple_Exchange
8.2.3 機(jī)器Exchange
8.3 電梯控制系統(tǒng)
8.3.1 非形式的規(guī)范
8.3.2 機(jī)器Lift
8.3.3 活性（liveness）的證明
8.3.4 活性證明義務(wù)的表述
8.4 練習(xí)
參考文獻(xiàn)
第三部分 程序設(shè)計(jì)
第9章 順序和循環(huán)
9.1 順序
9.1.1 語法
9.1.2 公理
9.1.3 基本性質(zhì)
9.2 循環(huán)
9.2.1 引論
9 2 2 定義
9.2.3 循環(huán)終止的解釋
9.2.4 循環(huán)的前－后關(guān)系的解釋
9.2.5 循環(huán)終止的實(shí)例
9.2.6 不變式定理
9.2.7 變動(dòng)量定理
9.2.8 變動(dòng)量和不變式定理的進(jìn)一步實(shí)用化
9.2.9 傳統(tǒng)循環(huán)
9.3 練習(xí)
第10章 程序設(shè)計(jì)實(shí)例
10.0 方法學(xué)
10.0.1 重用前面的算法
10.0.2 循環(huán)結(jié)構(gòu)的證明規(guī)則
10.0.3 順序結(jié)構(gòu)的證明規(guī)則
10.1 無約束搜索
10.1.1 引言
10.1.2 比較兩個(gè)序列
10.1.3 計(jì)算一個(gè)函數(shù)的自然數(shù)逆
10.1.4 自然數(shù)的除法
10.1.5 遞歸函數(shù)的特殊情況
10.1.6 給定底的對(duì)數(shù)
10.1.7 整數(shù)平方根
10.2 有約束搜索
10.2.1 引言
10.2.2 線性搜索
10.2.3 在數(shù)組中的線性搜索
10.2.4 在矩陣?yán)锏木€性檢索
10.2.5 二分搜索
10.2.6 再論單調(diào)函數(shù)
10.2.7 數(shù)組里的二分搜索
10.3 自然數(shù)
10.3.1 基本模式
10.3.2 自然數(shù)求冪
10.3.3 擴(kuò)展基本模式
10.3.4 對(duì)序列求和
10.3.5 子數(shù)列移位
10.3.6 向排序的數(shù)組中插入
10.4 序列
10.4.1 引言
10.4.2 累計(jì)序列里的元素
10.4.3 數(shù)的基數(shù)表示
10.4.4 將自然數(shù)轉(zhuǎn)換為基數(shù)表示
10.4.5 二元運(yùn)算的快速計(jì)算
10.4.6 左遞歸和右遞歸
10.4.7 過濾器
10.5 樹
10.5.1 公式的記法
10.5.2 將樹變換到公式
10.5.3 從樹變換到波蘭表示串
10.5.4 將公式變換到波蘭表示串
10.6 練習(xí)
參考文獻(xiàn)
第四部分 精化
第11章 精化
11.1 廣義代換的精化
11.1.1 非形式的討論
11.1.2 形式定義
11.1.3 廣義代換的相等
11.1.4 單調(diào)性
11.1.5 廣義賦值的精化
11.2 抽象機(jī)的精化
11.2.1 非形式的討論
11.2.2 形式定義
11.2.3 充分條件
11.2.4 單調(diào)性
11.2.5 實(shí)例重溫
11.2.6 最后的潤色
11.2.7 精化條件的直觀解釋
11.2.8 對(duì)小例子的應(yīng)用
11.3 形式定義
11.3.1 語法
11.3.2 類型檢查
11.3.3 證明義務(wù)
11.4 練習(xí)
參考文獻(xiàn)
第12章 構(gòu)造大型抽象機(jī)
12.1 精化的實(shí)現(xiàn)
12.1.1 引言
12.1.2 有關(guān)引入的實(shí)際考慮
12.1.3 IMPLEMENTATION結(jié)構(gòu)
12.1.4 IMPORTS子句
12.1.5 可見性規(guī)則
12.1.6 機(jī)器重命名
12.1.7 VALUES子句
12.1.8 IMPORTS和INCLUDES子句的比較
12.1.9 PROMOTES和EXTENDS子句
12.1.10 再論具體常量和具體變量
12.1.11 在實(shí)現(xiàn)中允許出現(xiàn)的各種結(jié)構(gòu)
12.2 共享
12.2.1 引言
12.2.2 SEES子句
12.2.3 可見性
12.2.4 傳遞性和循環(huán)定義
12.2.5 機(jī)器重命名
12.2.6 USES子句和SEES子句的比較
12.3 再論循環(huán)結(jié)構(gòu)
12.4 多重精化和實(shí)現(xiàn)
12.5 遞歸定義的操作
12.5.1 引言
12.5.2 語法
12.5.3 證明規(guī)則
12.6 形式證明
12.6.1 一個(gè)IMPLEMENTATION的語法
12.6.2 對(duì)IMPORTS子句的類型檢查
12.6.3 對(duì)SEES子句的類型檢查
12.6.4 一個(gè)IMPLEMENTATION的證明義務(wù)
12.6.5 對(duì)SEES子句的證明義務(wù)
第13章 精化的實(shí)例
13.1 一個(gè)基本機(jī)器庫
13.1.1 機(jī)器BASIC_CONSTANTS
13.1.2 機(jī)器BASIC_IO
13.1.3 機(jī)器BASIC_BOOL
13.1.4 機(jī)器BASIC_enum
13.1.5 機(jī)器BASIC_FILE_VAN
13.2 實(shí)例研究：數(shù)據(jù)庫系統(tǒng)
13.2.1 有關(guān)文件的機(jī)器
13.2.2 有關(guān)對(duì)象的機(jī)器
13.2.3 一個(gè)數(shù)據(jù)庫
13.2.4 界面
13.3 一個(gè)實(shí)用的抽象機(jī)庫
13.3.1 機(jī)器ARRAY_VAR
13.3.2 機(jī)器SEQUENCE_VAR
13.3.3 機(jī)器SET_VAR
13.3.4 機(jī)器ARRAY_ECTION
13.3.5 機(jī)器SEQUENCE_COLLECTION
13.3.6 機(jī)器SET_ECTION
13.3.7 機(jī)器TREE_VAR
13.4 實(shí)例研究：鍋爐控制系統(tǒng)
13.4.1 引言
13.4.2 非形式的規(guī)范
13.4.3 系統(tǒng)分析
13.4.4 系統(tǒng)集成
13.4.5 形式化規(guī)范和設(shè)計(jì)
13.4.6 最后的體系結(jié)構(gòu)
13.4.7 修改初始規(guī)范
參考文獻(xiàn)
附錄
附錄A 記法綜述
附錄B 語法
附錄C 定義
附錄D 可見性規(guī)則
附錄E 規(guī)則和公理
附錄F 證明義務(wù)