圖書簡介
本書是世界著名的計算機科學家DinesBjorner教授對其所從事的軟體工程研究的總結。
這幾卷書主要講述了如何使用形式方法指導軟體工程的開發，特別是作者獨創性地提出了領域工程這一全新的研究領域並在第~3~卷中予以系統的論述。作者結合~RAISE（工業軟體開發的嚴格方法）規約語言，詳細闡釋了在軟體的領域分析、需求分析、軟體設計和開發的各個階段，如何採用形式方法來指導軟體開發模式，來保證軟體開發的可靠性和正確性。
目錄
原著作者為中文版所作的序
譯者序
序言ix
概述ix
“UML”化的形式技術x
RAISE 規約語言： RSLx
致謝x
第 2 卷的簡要指南xi
part I 開篇1
xpart開篇1
chapter 1序言3
1.1前言3
1.1.1為什麼有本卷3
1.1.2為什麼要掌握這些原理、技術與工具3
1.1.3本卷“包含”了什麼4
1.1.4本卷是如何“陳述”的5
1.2“輕量級”形式技術5
1.3 RSL 的入門讀物7
1.3.1類型7
類型表達式7
類型定義8
具體類型8
子類型9
分類 ------ 抽象類型9
1.3.2 RSL 謂詞演算10
命題表達式10
簡單謂詞表達式10
量化表達式10
1.3.3具體 RSL 類型11
集合枚舉11
笛卡爾枚舉11
列表枚舉12
映射枚舉12
集合操作13
笛卡爾操作15
列表操作15
映射操作17
1.3.4 演算 + 函式19
演算句法19
自由與約束變數19
代入19
$\alpha $ 換名與 $\beta $ 規約20
函式基調20
函式定義20
1.3.5其他套用表達式21
let 表達式21
條件表達式22
操作符/運算元表達式23
1.3.6命令式結構24
變數與賦值24
語句序列與 \bf skip24
命令式條件語句24
循環條件語句24
疊代序列25
1.3.7進程結構25
進程通道25
進程複合25
輸入/輸出事件26
進程定義26
1.3.8簡單 RSL 規約26
1.4文獻評註27
part II 規約刻面29
xpart規約刻面29
chapter 2層次與複合31
2.1關鍵問題31
2.1.1非形式說明31
2.1.2形式說明32
2.2初步的方法論的結論33
2.2.1一些定義33
層次抽象33
“自頂向下”33
“自底向上”33
2.2.2原則與技術33
2.3主要的例子34
2.3.1層次的敘述表示34
2.3.2層次的形式表示36
2.3.3複合的，敘述性表示39
2.3.4複合的形式表示41
2.4討論43
2.5文獻評註：Stanis\l aw Leshniewski43
2.6練習43
chapter 3指稱和計算47
3.1前言47
3.1.1計算和指稱47
3.1.2句法和語義48
3.1.3特性描述48
3.2指稱語義48
3.2.1一個簡單的例子：數符48
3.2.2指稱原則49
3.2.3表達式指稱50
一個擴展52
3.2.4GOTO 連續53
問題54
句法類型56
語義類型57
主要的語義函式58
程式58
塊58
一個深奧的問題59
例 3.3\hbox 的其他評論60
其餘的語義函式60
賦值60
語句列表60
條件 GOTO61
while 循環61
討論61
3.2.5指稱語義的討論61
3.3計算語義63
3.3.1關鍵問題63
3.3.2兩個例子63
3.3.3表達式計算63
計算狀態64
引出控制棧的動機64
細化函式65
討論66
3.3.4GOTO 程式的計算語義66
句法66
一些語義觀測結果67
觀測 167
觀測 267
語義類型68
解釋器函式68
3.3.5協同例程程式的計算語義71
“協同例程”程式文本 I71
協同例程程式文本 II72
3.3.6討論72
有關連續的機械化73
有關通過標號變數的 GOTO 的“威力”73
有關計算語義73
3.4回顧：指稱和計算73
3.5一些語義的創始人74
3.5.1John McCarthy74
3.5.2Peter Landin75
3.6練習76
chapter 4格局：上下文和狀態79
4.1引言80
4.2問題82
4.3“現實世界”上下文和狀態83
4.3.1物理系統：上下文和狀態83
4.3.2上下文和狀態84
4.3.3非物理系統：上下文和狀態84
上下文84
狀態85
模型85
4.3.4討論，I85
4.3.5討論，II86
4.4第一次總結：上下文和狀態86
4.4.1概述86
模型和規約狀態86
4.4.2開發原則和技術87
4.5程式設計語言格局87
4.6並發進程格局87
4.6.1示例87
一句提示88
4.2(a) 語義的注釋89
4.2(b) 語義的注釋89
4.2(c) 語義的注釋89
4.2(d) 語義的注釋89
4.6.2總結92
4.7第二次總結：上下文和狀態93
4.8信息狀態和行為狀態93
4.8.1作為狀態機數據的程式流程圖94
4.8.2流程圖 $\equiv $ 機器94
4.8.3流程圖機94
4.8.4評論95
4.8.5結論95
4.9最後的總結：上下文和狀態96
4.10練習97
part\ III\hskip 關鍵領域和系統刻面99
xpart關鍵領域和系統刻面99
chapter 5時間、空間和空間/時間101
5.1時間101
5.1.1時間 ------ 基礎102
時間變化實體 = 動態實體102
時間和動態性104
5.1.2時間 ------ 一般問題104
5.1.3時間的 \CJKfamily kai“A 序列”和 \CJKfamily kai“B 序列”模型104
5.1.4時間的連續統理論105
5.1.5時態事件106
5.1.6時態行為106
5.1.7時間表示106
5.1.8時間“上”的操作108
5.2空間108
5.2.1空間 ------ 基礎108
5.2.2位置變化實體109
5.2.3位置和動態性110
5.2.4空間 ------ 一般問題111
點、曲線、曲面、體積111
空間“事件”111
空間“行為”112
空間體的表示112
空間上的操作112
5.3空間/時間113
5.3.1指導示例113
5.3.2空間/時間的表示114
5.3.3Blizard 的時間空間理論114
\CJKfamily kaiBlizard 空間/時間模型討論115
5.4討論115
5.5文獻評註115
5.6練習115
part\ IV\hskip 語言學119
xpart語言學119
chapter 6語用121
6.1前言121
6.2日常語用122
6.3“形式”語用122
6.4討論123
6.4.1概述123
6.4.2原則和技術123
6.5文獻評註123
6.6練習124
chapter 7語義126
7.1前言126
7.2具體語義127
7.3“抽象”語義127
7.4預備語義概念127
7.4.1句法和語義類型127
7.4.2上下文128
7.4.3狀態128
7.4.4格局128
7.4.5解釋、求值、細化128
7.5指稱語義129
7.5.1簡單情況130
7.5.2複合情況130
7.6宏擴展語義130
7.6.1重寫131
7.6.2宏擴展131
7.6.3歸納重寫132
靜態歸納語義132
動態歸納語義133
7.6.4不動點求值134
7.7操作和計算語義135
7.7.1棧語義135
7.7.2屬性語法語義135
符號屬性語法解析樹示例138
7.8證明規則語義139
7.9討論141
7.9.1概述141
7.9.2原則、技術和工具141
7.10文獻評註142
7.11練習142
chapter 8句法145
8.1問題145
8.1.1形式和內容：句法和語義145
8.1.2本章的結構和內容146
8.2句子和語義結構146
8.2.1概述147
句子結構的句法147
語義結構的句法147
8.2.2句子結構示例147
簡單句子結構的建模148
8.2.3語義結構示例149
8.3第一個抽象句法，John McCarthy152
8.3.1分析語法：觀測器和選擇器152
8.3.2合成語法：生成器153
8.4 BNF 語法 $\approx $ 具體句法153
8.4.1 BNF 語法154
8.4.2 BNF$\leftrightarrow $ RSL 語法解析樹關係154
8.5結構生成器和識別器156
8.5.1上下文無關語法和語言156
8.5.2語法解析樹157
8.5.3正則表達式和語言159
8.5.4語言識別器160
8.6XML：可擴展標記語言（Extensible Markup Language）160
8.6.1例160
8.6.2討論162
8.6.3歷史背景162
8.6.4目前的 XML“狂熱”162
8.6.5 XML 表達式162
8.6.6 XML 模式164
8.6.7參考166
8.7抽象句法166
8.7.1存儲模型的抽象句法166
值和值的類型167
位置和位置類型167
存儲168
類型約束168
8.7.2其他存儲模型的抽象句法169
非形式闡述169
形式說明170
8.8轉換 RSL 類型到 BNF170
8.8.1問題170
8.8.2可能的解決辦法171
8.9非形式和形式句法討論172
8.9.1概述172
8.9.2原則、技術和工具172
8.10文獻評註173
8.11練習173
chapter 9符號體系180
9.1符號體系 = 句法 $\oplus $ 語義 $\oplus $ 語用180
9.2符號體系181
9.3語言構件181
9.4語言學182
9.5語言和系統183
9.5.1職業語言183
9.5.2元語言184
9.5.3系統184
物理系統角度184
物理和非物理系統的例子185
語言系統角度186
示例系統語言187
流程圖語言191
簡單流程圖的非形式句法191
簡單流程圖192
簡單流程圖的形式句法192
結構化流程圖193
系統圖和形式規約194
9.5.4系統圖語言195
9.5.5系統概念討論196
9.5.6作為語言的系統196
9.6討論197
9.6.1概述197
9.6.2原則、技術和工具197
9.7Charles Sanders Peirce197
9.8文獻評註197
9.9練習198
part\ V\hskip 其他規約技術203
xpart其他規約技術203
chapter 10模組化205
10.1前言206
10.1.1一些示例206
示例回顧210
模組描述：對象和模式210
實現210
逐步開發211
關注分離211
10.1.2預備性討論211
軟體設備211
抽象數據類型 $\DOTSB \mapstochar \rightarrow $ 代數語義211
框架方法212
實體關係圖（Entity-Relationship，ER）212
模組化的一般語用213
模組化的一般語義213
模組化的一般句法213
一般的模組規約方法213
10.1.3章節結構213
10.2 RSL 類、對象和模式213
10.2.1介紹 RSL “類”概念214
RSL 聲明的意義 ------回顧214
RSL\ “類”概念的第一個動機：關注焦點214
RSL\ “類”概念的第二個動機：語義代數214
RSL\ “類”概念的第三個動機215
RSL\ “類”概念的第四個動機：命名模式216
10.2.2 RSL\ “類”概念217
10.2.3 RSL “對象”概念218
10.2.4 RSL\ “模式”概念218
簡單模式218
模式擴展219
隱藏220
其他223
10.2.5 RSL\ “模式”參數化223
動機：模式為什麼和如何參數化？223
參數化模式的句法和語義225
10.2.6“大型”示例226
對比背景示例226
敘述226
形式化226
模式化示例228
10.2.7定義：類、模式和對象230
10.3UML 和 RSL231
10.3.1 UML 圖概述231
用例圖231
序列/合作圖232
狀態圖232
10.3.2類圖232
UML “標準化”232
10.3.3類圖232
類232
關聯233
連線234
泛化235
10.3.4例：鐵路網235
10.3.5比較 UML 和 RSL OO 結構236
10.3.6引用237
10.3.7類圖的限制237
10.4討論238
10.4.1模組性問題238
模組規約和程式設計238
模組性概念的穩定性238
面向對象（ Object-Oriented，OO）“程式設計”何去何從238
模式、對象和模組演算238
UML 類圖概念的形式化239
10.4.2原則、技術和工具239
10.5文獻評註239
10.6練習239
chapter 11自動機和機器241
11.1離散狀態自動機241
11.1.1直觀理解243
11.1.2動機243
11.1.3語用243
11.2離散狀態機器245
11.3有限狀態自動機246
11.3.1正則表達式語言識別器246
11.3.2正則表達式247
11.3.3形式語言和自動機248
11.3.4自動機完全化248
11.3.5非確定性自動機248
11.3.6最小狀態有限自動機249
11.3.7有限狀態自動機形式化， I250
11.3.8有限狀態自動機實現，I250
11.3.9有限狀態自動機形式化，II251
11.3.10有限狀態自動機實現，II252
11.3.11有限狀態自動機 ------ 總結252
11.4有限狀態機器253
11.4.1有限狀態機器控制器253
11.4.2有限狀態機器語法分析器255
11.4.3有限狀態機器形式化256
11.4.4有限狀態機器實現257
11.4.5有限狀態機器 ------ 總結258
11.5下推棧設備259
11.5.1下推棧自動機和機器259
11.5.2下推棧機器形式化260
11.5.3下推棧設備總結262
11.6文獻評註：自動機和機器262
11.7練習262
part\ VI\hskip 並發和時態265
xpart並發和時態265
chapter 12佩特里網267
12.1問題267
12.2條件事件網（Condition Event Net，CEN）268
12.2.1描述268
12.2.2CEN 小示例268
12.2.3條件事件網的 RSL 模型271
CEN 句法和靜態語義271
動態語義273
12.3位置變遷網（Place Transition Net，PTN）273
12.3.1描述274
12.3.2PTN 小例子274
12.3.3位置變遷網的 RSL 模型275
PTN 句法和靜態語義275
動態語義276
12.3.4鐵路領域佩特里網示例278
進路（route）描述278
聯鎖表278
單元的佩特里網279
轉轍器的佩特里網280
信號的佩特里網280
進路的佩特里網280
聯鎖表佩特里網的構造281
進路和單元281
進路和轉轍器281
進路和信號281
總結281
12.4染色佩特里網（Coloured Petri Net，CPN）282
12.4.1描述282
12.4.2CPN 示例283
12.4.3染色佩特里網 RSL 模型285
CPN 句法和靜態語義285
染色佩特里網的動態語義287
輔助語義函式287
染色佩特里網的變遷函式288
12.4.4時間化染色佩特里網289
12.5CEN 示例：工作流系統290
12.5.1項目計畫290
項目計畫290
項目計畫構造292
12.5.2項目活動293
項目控制流：“波”和跡293
項目計畫“執行”295
12.5.3項目生成300
進程生成300
通道分配301
12.6CPN 和 RSL 示例：超標量處理器302
12.6.1描述302
12.6.2染色佩特里網303
12.6.3 RSL\ 模型：超標量處理器308
12.7討論316
12.8文獻評註317
12.9練習317
chapter 13訊息和活序列圖319
paragraph\textup 讀者指南319
13.1訊息序列圖319
13.1.1問題319
13.1.2基本 MSC（Basic MSC，\textrm BMSC）320
非形式闡述320
BMSC 示例323
\textrm BMSC 句法的 RSL 模型324
13.1.3高級 MSC（High-Level MSC，\textrm HMSC）326
非形式闡述326
HMSC 示例326
13.1.4\textrm HMSC 句法的 RSL 模型326
13.1.5MSC 是 HMSC327
13.1.6MSC 的句法良構性328
13.1.7示例：\textrm IEEE 802.11 無線網路333
描述333
IEEE 802.11 示例的 RSL 模型336
13.1.8基本訊息序列圖的語義342
13.1.9高級訊息序列圖的語義343
13.2活序列圖：非形式闡述344
13.2.1活序列圖句法344
活序列圖的圖形句法344
全稱和存在圖344
前圖（Prechart）344
“熱”和“冷”訊息345
同步和異步訊息345
條件345
子圖346
位置347
13.2.2活序列圖示例，I348
13.3進程代數350
13.3.1進程代數 \ensuremath \mathit PA_\epsilon 350
基調350
等式351
可導出性352
歸約到基本項353
13.3.2 \ensuremath \mathit PA_\epsilon 語義356
13.3.3進程代數 $PAc\@uscore .\epsilon $359
13.3.4 \ensuremath \mathit PAc_\epsilon 的語義361
13.4活序列圖的代數語義364
13.4.1活序列圖的文本句法364
13.4.2活序列圖語義364
13.4.3活序列圖實例，II368
13.5關聯訊息圖到 RSL368
13.5.1集成的類型368
13.5.2 RSL 子集369
句法369
有通信行為的操作語義369
13.5.3關聯活序列圖到 RSL371
句法限制371
滿足關係372
13.5.4檢查滿足性377
13.5.5工具支持378
13.6通信事務進程（Communicating Transaction Processes，CTP）379
13.6.1直觀理解379
13.6.2\textup 闡述 CTP380
\textup CTP 圖380
\textup CTP 進程380
\textup CTP 事務模式381
\textup CTP 事務圖382
\textup 簡單 CTP 訊息序列圖382
\textup 使能的 CTP 事務圖383
\textup 使能的和被調用的模式和圖383
詳述調用和執行383
\textup CTP 變遷384
13.6.3哲學家就餐示例385
13.6.4\textup CTP 形式化388
\textup 句法和一些語義類型388
\textup 輔助句法和語義函式基調389
\textup 輔助函式基調和定義390
\textup CTP 的良構性390
\textup 圖的良構性392
\textup 動態語義，類型394
paragraph\textup 語義類型394
paragraph\textup 良構性395
\textup 動態語義，函式396
paragraph\textup 輔助函式396
paragraph\textup 初始化398
paragraph\textup 使能398
paragraph\textup 激活399
13.7討論401
13.7.1概述401
13.7.2原則、技術和工具402
13.8文獻評註402
13.9練習403
chapter 14狀態圖406
14.1前言406
14.2狀態圖的描述407
14.3狀態圖句法的 RSL 模型411
14.4例413
14.4.1鐵路線路自動閉塞414
敘述414
一般線路段414
第一線路段416
狀態圖416
一般模型416
特殊情況416
14.4.2鐵路線路方向協定系統418
敘述418
LDAS 內部行為（狀態圖）420
車站 A 的內部狀態（狀態圖）421
車站 B 的內部行為（狀態圖）421
外部行為（活序列圖）421
14.4.3無線雨量計422
描述422
狀態圖模型423
RSL\ 模型424
14.5狀態圖的進程代數427
14.5.1SPL（Statechart Process Language）: 狀態圖進程語言428
14.5.2SPL 語義428
14.5.3SPL 項等價429
14.6狀態圖語義430
14.6.1狀態圖的 SPL 語義430
14.6.2狀態圖示例433
14.7關聯狀態圖到 RSL433
14.7.1句法限制433
14.7.2滿足關係435
14.7.3滿足檢查435
14.7.4工具支持436
14.8討論436
14.8.1概述436
14.8.2原則、技術和工具436
14.9文獻評註437
14.10練習437
paragraph\textup 數字鐘狀態：441
paragraph\textup 時間/日期更新狀態：441
paragraph\textup 鬧鈴更新狀態：441
paragraph\textup 跑表狀態：441
paragraph\textup 數字鐘的高級描述：442
chapter 15時間的定量模型443
15.1問題443
15.1.1軟時態443
15.1.2硬時態444
15.1.3軟實時和硬實時444
15.1.4例子 ------“老方法”！444
15.1.5本章的結構445
15.2時態邏輯446
15.2.1問題446
15.2.2哲學語言學背景446
15.2.3區間時態邏輯 451
15.2.4經典時態操作符 452
15.3時段演算452
15.3.1例子，第 I 部分453
15.3.2一些基礎概念453
布爾狀態、狀態斷言和特性函式453
狀態時段454
什麼是煤氣灶？454
煤氣泄漏455
煤氣灶需求456
15.3.3例子，第 II 部分456
問題描述456
構件456
屬性457
事件457
行為457
不變式458
需求： L\_Req458
基礎模型458
形式需求458
15.3.4句法459
簡單表達式459
狀態表達式和斷言460
時段和時段項460
時段公式460
通常的時段公式簡寫460
15.3.5非形式語義461
15.3.6例子，第 III 部分462
電梯例子：設計462
軟體設計， L\_Design462
領域描述：假設， L\_Domain463
簡單設計相對於領域和需求的正確性464
公路鐵路水平交叉口例子464
問題描述465
形式化465
\CJKfamily kai[1] 狀態變數465
\CJKfamily kai[2] 需求466
\CJKfamily kai[2.1] 安全需求467
\CJKfamily kai[2.2] 功能需求467
問題描述468
火車接近470
火車通過470
一些觀察470
評論470
關於驗證和模型檢測的問題471
15.3.7變遷和事件471
15.3.8討論：從領域到設計475
15.4 TRSL: 具有時間的 RSL475
15.4.1 TRSL 的設計標準476
第一個 TRSL 設計決策476
第二個 TRSL 設計決策476
15.4.2 TRSL 語言478
句法478
語義478
15.4.3另一個煤氣灶的例子479
15.4.4討論482
15.5具有時間和時段的 RSL482
15.5.1 TRSL 的回顧482
15.5.2 TRSL 和時段演算483
問題描述484
時段演算需求484
TRSL 規約484
滿足關係485
15.6討論485
15.6.1一般問題485
15.6.2原則、技術和工具486
15.7文獻評註486
15.8練習487
part\ VII\hskip 解釋器和編譯器定義489
xpart解釋器和編譯器定義489
chapter 16SAL：簡單套用式語言491
16.1提示491
16.2\textrm SAL 句法492
16.2.1\textrm SAL 句法的非形式說明492
16.2.2\textrm SAL 句法的形式說明492
16.2.3評論493
16.3指稱語義493
16.3.1非形式語義493
16.3.2形式語義494
語義類型494
操作符意義494
語義函式495
16.3.3\textrm SAL 語義的回顧，1495
16.3.4兩句題外話496
後面的內容!496
最近的錯誤496
16.4一階套用式語義498
16.4.1句法類型498
16.4.2語義類型498
16.4.3抽象函式499
16.4.4輔助函式500
16.4.5語義函式500
16.4.6回顧503
16.4.7\textrm SAL 語義的回顧，2503
16.5抽象命令式棧語義504
16.5.1設計決策 ------ 非形式動機說明504
16.5.2語義風格評論504
16.5.3句法類型505
16.5.4語義類型505
16.5.5抽象函式505
16.5.6運行時函式505
16.5.7語義函式507
兩個不變式507
[0] 解釋程式507
前一步驟：507
當前步驟：507
[1] 解釋常量表達式508
前一步驟：508
當前步驟：508
[2] 解釋變數表達式508
前一步驟：508
當前步驟：508
[3] 解釋前綴表達式509
前一步驟：509
當前步驟：509
[4] 解釋中綴表達式509
前一步驟：509
當前步驟：509
[5] 解釋條件表達式510
前一步驟：510
當前步驟：510
[6] 解釋 lambda 表達式510
前一步驟：510
當前步驟：510
[7] 解釋簡單 let 表達式510
前一步驟：510
當前步驟：511
[8] 解釋遞歸 let 表達式511
前一步驟：511
當前步驟：511
[9] 解釋函式套用表達式511
前一步驟：511
當前步驟：512
16.5.8\textrm SAL 語義的回顧，3512
16.6宏擴展語義512
16.6.1棧語義分析513
非形式設計描述516
[1] 運行時狀態516
[2] 宏擴展516
[3] 閉包的實現517
[4] 編譯狀態 ------ 編譯時規約517
[5] 編譯狀態 ------ 字典517
執行518
16.6.2句法類型519
16.6.3編譯時類型519
16.6.4運行時語義類型519
16.6.5運行時狀態520
16.6.6運行時棧操作520
16.6.7運行時棧搜尋變數值520
16.6.8宏擴展函式521
[0] 程式宏擴展521
前一步驟：521
當前步驟：522
[1] 常量表達式宏擴展522
前一步驟：522
當前步驟：522
[2] 變數表達式宏擴展522
前一步驟：522
當前步驟：522
[3] 前綴表達式宏擴展523
前一步驟：523
當前步驟：523
[4] 中綴表達式宏擴展523
前一步驟：523
當前步驟：523
[5] 條件表達式宏擴展524
前一步驟：524
當前步驟：524
[6] lambda 表達式宏擴展524
前一步驟：524
當前步驟：524
[7] 簡單 Let 表達式的宏擴展525
前一步驟：525
當前步驟：525
塊宏擴展525
[8] 遞歸函式/Let 表達式宏擴展527
前一步驟：527
當前步驟：527
[9] 函式套用表達式宏擴展528
前一步驟：528
當前步驟：528
16.6.9\textrm SAL 語義的回顧，4528
16.7ASM：一個彙編語言529
16.7.1語義類型529
16.7.2計算機狀態530
16.7.3地址概念530
16.7.4機器指令530
16.7.5機器語義532
解釋代碼532
確定標號索引533
立即存儲和存儲指令533
立即裝入和裝入指令533
套用函式指令534
無條件轉移指令536
條件轉移指令536
暫存器傳送和調整指令537
封裝和解封裝指令537
輸出指令537
結束指令538
16.7.6ASM 的回顧538
16.8一個編譯算法538
16.8.1句法類型539
16.8.2編譯時類型和狀態539
16.8.3編譯時動態函式539
16.8.4編譯時靜態函式539
16.8.5運行時常量值540
16.8.6編譯函式540
[0] 程式編譯540
前一步驟：540
當前步驟：541
[1] 常量表達式編譯541
前一步驟：541
當前步驟：541
[2] 變數表達式編譯541
前一步驟：541
當前步驟：542
[3] 前綴表達式編譯543
前一步驟：543
當前步驟：543
[4] 中綴表達式編譯543
前一步驟：543
當前步驟：543
[5] 條件表達式編譯543
前一步驟：543
當前步驟：544
[6] Lambda 表達式編譯544
前一步驟：544
當前步驟：544
[7] 簡單 Let 表達式編譯545
前一步驟：545
當前步驟：545
[*] 塊表達式545
前一步驟：545
當前步驟：546
[8] 遞歸函式/Let 表達式編譯546
前一步驟：546
當前步驟：547
[9] 函式套用表達式編譯547
前一步驟：547
當前步驟：548
16.8.7編譯算法的回顧548
16.9一個屬性語法語義548
16.9.1抽象句法類型549
16.9.2\textrm SAL BNF 語法，1549
16.9.3結點屬性550
16.9.4常量550
16.9.5一些排印區別550
16.9.6編譯函式550
[0] 程式編譯550
[1] 常量表達式編譯550
[2] 變數表達式編譯550
前一步驟：551
當前步驟：551
[3] 前綴表達式編譯551
[4] 中綴表達式編譯551
[5] 條件表達式編譯551
[6] lambda 表達式編譯551
前一步驟：552
當前步驟：552
前一步驟：552
當前步驟：552
[7] 簡單 let 表達式編譯552
前一步驟：553
當前步驟：553
前一步驟：553
當前步驟：553
[*] 塊表達式編譯553
前一步驟：554
當前步驟：554
[8] 遞歸函式/let 表達式編譯554
[9] 函式套用表達式編譯554
前一步驟：555
當前步驟：555
16.9.7屬性語義回顧，1555
前一步驟：556
當前步驟：556
16.10另一個屬性語法語義556
前一步驟：557
當前步驟：557
16.10.1抽象句法類型557
16.10.2\textrm SAL BNF 語法，2557
前一步驟：558
當前步驟：558
16.10.3全局變數558
前一步驟：559
當前步驟：559
16.10.4常量559
16.10.5結點屬性560
16.10.6編譯函式560
[0] 程式編譯560
[1] 常量表達式編譯560
[2] 變數表達式編譯560
[3] 前綴表達式編譯560
[4] 中綴表達式編譯560
前一步驟：561
當前步驟：561
前一步驟：561
當前步驟：561
[5] 條件表達式編譯561
[6] lambda 表達式編譯561
前一步驟：562
當前步驟：562
前一步驟：562
當前步驟：562
[7] 簡單 let 表達式編譯562
[$\bullet $] 塊表達式編譯562
前一步驟：563
當前步驟：563
[8] 遞歸函式/let 表達式編譯563
[9] 函式套用表達式編譯563
16.10.7屬性語義的回顧，2563
16.11討論563
16.11.1概述563
前一步驟：564
當前步驟：564
前一步驟：565
當前步驟：565
16.11.2原則、技術和工具565
前一步驟：566
當前步驟：566
16.12回顧和文獻評註566
前一步驟：567
當前步驟：567
前一步驟：568
當前步驟：568
前一步驟：569
當前步驟：569
16.13練習569
chapter 17SIL：簡單命令式語言571
17.1背景571
17.2句法類型572
17.2.1具體的模式性句法573
17.2.2抽象句法573
17.3命令式指稱語義573
17.3.1語義類型574
17.3.2輔助語義函式574
17.3.3語義函式574
過程指稱574
語句和表達式函式575
17.4宏擴展語義575
17.4.1句法類型576
17.4.2編譯時語義類型576
17.4.3運行時語義類型576
運行時狀態“快照”576
語義類型577
17.4.4運行時狀態聲明和初始化577
17.4.5抽象函式578
17.4.6宏578
17.5討論580
17.5.1概述580
17.5.2原則、技術和工具580
17.6文獻評註580
17.7練習581
chapter 18SMIL：簡單模組命令式語言583
18.1句法類型583
18.2指稱語義584
18.2.1語義類型584
18.2.2輔助函式584
靜態函式584
時態函式585
18.2.3語義函式585
語義函式類型585
語義函式定義586
18.3宏擴展語義586
18.3.1運行時語義類型587
18.3.2編譯/運行時語義類型587
18.3.3編譯時語義類型588
18.3.4語義函式589
18.4討論590
18.4.1概述590
18.4.2原則、技術和工具590
18.5文獻評註591
18.6練習591
chapter 19SPIL：簡單並行命令式語言586
19.1問題586
19.2句法586
19.2.1非形式句法587
進程表達式587
表達式和語句587
系統進程588
19.2.2形式句法588
19.3進程概念和語義類型589
19.3.1句法概念589
文本的589
上下文的：作用域和綁定590
上下文的：隱藏和模組化590
19.3.2機器和解釋器590
19.3.3語義概念和類型590
動作590
進程591
對象591
環境 $\rho :$ENV ------ I591
存儲 $\sigma :\Sigma $591
19.4面向進程的語義類型591
19.4.1唯一進程標識符 $\pi :\Pi $592
19.4.2堆 $\xi :\Xi $592
19.4.3輸入/輸出通道綁定593
19.4.4環境 $\rho :$ ENV594
19.4.5狀態複合 594
全局狀態595
19.5初始和輔助語義函式595
19.5.1開始函式595
19.5.2系統函式596
19.5.3綁定和分配函式596
19.5.4自由和綁定函式597
19.5.5分配函式597
19.5.6變遷循環598
19.6語義函式598
19.6.1 \CJKfamily kai下一狀態變遷函式598
19.6.2賦值語句598
19.6.3\sl case 語句599
19.6.4\sl while 循環599
19.6.5\sl repeat until 循環600
19.6.6簡單輸入/輸出進程600
19.6.7並行進程命令 601
19.6.8 \CJKfamily kaistop 進程技術細節601
19.6.9進程 \CJKfamily kaicall 命令602
19.6.10內部非確定性進程， 602
19.6.11外部非確定性進程 602
19.6.12非確定性輸入/輸出進程603
19.6.13嵌入式系統進程命令603
19.6.14 \CJKfamily kaifinish 進程技術細節604
19.7討論604
19.7.1概述604
19.7.2原則、技術和工具604
19.8文獻評註605
19.9練習605
part\ VIII\hskip 結束語609
xpart結束語609
chapter 20結束語611
20.1總結611
20.2結論：卷 1 和 2611
20.3卷 3 的預覽612
20.4“UML”化形式技術613
part\ IX\hskip 附錄615
xpart附錄615
chapter命名規則617
chapter參考文獻621
