軟體工程卷2：系統與語言規約

《軟體工程卷2：系統與語言規約》是2009年清華大學出版社出版的圖書，作者是Dines Bjorner。

基本介紹

• 中文名：軟體工程卷2：系統與語言規約
• 別名：系統與語言規約
• 作者：Dines Bjorner
• 譯者：劉伯超
• 出版社：清華大學出版社
• 出版時間：2009年12月8日
• 定價：79 元
• 裝幀：平裝
• ISBN：9787302208914 

圖書簡介

本書是世界著名的計算機科學家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