软件工程 卷2 系统与语言规约PDF电子书下载

Ⅰ 开篇 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