Ⅰ 开篇 3
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
1.3.2 RSL谓词演算 10
1.3.3 具体RSL类型 11
1.3.4 λ演算＋函数 19
1.3.5 其他应用表达式 21
1.3.6 命令式结构 24
1.3.7 进程结构 25
1.3.8 简单RSL规约 26
1.4 文献评注 27
Ⅱ 规约刻面 31
2 层次与复合 31
2.1 关键问题 31
2.1.1 非形式说明 31
2.1.2 形式说明 32
2.2 初步的方法论的结论 33
2.2.1 一些定义 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 文献评注：Stanislaw Leshniewski 43
2.6 练习 43
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
3.2.4 GOTO连续 53
3.2.5 指称语义的讨论 61
3.3 计算语义 63
3.3.1 关键问题 63
3.3.2 两个例子 63
3.3.3 表达式计算 63
3.3.4 GOTO程序的计算语义 66
3.3.5 协同例程程序的计算语义 71
3.3.6 讨论 72
3.4 回顾：指称和计算 73
3.5 一些语义的创始人 74
3.5.1 John McCarthy 74
3.5.2 Peter Landin 75
3.6 练习 76
4 格局：上下文和状态 79
4.1 引言 80
4.2 问题 82
4.3 “现实世界”上下文和状态 83
4.3.1 物理系统：上下文和状态 83
4.3.2 上下文和状态 84
4.3.3 非物理系统：上下文和状态 84
4.3.4 讨论，Ⅰ 85
4.3.5 讨论，Ⅱ 86
4.4 第一次总结：上下文和状态 86
4.4.1 概述 86
4.4.2 开发原则和技术 87
4.5 程序设计语言格局 87
4.6 并发进程格局 87
4.6.1 示例 87
4.6.2 总结 92
4.7 第二次总结：上下文和状态 93
4.8 信息状态和行为状态 93
4.8.1 作为状态机数据的程序流程图 94
4.8.2 流程图≡机器 94
4.8.3 流程图机 94
4.8.4 评论 95
4.8.5 结论 95
4.9 最后的总结：上下文和状态 96
4.10 练习 97
Ⅲ 关键领域和系统刻面 101
5 时间、空间和空间／时间 101
5.1 时间 101
5.1.1 时间——基础 102
5.1.2 时间——一般问题 104
5.1.3 时间的“A序列”和“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
5.3 空间／时间 113
5.3.1 指导示例 113
5.3.2 空间／时间的表示 114
5.3.3 Blizard的时间空间理论 114
5.4 讨论 115
5.5 文献评注 115
5.6 练习 115
Ⅳ 语言学 121
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
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
7.6.4 不动点求值 134
7.7 操作和计算语义 135
7.7.1 栈语义 135
7.7.2 属性语法语义 135
7.8 证明规则语义 139
7.9 讨论 141
7.9.1 概述 141
7.9.2 原则、技术和工具 141
7.10 文献评注 142
7.11 练习 142
8 句法 145
8.1 问题 145
8.1.1 形式和内容：句法和语义 145
8.1.2 本章的结构和内容 146
8.2 句子和语义结构 146
8.2.1 概述 147
8.2.2 句子结构示例 147
8.2.3 语义结构示例 149
8.3 第一个抽象句法，John McCarthy 152
8.3.1 分析语法：观测器和选择器 152
8.3.2 合成语法：生成器 153
8.4 BNF语法≈具体句法 153
8.4.1 BNF语法 154
8.4.2 BNF？RSL语法解析树关系 154
8.5 结构生成器和识别器 156
8.5.1 上下文无关语法和语言 156
8.5.2 语法解析树 157
8.5.3 正则表达式和语言 159
8.5.4 语言识别器 160
8.6 XML：可扩展标记语言（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
8.7.2 其他存储模型的抽象句法 169
8.8 转换RSL类型到BNF 170
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
9 符号体系 180
9.1 符号体系＝句法？语义？语用 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
9.5.4 系统图语言 195
9.5.5 系统概念讨论 196
9.5.6 作为语言的系统 196
9.6 讨论 197
9.6.1 概述 197
9.6.2 原则、技术和工具 197
9.7 Charles Sanders Peirce 197
9.8 文献评注 197
9.9 练习 198
Ⅴ 其他规约技术 205
10 模块化 205
10.1 前言 206
10.1.1 一些示例 206
10.1.2 预备性讨论 211
10.1.3 章节结构 213
10.2 RSL类、对象和模式 213
10.2.1 介绍RSL“类”概念 214
10.2.2 RSL“类”概念 217
10.2.3 RSL“对象”概念 218
10.2.4 RSL“模式”概念 218
10.2.5 RSL“模式”参数化 223
10.2.6 “大型”示例 226
10.2.7 定义：类、模式和对象 230
10.3 UML和RSL 231
10.3.1 UML图概述 231
10.3.2 类图 232
10.3.3 类图 232
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
10.4.2 原则、技术和工具 239
10.5 文献评注 239
10.6 练习 239
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 有限状态自动机形式化，Ⅰ 250
11.3.8 有限状态自动机实现，Ⅰ 250
11.3.9 有限状态自动机形式化，Ⅱ 251
11.3.10 有限状态自动机实现，Ⅱ 252
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
Ⅵ 并发和时态 267
12 佩特里网 267
12.1 问题 267
12.2 条件事件网（Condition Event Net,CEN） 268
12.2.1 描述 268
12.2.2 CEN小示例 268
12.2.3 条件事件网的RSL模型 271
12.3 位置变迁网（Place Transition Net,PTN） 273
12.3.1 描述 274
12.3.2 PTN小例子 274
12.3.3 位置变迁网的RSL模型 275
12.3.4 铁路领域佩特里网示例 278
12.4 染色佩特里网（Coloured Petri Net,CPN） 282
12.4.1 描述 282
12.4.2 CPN示例 283
12.4.3 染色佩特里网RSL模型 285
12.4.4 时间化染色佩特里网 289
12.5 CEN示例：工作流系统 290
12.5.1 项目计划 290
12.5.2 项目活动 293
12.5.3 项目生成 300
12.6 CPN和RSL示例：超标量处理器 302
12.6.1 描述 302
12.6.2 染色佩特里网 303
12.6.3 RSL模型：超标量处理器 308
12.7 讨论 316
12.8 文献评注 317
12.9 练习 317
13 消息和活序列图 319
13.1 消息序列图 319
13.1.1 问题 319
13.1.2 基本MSC(Basic MSC,BMSC) 320
13.1.3 高级MSC(High-Level MSC,HMSC) 326
13.1.4 HMSC句法的RSL模型 326
13.1.5 MSC是HMSC 327
13.1.6 MSC的句法良构性 328
13.1.7 示例：IEEE 802.11无线网络 333
13.1.8 基本消息序列图的语义 342
13.1.9 高级消息序列图的语义 343
13.2 活序列图：非形式闸述 344
13.2.1 活序列图句法 344
13.2.2 活序列图示例，Ⅰ 348
13.3 进程代数 350
13.3.1 进程代数PA∈ 350
13.3.2 PA∈语义 356
13.3.3 进程代数PAc∈ 359
13.3.4 PAc∈的语义 361
13.4 活序列图的代数语义 364
13.4.1 活序列图的文本句法 364
13.4.2 活序列图语义 364
13.4.3 活序列图实例，Ⅱ 368
13.5 关联消息图到RSL 368
13.5.1 集成的类型 368
13.5.2 RSL子集 369
13.5.3 关联活序列图到RSL 371
13.5.4 检查满足性 377
13.5.5 工具支持 377
13.6 通信事务进程（Communicating Transaction Processes,CTP） 378
13.6.1 直观理解 378
13.6.2 阐述CTP 379
13.6.3 哲学家就餐示例 384
13.6.4 CTP形式化 387
13.7 讨论 400
13.7.1 概述 400
13.7.2 原则、技术和工具 401
13.8 文献评注 401
13.9 练习 402
14 状态图 406
14.1 前言 406
14.2 状态图的描述 407
14.3 状态图句法的RSL模型 411
14.4 例 413
14.4.1 铁路线路自动闭塞 413
14.4.2 铁路线路方向协议系统 417
14.4.3 无线雨量计 421
14.5 状态图的进程代数 426
14.5.1 SPL（Statechart Process Language）：状态图进程语言 427
14.5.2 SPL语义 427
14.5.3 SPL项等价 428
14.6 状态图语义 429
14.6.1 状态图的SPL语义 429
14.6.2 状态图示例 431
14.7 关联状态图到RSL 431
14.7.1 句法限制 431
14.7.2 满足关系 433
14.7.3 满足检查 433
14.7.4 工具支持 434
14.8 讨论 434
14.8.1 概述 434
14.8.2 原则、技术和工具 434
14.9 文献评注 435
14.10 练习 435
15 时间的定量模型 441
15.1 问题 441
15.1.1 软时态 441
15.1.2 硬时态 442
15.1.3 软实时和硬实时 442
15.1.4 例子——“老方法”！ 442
15.1.5 本章的结构 443
15.2 时态逻辑 444
15.2.1 问题 444
15.2.2 哲学语言学背景 444
15.2.3 区间时态逻辑，ITL 445
15.2.4 经典时态操作符：◇,□ 450
15.3 时段演算 450
15.3.1 例子，第Ⅰ部分 451
15.3.2 一些基础概念 451
15.3.3 例子，第Ⅱ部分 454
15.3.4 句法 457
15.3.5 非形式语义 459
15.3.6 例子，第Ⅲ部分 460
15.3.7 变迁和事件 469
15.3.8 讨论：从领域到设计 473
15.4 TRSL：具有时间的RSL 473
15.4.1 TRSL的设计标准 474
15.4.2 TRSL语言 476
15.4.3 另一个煤气灶的例子 477
15.4.4 讨论 480
15.5 具有时间和时段的RSL 480
15.5.1 TRSL的回顾 480
15.5.2 TRSL和时段演算 481
15.6 讨论 483
15.6.1 一般问题 483
15.6.2 原则、技术和工具 484
15.7 文献评注 484
15.8 练习 485
Ⅶ 解释器和编译器定义 489
16 SAL：简单应用式语言 489
16.1 提示 489
16.2 SAL句法 490
16.2.1 SAL句法的非形式说明 490
16.2.2 SAL句法的形式说明 490
16.2.3 评论 491
16.3 指称语义 491
16.3.1 非形式语义 491
16.3.2 形式语义 492
16.3.3 SAL语义的回顾，1 493
16.3.4 两句题外话 494
16.4 一阶应用式语义 496
16.4.1 句法类型 496
16.4.2 语义类型 496
16.4.3 抽象函数 497
16.4.4 辅助函数 498
16.4.5 语义函数 498
16.4.6 回顾 501
16.4.7 SAL语义的回顾，2 501
16.5 抽象命令式栈语义 502
16.5.1 设计决策——非形式动机说明 502
16.5.2 语义风格评论 502
16.5.3 句法类型 503
16.5.4 语义类型 503
16.5.5 抽象函数 503
16.5.6 运行时函数 503
16.5.7 语义函数 505
16.5.8 SAL语义的回顾，3 510
16.6 宏扩展语义 510
16.6.1 栈语义分析 511
16.6.2 句法类型 516
16.6.3 编译时类型 516
16.6.4 运行时语义类型 516
16.6.5 运行时状态 517
16.6.6 运行时栈操作 517
16.6.7 运行时栈搜索变量值 517
16.6.8 宏扩展函数 518
16.6.9 SAL语义的回顾，4 525
16.7 ASM：一个汇编语言 526
16.7.1 语义类型 526
16.7.2 计算机状态 526
16.7.3 地址概念 527
16.7.4 机器指令 527
16.7.5 机器语义 529
16.7.6 ASM的回顾 534
16.8 一个编译算法 534
16.8.1 句法类型 535
16.8.2 编译时类型和状态 535
16.8.3 编译时动态函数 535
16.8.4 编译时静态函数 535
16.8.5 运行时常量值 536
16.8.6 编译函数 536
16.8.7 编译算法的回顾 544
16.9 一个属性语法语义 544
16.9.1 抽象句法类型 545
16.9.2 SAL BNF语法，1 545
16.9.3 结点属性 546
16.9.4 常量 546
16.9.5 一些排印区别 546
16.9.6 编译函数 546
16.9.7 属性语义回顾，1 551
16.10 另一个属性语法语义 552
16.10.1 抽象句法类型 553
16.10.2 SAL BNF语法，2 553
16.10.3 全局变量 554
16.10.4 常量 555
16.10.5 结点属性 556
16.10.6 编译函数 556
16.10.7 属性语义的回顾，2 559
16.11 讨论 559
16.11.1 概述 559
16.11.2 原则、技术和工具 561
16.12 回顾和文献评注 562
16.13 练习 565
17 SIL：简单命令式语言 567
17.1 背景 567
17.2 句法类型 567
17.2.1 具体的模式性句法 568
17.2.2 抽象句法 568
17.3 命令式指称语义 568
17.3.1 语义类型 569
17.3.2 辅助语义函数 569
17.3.3 语义函数 569
17.4 宏扩展语义 570
17.4.1 句法类型 571
17.4.2 编译时语义类型 571
17.4.3 运行时语义类型 571
17.4.4 运行时状态声明和初始化 572
17.4.5 抽象函数 573
17.4.6 宏 573
17.5 讨论 575
17.5.1 概述 575
17.5.2 原则、技术和工具 575
17.6 文献评注 575
17.7 练习 576
18 SMIL：简单模块命令式语言 577
18.1 句法类型 577
18.2 指称语义 578
18.2.1 语义类型 578
18.2.2 辅助函数 578
18.2.3 语义函数 579
18.3 宏扩展语义 580
18.3.1 运行时语义类型 581
18.3.2 编译／运行时语义类型 581
18.3.3 编译时语义类型 582
18.3.4 语义函数 583
18.4 讨论 584
18.4.1 概述 584
18.4.2 原则、技术和工具 584
18.5 文献评注 585
18.6 练习 585
19 SPIL：简单并行命令式语言 586
19.1 问题 586
19.2 句法 586
19.2.1 非形式句法 587
19.2.2 形式句法 588
19.3 进程概念和语义类型 589
19.3.1 句法概念 589
19.3.2 机器和解释器 590
19.3.3 语义概念和类型 590
19.4 面向进程的语义类型 591
19.4.1 唯一进程标识符π:П 592
19.4.2 堆ξ:Ξ 592
19.4.3 输入／输出通道绑定 593
19.4.4 环境ρ:ENV 594
19.4.5 状态复合Ψ,Γ,Ξ,∑,Ω 594
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 下一状态变迁函数 598
19.6.2 赋值语句 598
19.6.3 case语句 599
19.6.4 while循环 599
19.6.5 repeat until循环 600
19.6.6 简单输入／输出进程 600
19.6.7 并行进程命令，‖ 601
19.6.8 stop进程技术细节 601
19.6.9 进程call命令 602
19.6.10 内部非确定性进程，？ 602
19.6.11 外部非确定性进程，？ 602
19.6.12 非确定性输入／输出进程 603
19.6.13 嵌入式系统进程命令 603
19.6.14 finish进程技术细节 604
19.7 讨论 604
19.7.1 概述 604
19.7.2 原则、技术和工具 604
19.8 文献评注 605
19.9 练习 605
Ⅷ 结束语 611
20 结束语 611
20.1 总结 611
20.2 结论：卷1和2 611
20.3 卷3的预览 612
20.4 “UML”化形式技术 613
Ⅸ 附录 617
命名规则 617
参考文献 621