20世紀后半葉，計算機的計算能力得到了極大的提高。現今的計算機比曾經的計算機速度快得多得多，它們內存更大，日常能夠與世界各地的遠程計算機進行通信——而且能夠安放在一張桌子上。但是，盡管取得了這樣顯著的進步，現今的用戶仍迫切期望能夠進一步將技術發揮到極致。隨著硬件工程師建造的計算機功能日益強大，軟件為了趕上硬件的發展也必然變得復雜得多。

中規模和大規模程序設計項目需要一個團隊在可接受的時間期限內把所有的東西集成在一起。程序員如何理解自己的工作、如何將自己的工作與其他同事的工作集成在一起以達到總體指標等問題是關注的重點。如果沒有這樣的理解，了解現今的計算硬件的商業潛能實際上是不可能的。

程序設計能夠趕上硬件的巨大進展要歸功于程序設計、構造以及組織原理的相應的巨大進展。這些方法和原理的功效不言而喻——計算機技術遍及各方面——但更重要的是它們已經開始反過來影響硬件的設計。對這樣的方法的研究稱為程序設計方法學，其研究課題包括系統模型、域模型、并發、面向對象、程序規范與驗證等。

這些是本論文集的主題。

程序設計方法學

現今的大多數系統的目標是安全、可靠、易于使用和實時。為了達到這些目標，程序員需要合適的工具。這些工具在此環境中是“基于智能的”，并且包含有助于以研究人員能夠理解、計算機能夠解釋的方式組織和表示復雜問題的技術。

降低復雜性（或者只要可能，至少隱藏復雜性）的期望一直是發明設計原理和方法的動力，它們中的許多現在已經集成在普遍使用的程序設計語言和（自動）程序開發工具中。例如，類型語言可以幫助進行錯誤檢測，而面向對象語言和數據抽象（在Java中二者都存在）支持程序修改、接口級程序設計和易讀性。同時，隨著并發語言以及形式化工具（包括驗證中所使用的模型檢驗和證明幫助）的引入，并發也已經開始非常流行。

這些工具中的許多核心有深刻的理論背景——“斷言”和“程序不變量”依賴于程序設計邏輯理論；而規范和精化技術的程序語義是以它們為基礎的。本論文集中的短文集中論述構造先進應用程序的新方法和正在涌現的方法；它們要解決軟件開發人員面臨的問題，提出實際解決方案和它們的理論基礎。

匯編有關本主題論文成一本書的思想是在國際信息聯合會2.3工作小組（IFIP）的技術研討會上出現的。

工作小組2.3

IFIP的工作小組定期開會討論新的思想——他們自己的和其他人的——評價和促進計算系統的許多方面的發展趨勢。雖然他們常常提出特殊的課程和召開會議，但他們的官方作品隨小組的不同而差別很大，并且與當前成員的傳統和風格關系極大。

術語“程序設計方法學”是由WG 2.3的成員之一提出的一個新詞語，在小組內流行已將近30年，其成員對上述提到的許多課題做出了貢獻；的確，現在程序設計方法學方面許多活躍的研究領域是在WG2.3會議上曾提出和討論的。

關于本論文集

本卷論述的是該小組的第二官方出版物。我們的目的是收集能夠吸引在大學或企業工作的學生和專業人員的資料。的確，我們希望本論文集能夠作為程序設計方法學方面前沿研究活動的參考，并且能夠指導程序設計方法學方面的前沿研究活動。

課題的內容能夠反映當前成員的興趣，能夠解決與實際工作中高度復雜的應用程序的當前需求有關的具體問題。許多短文含有新的材料，能夠強調特定的理論進展，而其他的一些目的是綜述或評價某一具體領域的發展，或概述要進一步研究的發人深思的問題。

本書結構

本書包含三部分，每一部分涉及程序設計方法學的一個專題。每一部分又可以進一步分成幾小部分，每一小部分匯集重點討論這一部分主題內的某一具體課題的短文。每一小部分開始時的簡短引言可以為之后的詳細論述做準備。

系統可能很復雜，因為它們可能分布在網絡上，或者它們是時間關鍵型或并發的系統— 本書的第一部分主要論述描述、建模和分析這樣的系統的方法，第二部分集中論述專用的程序設計技術——程序員的工具包，最后一部分詳細說明一些課題的應用，包括安全性和電話學。

致謝

可以說，沒有這些文章的作者的創造性工作，就沒有本書。我們特別感謝Natarajan Shankar（WG2.3的主席），是他最先提議進行這一項目的。此外，也要特別感謝David Gries，感謝他在本書實現的過程中所給予的幫助。

Annabelle McIver

Carroll Morgan

澳大利亞，悉尼，2002

撰稿者名單
譯者序
前言
第一部分 模型與正確性
Section A 并行與交互 1
第1章 需要：并行性的組構方法 3
1.1 組構性 3
1.2 并發性的本質是干擾 4
1.3 推理干擾 5
1.4 關于假設/承諾推理的一些問題 7
1.5 寄生變量的作用 7
1.6 粒度所關心的事情 7
1.7 抽象的原子性及其精化 8
1.8 結論 8
1.9 致謝 8
參考文獻 9
第2章 用契約強制行為 11
2.1 引言 11
2.2 契約 12
2.2.1 狀態與狀態變化 12
2.2.2 契約 13
2.2.3 操作語義 14
2.2.4 契約舉例 15
2.2.5 行動系統 16
2.2.6 行動系統舉例 17
2.3 利用契約達到目標 18
2.3.1 最弱的前置條件 18
2.3.2 正確性與成功策略 20
2.3.3 契約的精化 22
2.4 強制行為屬性 23
2.4.1 分析行為 23
2.4.2 構造解釋程序 24
2.4.3 其他暫態屬性 25
2.5 分析行動系統的行為 27
2.5.1 行動系統的分類 27
2.5.2 分析行為 28
2.6 驗證強制 30
2.6.1 謂詞級正確性條件 30
2.6.2 基于不變量的方法 31
2.6.3 示范方法 32
2.6.4 例子系統中的強制性 33
2.7 結論及相關工作 36
參考文獻 36
Section B 異步邏輯方法 38
第3章 異步進展 40
3.1 引言 40
3.2 程序 41
3.3 達成 43
3.4 退耦 44
3.5 舉例——松耦合程序 45
3.6 異步安全 46
3.7 警告 47
3.8 結論 48
3.9 致謝 48
參考文獻 48
第4章 并發面向對象程序簡化定理 50
4.1 引言 50
4.2 Seuss程序設計符號 51
4.2.1 Seuss語法 52
4.2.2 Seuss語義（可選） 55
4.3 Seuss程序模型 56
4.4 對程序的限制 58
4.4.1 方框上的偏序 58
4.4.2 把過程看作關系 59
4.4.3 方框條件 60
4.5 兼容性 61
4.5.1 兼容性舉例 61
4.5.2 兼容過程的半交換性 62
4.6 簡化定理的證明 64
4.6.1 松執行 64
4.6.2 簡化方案 65
4.7 結束語 66
4.8 致謝 67
參考文獻 67
Section C 系統與實時性 68
第5章 抽象時間 70
5.1 引言 70
5.2 流 70
5.2.1 數學基礎：流 71
5.2.2 建時間模型 71
5.3 把組件看作流函數 73
5.4 時間抽象 74
5.4.1 抽象的一般概念 74
5.4.2 抽象時間 75
5.5 結論 76
5.5.1 文獻中的時間模型 76
5.5.2 結語 77
5.6 致謝 77
參考文獻 78
第6章 實時精化的謂詞語義 80
6.1 背景知識 80
6.2 語言和語義 81
6.2.1 實時規范命令 83
6.2.2 簡單實時命令 86
6.2.3 順序組合 86
6.2.4 不確定選擇、條件和挑選 88
6.2.5 局部和輔助變量 90
6.3 一個例子 91
6.4 循環 93
6.5 定時約束分析 96
6.6 結論 97
6.7 致謝 98
參考文獻 98
Section D 規定復雜的行為 100
第7章 系統描述的方面 102
7.1 引言 102
7.2 符號處理 102
7.3 機器和領域 104
7.3.1 規范接口 104
7.3.2 需求接口 104
7.3.3 系統描述 104
7.3.4 有目的的描述 105
7.3.5 為什么需要單獨的描述 106
7.4 描述實際領域 107
7.4.1 標記 107
7.4.2 使用定義 108
7.4.3 區分定義和描述 109
7.5 描述與模型 109
7.5.1 電梯模型 110
7.5.2 模型的關系 111
7.5.3 實際模型 112
7.5.4 描述模型和所建模的域 112
7.6 問題分解與描述結構 113
7.6.1 檢查子問題 113
7.6.2 諸多的矛盾 114
7.6.3 身份關注點 114
7.6.4 病人監測 115
7.7 軟件開發的前景 115
7.7.1 無意義的規范 116
7.7.2 離散復雜性 116
7.8 致謝 117
參考文獻 117
第8章 建立動態系統的體系結構的模型 118
8.1 引言 118
8.1.1 動態系統 118
8.1.2 連續變化的情境 118
8.2 動態系統的模型 119
8.2.1 ARC的符號 119
8.2.2 模型的確認 122
8.3 適于重用的體系結構 123
8.3.1 生存 123
8.3.2 遞增的變化 124
8.3.3 松散耦合的組件 125
8.3.4 游戲很重要 126
8.4 結論 126
參考文獻 127
第9章 “方法是什么？”——關于域工程方面的一篇短文 130
9.1 引言 130
9.1.1 域、需求和軟件設計 130
9.1.2 要解決的問題 131
9.1.3 愿望 131
9.1.4 本文的結構 131
9.1.5 一些格式上的約定 132
9.2 方法和方法論 132
9.2.1 方法 132
9.2.2 方法論 132
9.2.3 方法構成 132
9.2.4 方法的原理 133
9.2.5 討論 134
9.3 域觀點和方面 134
9.3.1 涉眾與涉眾的觀點 135
9.3.2 域方面 138
9.3.3 討論 146
9.4 結論 147
9.4.1 討論 147
9.4.2 未來的工作 147
9.5 致謝 148
參考文獻 148
第二部分 程序設計技術
Section E 面向對象 151
第10章 面向對象程序設計和軟件開發——一種重要的評價方法 153
10.1 引言 153
10.2 面向對象——其要求與限制 154
10.3 面向對象程序設計——評論 155
10.3.1 類規范 155
10.3.2 對象實例化 156
10.3.3 軟件體系結構和組件概念 156
10.3.4 繼承和多態 157
10.3.5 順序性 157
10.4 短評面向對象分析與設計 158
10.4.1 系統模型和語義綜合 158
10.4.2 軟件和系統的體系結構 158
10.4.3 并發性 158
10.4.4 UML中的數據建模 158
10.5 結論 159
參考文獻 159
第11章 指針和對象的痕跡模型 161
11.1 引言：圖模型 161
11.2 痕跡模型 165
11.3 應用 169
11.4 結論 173
11.5 致謝 174
參考文獻 174
附錄 175
第12章 作為堆不變量的對象模型 177
引言 177
12.1 瞬象和對象模型 178
12.2 對象模型舉例 179
12.2.1 鏈表 179
12.2.2 記錄表 180
12.2.3 記錄數組 180
12.2.4 記錄的集合 180
12.2.5 映射 181
12.3 關系邏輯 181
12.4 圖邏輯 183
12.4.1 轉換字段和分類 183
12.4.2 限定的集合 183
12.4.3 解釋具體的對象模型 183
12.4.4 組合對象模型 184
12.4.5 抽象字段 184
12.4.6 索引字段 184
12.5 文本注釋 184
12.5.1 表示不變量 185
12.5.2 全局不變量 185
12.5.3 抽象字段的定義 186
12.6 討論 187
12.6.1 相關方法 187
12.6.2 相關語言 187
12.6.3 代碼與問題對象模型的比較 188
12.6.4 抽象字段與抽象對象的比較 188
12.6.5 字段作為關系 189
12.6.6 限定的集合 189
12.6.7 索引字段 190
12.6.8 外延相等 190
12.7 致謝 190
參考文獻 191
第13章 抽象依賴 193
13.1 引言 193
13.2 數據抽象的必要性 194
13.3 抽象變量的有效性 195
13.4 符號的定義 196
13.5 舉例：Readers 199
13.6 有關工作 204
13.7 結論 205
13.8 致謝 206
參考文獻 206
Section F 類型理論 209
第14章 類型系統 210
14.1 計算機科學中的類型系統 210
14.2 類型系統的用途 211
14.2.1 錯誤檢測 211
14.2.2 抽象 212
14.2.3 文檔 212
14.2.4 語言設計 212
14.2.5 語言安全 213
14.2.6 效率 214
14.2.7 更多的應用 214
14.3 歷史 215
參考文獻 216
第15章 類型的含義是什么？——從本質到外在語義 222
15.1 語法和類型化規則 223
15.2 本質語義 224
15.3 未類型化的語義 225
15.4 邏輯關系 226
15.5 分類 230
15.6 外在的PER語義 233
15.7 進一步的工作與未來方向 235
15.8 致謝 235
參考文獻 235
第三部分 應用與自動機理論
Section G 通過自動機將理論應用于實踐 237
第16章 利用推理、探索和抽象進行自動驗證 238
16.1 計算模型 239
16.2 程序行為邏輯 240
16.3 驗證技術 242
16.3.1 推理法 242
16.3.2 探索性方法 243
16.4 程序和屬性的抽象 244
16.4.1 數據抽象 244
16.4.2 謂詞抽象 245
16.5 驗證方法 248
16.6 結論 249
參考文獻 249
第17章 特征工程實驗 253
17.1 面向特征的規范 253
17.2 特征工程面臨的難題 254
17.3 面向特征的規范技術 255
17.4 一種樸素的特征工程方法 257
17.4.1 適用范圍 257
17.4.2 特征和特征合成語義 258
17.4.3 特征的語法 261
17.4.4 特征交互的語義 262
17.4.5 與呼叫有關的特征交互 262
17.4.6 與狀態信號有關的特征交互 263
17.4.7 與語音有關的交互 264
17.5 方法的應用 265
17.5.1 特征上下文 265
17.5.2 無約束目標特征集 266
17.5.3 特征集分析 268
17.6 評價 270
17.7 致謝 270
參考文獻 270
Section H 程序設計電路 272
第18章 高級電路設計 273
18.1 引言 273
18.2 電路圖 274
18.3 定時 275
18.4 觸發器 276
18.5 邊沿觸發 277
18.6 存儲器 279
18.7 合并 280
18.8 命令電路 282
18.9 函數電路 290
18.10 混合電路 293
18.11 性能 293
18.12 正確性 294
18.13 同步和異步電路 296
18.14 結論 297
18.15 致謝 297
參考文獻 298
Section I 安全與保密 299
第19章 能量分析：攻擊與防御策略 301
19.1 引言 301
19.1.1 背景知識 301
19.1.2 能量分析攻擊 301
19.1.3 貢獻 302
19.1.4 相關工作 302
19.1.5 本文的計劃 303
19.2 Twofish實現的能量分析 303
19.2.1 目標實現 303
19.2.2 能量攻擊裝置 304
19.2.3 Twofish變白過程攻擊 304
19.2.4 實驗結果 305
19.2.5 由變白密鑰到128位主密鑰 307
19.3 能量模型與攻擊 308
19.3.1 能量模型 308
19.3.2 統計能量攻擊 309
19.4 對能量分析的防御策略 310
19.4.1 ad-hoc方法 310
19.4.2 一種通用的防御策略 311
19.4.3 編碼 311
19.4.4 分析 312
19.4.5 概率論基礎 313
19.4.6 雙向分解的下限 313
19.4.7 編碼字節 317
19.5 結論 317
19.6 致謝 317
參考文獻 317
第20章 信息隱藏的概率方法 320
20.1 引言 320
20.2 背景知識：多級安全和信息流 320
20.3 經典信息論與程序精化 321
20.3.1 概率分布與隨機變量 321
20.3.2 條件分布 322
20.3.3 熵 322
20.3.4 條件熵 323
20.3.5 信息泄漏與信道容量 323
20.3.6 概率條件命令 323
20.4 命令程序中的信息流 325
20.4.1 信息流與程序精化 326
20.4.2 與其他工作的比較 329
20.5 舉例：安全文件存儲器 330
20.5.1 本質 330
20.5.2 添加文件名和數據 330
20.5.3 證明安全性與論證不安全性的對比 331
20.6 精化悖論 332
20.6.1 一些代數難題 332
20.6.2 量子模型 333
20.6.3 安全的本質 333
參考文獻 334

1. Java面向對象程序設計 [主編 姜春磊 陳虹潔]
2. C語言程序設計實驗指導與實訓（第二版） [主編 倪燃]
3. Python程序設計及實踐教程 [肖朝暉]
4. C語言程序設計 [魏琴 劉祖珉 趙仕波 肖陽春]
5. C語言程序設計實驗教程 [張小剛 司春景]
6. 電氣控制與PLC程序設計（第二版） [胡冠山]
7. Java Web項目化設計實踐教程 [邱云 曾陳萍]
8. C語言程序設計（第三版） [主編 丁紅 王立新 蔡開立]
9. Python數據分析 [主編　馮志輝　趙磊　李放]
10. Python程序設計與應用（第二版） [主編 張廣淵]
11. C程序設計實踐教程 [劉衛國]
12. C程序設計（慕課版） [劉衛國]
13. 程序設計基礎實踐教程（C/C++語言版） [張桂芬 葛麗娜]
14. C++案例項目精講 [主編 楊國興]
15. SwiftUI完全開發 [李智威 著]
16. MySQL數據庫項目式教程 [陳亞峰]
17. C語言程序設計習題與實驗指導（第二版） [主編 甄增榮 張賓]
18. C語言程序設計（第二版） [主編 甄增榮 田云霞]
19. Unity3D虛擬現實應用開發實踐 [主 編 劉龍]
20. Python程序設計 [主編 姜春磊 陳虹潔]
21. C語言程序設計實踐教程（活頁式） [主編 鄭茵 陳巍 滕泓虬]
22. 面向對象程序設計 [主編 張勇 張平華 趙小龍]
23. Python程序設計基礎及實戰 [主編　劉健]
24. C語言程序設計 [姜雪]
25. Python程序設計實踐教程 [王鶴琴 蔡正保]
26. C++程序設計實踐教程（第三版） [主編 劉衛國 曹岳輝]
27. C++程序設計（第三版） [主編 曹岳輝 劉衛國]
28. C語言程序設計項目化教程（活頁式） [主編 張利華 潘曉利]
29. 機器人流程自動化（RPA）實戰——基于UiPath [主編　金鑫]
30. Python 語言程序設計實踐指導 [主編　張雙獅]