齣版者的話
專傢指導委員會
譯者序
前言
第一章 概述
1.1 問題
1.2 淨室方法
1.3 關於本書
備注
第二章 運算函數
2.1 運算
2.2 函數錶示法並行處理
2.3 條件並行處理
2.4 局部變量
2.5 基於預期函數的規定
2.6 其他標記法簡介
2.7 預期函數的編寫
練習
備注
第三章 驗證
3.1 結構化控製語句
3.2 預期函數的定位
3.3 替換原則
3.4 代碼序列
3.5 跟蹤錶
3.6 語句
3.7 條件分支跟蹤錶
練習
備注
第四章 迭代的驗證
4.1 語句
4.2 循環中止的驗證
4.3 已初始化循環
4.4 為獨立的循環編寫預期函數
4.5 其他形式的不定迭式
練習
備注
第五章 基於預期函數的程序設計
5.1 Pascal程序：最長一行的長度
5.2 C程序：統計字符及數字的齣現次數
5.3 Icon程序：字符串解壓縮
5.4 抽象化的探討：登記注冊係統
5.5 讓事情簡單
練習
備注
第6章 驗證過程的迴顧
6.1 為什麼驗證必須迴顧
6.2 淨定過程中的驗證迴顧
6.3 驗證迴顧是如何完成的
6.4 示例：注冊登記係統的另一個例程
6.5 示例：測試數據生成器例程
6.6 示例討論
練習
備注
第7章 定迭代
7.1 序列上的定迭代
7.2 序列變量
7.3 其他序列錶達式
7.4 整型值的範圍
7.5 其他數據結構
7.6 迭代機製
7.7 程序設計中的集閤與序列
練習
備注
第8章 數據抽象與麵嚮對象編程
8.1 數據抽象與封裝
8.2 抽象函數
8.3 數據不變性
8.4 麵嚮對象編程
練習
備注
第9章 遞歸與函數語言
9.1 遞歸例程
9.2 終止
9.3 相互遞歸
9.4 函數化語言
練習
備注
第10章 測試
10.1 測試的角色
10.2 基於使用的測試
10.3 測試數據生成器
10.4 測試的其他方式
練習
備注
第11章 增量開發
11.1 用增量的方式開發程序
11.2 計劃與實現的過程
11.3 示例：排演計劃
練習
備注
第12章 我們將走嚮何方
12.1 淨室過程的其他部分
12.2 其他的形式方法
12.3 我們學會瞭什麼
12.4 展望未來
備注
部分習題的提示
參考文獻
· · · · · · (收起)