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

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

程序設(shè)計能夠趕上硬件的巨大進展要歸功于程序設(shè)計、構(gòu)造以及組織原理的相應(yīng)的巨大進展。這些方法和原理的功效不言而喻——計算機技術(shù)遍及各方面——但更重要的是它們已經(jīng)開始反過來影響硬件的設(shè)計。對這樣的方法的研究稱為程序設(shè)計方法學(xué)，其研究課題包括系統(tǒng)模型、域模型、并發(fā)、面向?qū)ο�、程序�?guī)范與驗證等。

這些是本論文集的主題。

程序設(shè)計方法學(xué)

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

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

這些工具中的許多核心有深刻的理論背景——“斷言”和“程序不變量”依賴于程序設(shè)計邏輯理論；而規(guī)范和精化技術(shù)的程序語義是以它們?yōu)榛�礎(chǔ)的。本論文集中的短文集中論述構(gòu)造先進應(yīng)用程序的新方法和正在涌現(xiàn)的方法；它們要解決軟件開發(fā)人員面臨的問題，提出實際解決方案和它們的理論基礎(chǔ)。

匯編有關(guān)本主題論文成一本書的思想是在國際信息聯(lián)合會2.3工作小組（IFIP）的技術(shù)研討會上出現(xiàn)的。

工作小組2.3

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

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

關(guān)于本論文集

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

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

本書結(jié)構(gòu)

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

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

致謝

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

Annabelle McIver

Carroll Morgan

澳大利亞，悉尼，2002

撰稿者名單
譯者序
前言
第一部分 模型與正確性
Section A 并行與交互 1
第1章 需要：并行性的組構(gòu)方法 3
1.1 組構(gòu)性 3
1.2 并發(fā)性的本質(zhì)是干擾 4
1.3 推理干擾 5
1.4 關(guān)于假設(shè)/承諾推理的一些問題 7
1.5 寄生變量的作用 7
1.6 粒度所關(guān)心的事情 7
1.7 抽象的原子性及其精化 8
1.8 結(jié)論 8
1.9 致謝 8
參考文獻 9
第2章 用契約強制行為 11
2.1 引言 11
2.2 契約 12
2.2.1 狀態(tài)與狀態(tài)變化 12
2.2.2 契約 13
2.2.3 操作語義 14
2.2.4 契約舉例 15
2.2.5 行動系統(tǒng) 16
2.2.6 行動系統(tǒng)舉例 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 構(gòu)造解釋程序 24
2.4.3 其他暫態(tài)屬性 25
2.5 分析行動系統(tǒng)的行為 27
2.5.1 行動系統(tǒng)的分類 27
2.5.2 分析行為 28
2.6 驗證強制 30
2.6.1 謂詞級正確性條件 30
2.6.2 基于不變量的方法 31
2.6.3 示范方法 32
2.6.4 例子系統(tǒng)中的強制性 33
2.7 結(jié)論及相關(guān)工作 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 結(jié)論 48
3.9 致謝 48
參考文獻 48
第4章 并發(fā)面向?qū)ο蟪绦蚝喕�定�?50
4.1 引言 50
4.2 Seuss程序設(shè)計符號 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 把過程看作關(guān)系 59
4.4.3 方框條件 60
4.5 兼容性 61
4.5.1 兼容性舉例 61
4.5.2 兼容過程的半交換性 62
4.6 簡化定理的證明 64
4.6.1 松執(zhí)行 64
4.6.2 簡化方案 65
4.7 結(jié)束語 66
4.8 致謝 67
參考文獻 67
Section C 系統(tǒng)與實時性 68
第5章 抽象時間 70
5.1 引言 70
5.2 流 70
5.2.1 數(shù)學(xué)基礎(chǔ)：流 71
5.2.2 建時間模型 71
5.3 把組件看作流函數(shù) 73
5.4 時間抽象 74
5.4.1 抽象的一般概念 74
5.4.2 抽象時間 75
5.5 結(jié)論 76
5.5.1 文獻中的時間模型 76
5.5.2 結(jié)語 77
5.6 致謝 77
參考文獻 78
第6章 實時精化的謂詞語義 80
6.1 背景知識 80
6.2 語言和語義 81
6.2.1 實時規(guī)范命令 83
6.2.2 簡單實時命令 86
6.2.3 順序組合 86
6.2.4 不確定選擇、條件和挑選 88
6.2.5 局部和輔助變量 90
6.3 一個例子 91
6.4 循環(huán) 93
6.5 定時約束分析 96
6.6 結(jié)論 97
6.7 致謝 98
參考文獻 98
Section D 規(guī)定復(fù)雜的行為 100
第7章 系統(tǒng)描述的方面 102
7.1 引言 102
7.2 符號處理 102
7.3 機器和領(lǐng)域 104
7.3.1 規(guī)范接口 104
7.3.2 需求接口 104
7.3.3 系統(tǒng)描述 104
7.3.4 有目的的描述 105
7.3.5 為什么需要單獨的描述 106
7.4 描述實際領(lǐng)域 107
7.4.1 標記 107
7.4.2 使用定義 108
7.4.3 區(qū)分定義和描述 109
7.5 描述與模型 109
7.5.1 電梯模型 110
7.5.2 模型的關(guān)系 111
7.5.3 實際模型 112
7.5.4 描述模型和所建模的域 112
7.6 問題分解與描述結(jié)構(gòu) 113
7.6.1 檢查子問題 113
7.6.2 諸多的矛盾 114
7.6.3 身份關(guān)注點 114
7.6.4 病人監(jiān)測 115
7.7 軟件開發(fā)的前景 115
7.7.1 無意義的規(guī)范 116
7.7.2 離散復(fù)雜性 116
7.8 致謝 117
參考文獻 117
第8章 建立動態(tài)系統(tǒng)的體系結(jié)構(gòu)的模型 118
8.1 引言 118
8.1.1 動態(tài)系統(tǒng) 118
8.1.2 連續(xù)變化的情境 118
8.2 動態(tài)系統(tǒng)的模型 119
8.2.1 ARC的符號 119
8.2.2 模型的確認 122
8.3 適于重用的體系結(jié)構(gòu) 123
8.3.1 生存 123
8.3.2 遞增的變化 124
8.3.3 松散耦合的組件 125
8.3.4 游戲很重要 126
8.4 結(jié)論 126
參考文獻 127
第9章 “方法是什么？”——關(guān)于域工程方面的一篇短文 130
9.1 引言 130
9.1.1 域、需求和軟件設(shè)計 130
9.1.2 要解決的問題 131
9.1.3 愿望 131
9.1.4 本文的結(jié)構(gòu) 131
9.1.5 一些格式上的約定 132
9.2 方法和方法論 132
9.2.1 方法 132
9.2.2 方法論 132
9.2.3 方法構(gòu)成 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 結(jié)論 147
9.4.1 討論 147
9.4.2 未來的工作 147
9.5 致謝 148
參考文獻 148
第二部分 程序設(shè)計技術(shù)
Section E 面向?qū)ο?151
第10章 面向?qū)ο蟪绦蛟O(shè)計和軟件開發(fā)——一種重要的評價方法 153
10.1 引言 153
10.2 面向?qū)ο蟆�—其要求與限制 154
10.3 面向?qū)ο蟪绦蛟O(shè)計——評論 155
10.3.1 類規(guī)范 155
10.3.2 對象實例化 156
10.3.3 軟件體系結(jié)構(gòu)和組件概念 156
10.3.4 繼承和多態(tài) 157
10.3.5 順序性 157
10.4 短評面向?qū)ο蠓治雠c設(shè)計 158
10.4.1 系統(tǒng)模型和語義綜合 158
10.4.2 軟件和系統(tǒng)的體系結(jié)構(gòu) 158
10.4.3 并發(fā)性 158
10.4.4 UML中的數(shù)據(jù)建模 158
10.5 結(jié)論 159
參考文獻 159
第11章 指針和對象的痕跡模型 161
11.1 引言：圖模型 161
11.2 痕跡模型 165
11.3 應(yīng)用 169
11.4 結(jié)論 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 記錄數(shù)組 180
12.2.4 記錄的集合 180
12.2.5 映射 181
12.3 關(guān)系邏輯 181
12.4 圖邏輯 183
12.4.1 轉(zhuǎn)換字段和分類 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 相關(guān)方法 187
12.6.2 相關(guān)語言 187
12.6.3 代碼與問題對象模型的比較 188
12.6.4 抽象字段與抽象對象的比較 188
12.6.5 字段作為關(guān)系 189
12.6.6 限定的集合 189
12.6.7 索引字段 190
12.6.8 外延相等 190
12.7 致謝 190
參考文獻 191
第13章 抽象依賴 193
13.1 引言 193
13.2 數(shù)據(jù)抽象的必要性 194
13.3 抽象變量的有效性 195
13.4 符號的定義 196
13.5 舉例：Readers 199
13.6 有關(guān)工作 204
13.7 結(jié)論 205
13.8 致謝 206
參考文獻 206
Section F 類型理論 209
第14章 類型系統(tǒng) 210
14.1 計算機科學(xué)中的類型系統(tǒng) 210
14.2 類型系統(tǒng)的用途 211
14.2.1 錯誤檢測 211
14.2.2 抽象 212
14.2.3 文檔 212
14.2.4 語言設(shè)計 212
14.2.5 語言安全 213
14.2.6 效率 214
14.2.7 更多的應(yīng)用 214
14.3 歷史 215
參考文獻 216
第15章 類型的含義是什么？——從本質(zhì)到外在語義 222
15.1 語法和類型化規(guī)則 223
15.2 本質(zhì)語義 224
15.3 未類型化的語義 225
15.4 邏輯關(guān)系 226
15.5 分類 230
15.6 外在的PER語義 233
15.7 進一步的工作與未來方向 235
15.8 致謝 235
參考文獻 235
第三部分 應(yīng)用與自動機理論
Section G 通過自動機將理論應(yīng)用于實踐 237
第16章 利用推理、探索和抽象進行自動驗證 238
16.1 計算模型 239
16.2 程序行為邏輯 240
16.3 驗證技術(shù) 242
16.3.1 推理法 242
16.3.2 探索性方法 243
16.4 程序和屬性的抽象 244
16.4.1 數(shù)據(jù)抽象 244
16.4.2 謂詞抽象 245
16.5 驗證方法 248
16.6 結(jié)論 249
參考文獻 249
第17章 特征工程實驗 253
17.1 面向特征的規(guī)范 253
17.2 特征工程面臨的難題 254
17.3 面向特征的規(guī)范技術(shù) 255
17.4 一種樸素的特征工程方法 257
17.4.1 適用范圍 257
17.4.2 特征和特征合成語義 258
17.4.3 特征的語法 261
17.4.4 特征交互的語義 262
17.4.5 與呼叫有關(guān)的特征交互 262
17.4.6 與狀態(tài)信號有關(guān)的特征交互 263
17.4.7 與語音有關(guān)的交互 264
17.5 方法的應(yīng)用 265
17.5.1 特征上下文 265
17.5.2 無約束目標特征集 266
17.5.3 特征集分析 268
17.6 評價 270
17.7 致謝 270
參考文獻 270
Section H 程序設(shè)計電路 272
第18章 高級電路設(shè)計 273
18.1 引言 273
18.2 電路圖 274
18.3 定時 275
18.4 觸發(fā)器 276
18.5 邊沿觸發(fā) 277
18.6 存儲器 279
18.7 合并 280
18.8 命令電路 282
18.9 函數(shù)電路 290
18.10 混合電路 293
18.11 性能 293
18.12 正確性 294
18.13 同步和異步電路 296
18.14 結(jié)論 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 相關(guān)工作 302
19.1.5 本文的計劃 303
19.2 Twofish實現(xiàn)的能量分析 303
19.2.1 目標實現(xiàn) 303
19.2.2 能量攻擊裝置 304
19.2.3 Twofish變白過程攻擊 304
19.2.4 實驗結(jié)果 305
19.2.5 由變白密鑰到128位主密鑰 307
19.3 能量模型與攻擊 308
19.3.1 能量模型 308
19.3.2 統(tǒng)計能量攻擊 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 概率論基礎(chǔ) 313
19.4.6 雙向分解的下限 313
19.4.7 編碼字節(jié) 317
19.5 結(jié)論 317
19.6 致謝 317
參考文獻 317
第20章 信息隱藏的概率方法 320
20.1 引言 320
20.2 背景知識：多級安全和信息流 320
20.3 經(jīng)典信息論與程序精化 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 本質(zhì) 330
20.5.2 添加文件名和數(shù)據(jù) 330
20.5.3 證明安全性與論證不安全性的對比 331
20.6 精化悖論 332
20.6.1 一些代數(shù)難題 332
20.6.2 量子模型 333
20.6.3 安全的本質(zhì) 333
參考文獻 334

1. C程序設(shè)計實踐教程 [劉衛(wèi)國]
2. C程序設(shè)計（慕課版） [劉衛(wèi)國]
3. 程序設(shè)計基礎(chǔ)實踐教程（C/C++語言版） [張桂芬 葛麗娜]
4. C++案例項目精講 [主編 楊國興]
5. SwiftUI完全開發(fā) [李智威 著]
6. MySQL數(shù)據(jù)庫項目式教程 [陳亞峰]
7. C語言程序設(shè)計習(xí)題與實驗指導(dǎo)（第二版） [主編 甄增榮 張賓]
8. C語言程序設(shè)計（第二版） [主編 甄增榮 田云霞]
9. Unity3D虛擬現(xiàn)實應(yīng)用開發(fā)實踐 [主 編 劉龍]
10. Python程序設(shè)計 [主編 姜春磊 陳虹潔]
11. C語言程序設(shè)計實踐教程（活頁式） [主編 鄭茵 陳巍 滕泓虬]
12. 面向?qū)ο蟪绦蛟O(shè)計 [主編 張勇 張平華 趙小龍]
13. Python程序設(shè)計基礎(chǔ)及實戰(zhàn) [主編　劉健]
14. C語言程序設(shè)計 [姜雪]
15. Python程序設(shè)計實踐教程 [王鶴琴 蔡正保]
16. C++程序設(shè)計實踐教程（第三版） [主編 劉衛(wèi)國 曹岳輝]
17. C++程序設(shè)計（第三版） [主編 曹岳輝 劉衛(wèi)國]
18. C語言程序設(shè)計項目化教程（活頁式） [主編 張利華 潘曉利]
19. 機器人流程自動化（RPA）實戰(zhàn)——基于UiPath [主編　金鑫]
20. Python 語言程序設(shè)計實踐指導(dǎo) [主編　張雙獅]
21. Python程序設(shè)計案例教程 [主編 毛錦庚 鐘肖英 周賢來 ]
22. 基于.NET Core框架的分布式系統(tǒng)架構(gòu)設(shè)計 [湯佳 著]
23. Python語言程序設(shè)計教程 [郭其標 房宜汕]
24. Python程序設(shè)計 [李國燕 王新強 劉佳 等編著]
25. Python程序設(shè)計項目化教程（活頁式） [主編　盧鳳偉]
26. Java編程基礎(chǔ)案例式教程 [主編 陳艷華 唐春蘭]
27. Python語言同步案例習(xí)題精解 [主編 肖朝暉]
28. Unity應(yīng)用開發(fā)與實戰(zhàn)（微課版） [主 編 程永恒]
29. PHP程序設(shè)計項目化教程 [主 編 杜海穎]
30. 簡單易懂的Python入門教程 [［日］大澤文孝　著]