B方法

第一部分 數(shù)學
第1章 數(shù)學推理
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 一個證明過程
1.2.5 擴充記法形式
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 擴充的證明過程
1.3.8 存在量化公式
1.3.9 一些經(jīng)典結(jié)果
1.4 等式
1.5 有序?qū)?br />1.6 練習
第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 實例
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)的實例
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 練習
參考文獻
第3章 數(shù)學對象
3.1 廣義的交和并
3.2 構(gòu)造數(shù)學對象
3.2.1 非形式的引言
3.2.2 不動點
3.2.3 歸納原理
3.3 一個集合的有窮子集的集合
3.4 有窮集合和無窮集合
3.5 自然數(shù)
3.5.1 定義
3.5.2 皮阿諾“公理”
3.5.3 最小值
3.5.4 強歸納原理
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 序列上的運算
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 運算
3.8.6 樹的表達
3.9 標記樹
3.9.1 直接定義
3.9.2 歸納定義
3.9.3 歸納
3.9.4 遞歸
3.9.5 遞歸定義的運算
3.9.6 直接定義的運算
3.10 二叉樹
3.10.1 直接的運算
3.10.2 歸納
3.10.3 遞歸
3.10.4 遞歸定義的運算
3.11 良構(gòu)關(guān)系
3.11.1 定義
3.11.2 在良構(gòu)集上通過歸納進行證明
3.11.3 在良構(gòu)集上的遞歸
3.11.4 良構(gòu)性的證明
3.11.5 一個良構(gòu)關(guān)系實例
3.11.6 非經(jīng)典遞歸的其他實例
3.12 練習
第二部分 抽象機
第4章 抽象機引論
4.1 抽象機
4.2 靜態(tài)行為——描述狀態(tài)
4.3 動態(tài)行為——描述操作
4.4 將前－后謂詞作為規(guī)范
4.5 證明義務
4.6 代換作為規(guī)范
4.7 前條件代換（終止性）
4.8 參數(shù)化和初始化
4.9 帶有輸入?yún)?shù)的操作
4.10 帶有輸出參數(shù)的操作
4.11 規(guī)范的寬松風格和防御風格
4.12 多重簡單代換
4.13 條件代換
4.14 約束選擇代換
4.15 衛(wèi)式代換（可行性）
4.16 沒有任何作用的代換
4.17 上下文信息——集合和常量
4.18 無約束選擇代換
4.19 顯式定義
4.20 斷言
4.21 具體變量和抽象常量
4.22 練習
參考文獻
第5章 抽象機的定義
5.1 廣義代換
5.1.1 語法
5.1.2 類型檢查
5.1.3 公理
5.2 抽象機
5.2.1 語法
5.2.2 可見性規(guī)則
5.2.3 類型檢查
5.2.4 關(guān)于常量
5.2.5 證明義務
5.2.6 關(guān)于給定集合和預定義常量
參考文獻
第6章 抽象機理論
6.1 規(guī)范型
6.2 兩個有用的性質(zhì)
6.3 終止性、可行性和前－后謂詞
6.3.1 終止性
6.3.2 可行性
6.3.3 前－后謂詞
6.4 集合論模型
6.4.1 第一個模型——一個集合和一個關(guān)系
6.4.2 第二個模型——集合變換器
6.4.3 各種結(jié)構(gòu)的集合論解釋
6.5 練習
第7章 大型抽象機
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 機器的重命名
7.2.7 PROMOTES和EXTENDS子句
7.2.8 實例
7.3 遞增的規(guī)范描述和規(guī)范共享
7.3.1 非形式的介紹
7.3.2 USES子句
7.3.3 可見性規(guī)則
7.3.4 傳遞性
7.3.5 機器重命名
7.4 形式定義
7.4.1 語法
7.4.2 類型檢查
7.4.3 INCLUDES子句的證明義務
7.4.4 USES子句的證明義務
7.5 練習
第8章 抽象機的實例
8.1 一個貨單系統(tǒng)
8.1.1 非形式的規(guī)范
8.1.2 機器Client
8.1.3 機器Product
8.1.4 機器Invoice
8.1.5 機器Invoice_System
8.2 電話交換機
8.2.1 非形式的規(guī)范
8.2.2 機器Simple_Exchange
8.2.3 機器Exchange
8.3 電梯控制系統(tǒng)
8.3.1 非形式的規(guī)范
8.3.2 機器Lift
8.3.3 活性（liveness）的證明
8.3.4 活性證明義務的表述
8.4 練習
參考文獻
第三部分 程序設(shè)計
第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)終止的實例
9.2.6 不變式定理
9.2.7 變動量定理
9.2.8 變動量和不變式定理的進一步實用化
9.2.9 傳統(tǒng)循環(huán)
9.3 練習
第10章 程序設(shè)計實例
10.0 方法學
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 比較兩個序列
10.1.3 計算一個函數(shù)的自然數(shù)逆
10.1.4 自然數(shù)的除法
10.1.5 遞歸函數(shù)的特殊情況
10.1.6 給定底的對數(shù)
10.1.7 整數(shù)平方根
10.2 有約束搜索
10.2.1 引言
10.2.2 線性搜索
10.2.3 在數(shù)組中的線性搜索
10.2.4 在矩陣里的線性檢索
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 擴展基本模式
10.3.4 對序列求和
10.3.5 子數(shù)列移位
10.3.6 向排序的數(shù)組中插入
10.4 序列
10.4.1 引言
10.4.2 累計序列里的元素
10.4.3 數(shù)的基數(shù)表示
10.4.4 將自然數(shù)轉(zhuǎn)換為基數(shù)表示
10.4.5 二元運算的快速計算
10.4.6 左遞歸和右遞歸
10.4.7 過濾器
10.5 樹
10.5.1 公式的記法
10.5.2 將樹變換到公式
10.5.3 從樹變換到波蘭表示串
10.5.4 將公式變換到波蘭表示串
10.6 練習
參考文獻
第四部分 精化
第11章 精化
11.1 廣義代換的精化
11.1.1 非形式的討論
11.1.2 形式定義
11.1.3 廣義代換的相等
11.1.4 單調(diào)性
11.1.5 廣義賦值的精化
11.2 抽象機的精化
11.2.1 非形式的討論
11.2.2 形式定義
11.2.3 充分條件
11.2.4 單調(diào)性
11.2.5 實例重溫
11.2.6 最后的潤色
11.2.7 精化條件的直觀解釋
11.2.8 對小例子的應用
11.3 形式定義
11.3.1 語法
11.3.2 類型檢查
11.3.3 證明義務
11.4 練習
參考文獻
第12章 構(gòu)造大型抽象機
12.1 精化的實現(xiàn)
12.1.1 引言
12.1.2 有關(guān)引入的實際考慮
12.1.3 IMPLEMENTATION結(jié)構(gòu)
12.1.4 IMPORTS子句
12.1.5 可見性規(guī)則
12.1.6 機器重命名
12.1.7 VALUES子句
12.1.8 IMPORTS和INCLUDES子句的比較
12.1.9 PROMOTES和EXTENDS子句
12.1.10 再論具體常量和具體變量
12.1.11 在實現(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 機器重命名
12.2.6 USES子句和SEES子句的比較
12.3 再論循環(huán)結(jié)構(gòu)
12.4 多重精化和實現(xiàn)
12.5 遞歸定義的操作
12.5.1 引言
12.5.2 語法
12.5.3 證明規(guī)則
12.6 形式證明
12.6.1 一個IMPLEMENTATION的語法
12.6.2 對IMPORTS子句的類型檢查
12.6.3 對SEES子句的類型檢查
12.6.4 一個IMPLEMENTATION的證明義務
12.6.5 對SEES子句的證明義務
第13章 精化的實例
13.1 一個基本機器庫
13.1.1 機器BASIC_CONSTANTS
13.1.2 機器BASIC_IO
13.1.3 機器BASIC_BOOL
13.1.4 機器BASIC_enum
13.1.5 機器BASIC_FILE_VAN
13.2 實例研究：數(shù)據(jù)庫系統(tǒng)
13.2.1 有關(guān)文件的機器
13.2.2 有關(guān)對象的機器
13.2.3 一個數(shù)據(jù)庫
13.2.4 界面
13.3 一個實用的抽象機庫
13.3.1 機器ARRAY_VAR
13.3.2 機器SEQUENCE_VAR
13.3.3 機器SET_VAR
13.3.4 機器ARRAY_ECTION
13.3.5 機器SEQUENCE_COLLECTION
13.3.6 機器SET_ECTION
13.3.7 機器TREE_VAR
13.4 實例研究：鍋爐控制系統(tǒng)
13.4.1 引言
13.4.2 非形式的規(guī)范
13.4.3 系統(tǒng)分析
13.4.4 系統(tǒng)集成
13.4.5 形式化規(guī)范和設(shè)計
13.4.6 最后的體系結(jié)構(gòu)
13.4.7 修改初始規(guī)范
參考文獻
附錄
附錄A 記法綜述
附錄B 語法
附錄C 定義
附錄D 可見性規(guī)則
附錄E 規(guī)則和公理
附錄F 證明義務