B方法

第一部分 數學
第1章 數學推理
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 一些經典結果
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 一些經典結果
1.4 等式
1.5 有序對
1.6 練習
第2章 集合形式
2.1 基本集合結構
2.1.1 語法
2.1.2 公理
2.1.3 性質
2.2 類型檢查
2.3 派生結構
2.3.1 定義
2.3.2 實例
2.3.3 類型檢查
2.3.4 性質
2.4 二元關系
2.4.1 二元關系結構：第一組
2.4.2 二元關系結構：第二組
2.4.3 二元關系結構的實例
2.4.4 二元關系結構的類型檢查
2.5 函數
2.5.1 函數構造：第一組
2.5.2 函數構造：第二組
2.5.3 函數構造的示例
2.5.4 函數求值的性質
2.5.5 函數構造的類型檢查
2.6 分類的性質
2.6.1 有關成員關系的法則
2.6.2 單調性法則
2.6.3 包含法則
2.6.4 相等法則
2.7 例子
2.8 練習
參考文獻
第3章 數學對象
3.1 廣義的交和并
3.2 構造數學對象
3.2.1 非形式的引言
3.2.2 不動點
3.2.3 歸納原理
3.3 一個集合的有窮子集的集合
3.4 有窮集合和無窮集合
3.5 自然數
3.5.1 定義
3.5.2 皮阿諾“公理”
3.5.3 最小值
3.5.4 強歸納原理
3.5.5 最大值
3.5.6 自然數上的遞歸函數
3.5.7 算術
3.5.8 關系的迭代
3.5.9 有窮集的勢
3.5.10 關系的傳遞閉包
3.6 整數
3.7 有窮序列
3.7.1 歸納構造
3.7.2 直接構造
3.7.3 序列上的運算
3.7.4 排序及相關問題
3.7.5 整數序列的字典序
3.8 有窮樹
3.8.1 非形式的介紹
3.8.2 形式化構造
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 良構關系
3.11.1 定義
3.11.2 在良構集上通過歸納進行證明
3.11.3 在良構集上的遞歸
3.11.4 良構性的證明
3.11.5 一個良構關系實例
3.11.6 非經典遞歸的其他實例
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 參數化和初始化
4.9 帶有輸入參數的操作
4.10 帶有輸出參數的操作
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 關于常量
5.2.5 證明義務
5.2.6 關于給定集合和預定義常量
參考文獻
第6章 抽象機理論
6.1 規(guī)范型
6.2 兩個有用的性質
6.3 終止性、可行性和前－后謂詞
6.3.1 終止性
6.3.2 可行性
6.3.3 前－后謂詞
6.4 集合論模型
6.4.1 第一個模型——一個集合和一個關系
6.4.2 第二個模型——集合變換器
6.4.3 各種結構的集合論解釋
6.5 練習
第7章 大型抽象機
7.1 多重廣義代換
7.1.1 定義
7.1.2 基本性質
7.1.3 主要結果
7.2 規(guī)范的遞增描述
7.2.1 非形式的介紹
7.2.2 操作調用
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 練習
參考文獻
第三部分 程序設計
第9章 順序和循環(huán)
9.1 順序
9.1.1 語法
9.1.2 公理
9.1.3 基本性質
9.2 循環(huán)
9.2.1 引論
9 2 2 定義
9.2.3 循環(huán)終止的解釋
9.2.4 循環(huá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章 程序設計實例
10.0 方法學
10.0.1 重用前面的算法
10.0.2 循環(huán)結構的證明規(guī)則
10.0.3 順序結構的證明規(guī)則
10.1 無約束搜索
10.1.1 引言
10.1.2 比較兩個序列
10.1.3 計算一個函數的自然數逆
10.1.4 自然數的除法
10.1.5 遞歸函數的特殊情況
10.1.6 給定底的對數
10.1.7 整數平方根
10.2 有約束搜索
10.2.1 引言
10.2.2 線性搜索
10.2.3 在數組中的線性搜索
10.2.4 在矩陣里的線性檢索
10.2.5 二分搜索
10.2.6 再論單調函數
10.2.7 數組里的二分搜索
10.3 自然數
10.3.1 基本模式
10.3.2 自然數求冪
10.3.3 擴展基本模式
10.3.4 對序列求和
10.3.5 子數列移位
10.3.6 向排序的數組中插入
10.4 序列
10.4.1 引言
10.4.2 累計序列里的元素
10.4.3 數的基數表示
10.4.4 將自然數轉換為基數表示
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 單調性
11.1.5 廣義賦值的精化
11.2 抽象機的精化
11.2.1 非形式的討論
11.2.2 形式定義
11.2.3 充分條件
11.2.4 單調性
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章 構造大型抽象機
12.1 精化的實現
12.1.1 引言
12.1.2 有關引入的實際考慮
12.1.3 IMPLEMENTATION結構
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 在實現中允許出現的各種結構
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)結構
12.4 多重精化和實現
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 實例研究：數據庫系統(tǒng)
13.2.1 有關文件的機器
13.2.2 有關對象的機器
13.2.3 一個數據庫
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ī)范和設計
13.4.6 最后的體系結構
13.4.7 修改初始規(guī)范
參考文獻
附錄
附錄A 記法綜述
附錄B 語法
附錄C 定義
附錄D 可見性規(guī)則
附錄E 規(guī)則和公理
附錄F 證明義務