Ⅰ 开篇 3
1 绪论 3
1.1 准备 3
1.2 软件工程三部曲 5
1.2.1 软件和系统开发 6
1.2.2 三部曲引出 6
1.2.3 领域工程 6
1.2.4 需求工程 7
1.2.5 软件设计 8
1.2.6 讨论 9
1.3 文档 10
1.3.1 文档种类 10
1.3.2 时期、阶段和步骤文档 11
1.3.3 信息文档 11
1.3.4 描述文档 13
1.3.5 分析文档 16
1.4 形式技术和形式工具 18
1.4.1 关于形式技术和语言 18
1.4.2 软件工程教材中的形式技术 19
1.4.3 一些程序设计语言 19
1.4.4 一些形式规约语言 19
1.4.5 目前形式语言的不足 21
1.4.6 其他的形式工具 21
1.4.7 为什么要形式技术和形式工具 22
1.5 方和方法学 23
1.5.1 方法 23
1.5.2 方法学 23
1.5.3 讨论 23
1.5.4 元方法学 24
1.6 软件基础 24
1.6.1 教学法和范式 25
1.6.2 语用、语义和句法 25
1.6.3 规约和程序设计范式 28
1.6.4 描述、规定和规约 28
1.6.5 元语言 29
1.6.6 总结 29
1.7 目标和效果 29
1.7.1 目标 29
1.7.2 效果 30
1.7.3 讨论 30
1.8 文献评注 30
1.9 练习 31
Ⅱ 离散数学 35
2 数 35
2.1 引言 35
2.2 数符和数 35
2.3 数的子集 36
2.3.1 自然数：Nat 36
2.3.2 整数：Int 37
2.3.3 实数：Real 38
2.3.4 无理数 39
2.3.5 代数数 39
2.3.6 超越数 40
2.3.7 复数和虚数 40
2.4 类型定义：数 40
2.5 总结 41
2.6 文献评注 41
2.7 练习 42
3 集合 44
3.1 背景 44
3.2 数学的集合 45
3.3 特殊集合 46
3.3.1 外延公理 46
3.3.2 划分 46
3.3.3 幂集 47
3.4 分类和类型定义：集合 47
3.4.1 集合抽象 47
3.4.2 集合类型表达式和类型定义 47
3.4.3 分类 47
3.5 RSL中的集合 48
3.6 文献评注 48
3.7 练习 48
4 笛卡尔 50
4.1 要点 50
4.2 笛卡尔值表达式 50
4.3 笛卡尔类型 51
4.4 笛卡尔的目 52
4.5 笛卡尔的相等 52
4.6 一些构造的例子 52
4.7 分类和类型定义：笛卡尔 54
4.7.1 笛卡尔抽象 54
4.7.2 笛卡尔类型表达式和类型定义 54
4.8 RSL中的笛卡尔 55
4.9 文献评注 55
4.10 练习 55
5 类型 57
5.1 值和类型 58
5.2 现象和概念类型 58
5.2.1 现象和概念 58
5.2.2 实体：原子和复合 59
5.2.3 属性和值 59
5.3 程序设计语言类型概念 62
5.4 分类或抽象类型 64
5.5 内建和具体类型 64
5.6 类型检查 65
5.6.1 类型确定的变量和表达式 66
5.6.2 类型错误 66
5.6.3 类型错误检测 67
5.7 类型作为集合，类型作为格 67
5.8 总结 67
5.9 练习 67
6 函数 69
6.1 概述 70
6.2 要点 71
6.2.1 背景 71
6.2.2 一些函数概念 71
6.3 数足如何产生的 75
6.4 关于求值概念的题外话 76
6.4.1 求值，解释和细化 76
6.4.2 两个求值的例子 76
6.4.3 函数调用 77
6.5 函数代数 78
6.5.1 代数 78
6.5.2 函数类型 78
6.5.3 高阶函数类型 79
6.5.4 非确定性函数 79
6.5.5 常量函数 79
6.5.6 严格函数 80
6.5.7 严格函数和严格函数调用 80
6.5.8 函数上的操作 81
6.6 Curry化和λ记法 82
6.6.1 Curry化 82
6.6.2 λ记法 82
6.6.3 Curry化和λ记法的例子 83
6.7 关系和函数 83
6.7.1 谓词 84
6.7.2 通过关系搜索的函数求值 84
6.7.3 非确定性函数 85
6.8 类型定义 85
6.9 结论 85
6.10 文献评注 85
6.11 练习 86
7 λ演算 87
7.1 非形式介绍 87
7.2 “纯”λ演算句法 88
7.3 λ演算的语用 89
7.4 “纯”λ演算语义 89
7.4.1 自由和约束变量 90
7.4.2 绑定和辖域 90
7.4.3 变量的冲突和混淆 90
7.4.4 代入 90
7.4.5 α转换和β转换规则 91
7.4.6 λ转换 91
7.5 名调用和值调用 93
7.6 Church Rosser定理——非形式版本 93
7.7 RSLλ记法 93
7.7.1 扩展λ表达式 93
7.7.2 “let...in...end”结构 94
7.8 不动点 94
7.8.1 要点 94
7.8.2 非形式概述 95
7.8.3 不动点操作符Y 95
7.8.4 不动点求值 96
7.9 讨论 97
7.9.1 概述 97
7.9.2 关于最小、最大、全部不动点 97
7.9.3 强调 97
7.9.4 原则、技术和工具 98
7.10 文献评注 98
7.10.1 参考文献 98
7.10.2 Alonzo Church,1903-1995 98
7.11 练习 98
8 代数 101
8.1 引言 101
8.2 代数概念的形式定义 101
8.3 代数是如何产生的 102
8.4 代数的种类 103
8.4.1 具体代数 103
8.4.2 抽象代数 104
8.4.3 异构代数 104
8.4.4 泛代数 105
8.5 规约代数 106
8.5.1 表达代数的句法方式 106
8.5.2 一个栈代数的例子 106
8.5.3 一个队列代数的例子 107
8.5.4 “类”表达式的语义模型 108
8.6 代数规约的RSL句法 109
8.6.1 “类”表达式 109
8.6.2 “模式”声明 109
8.7 讨论 110
8.7.1 概述 110
8.7.2 原则、技术与工具 110
8.8 文献评注 110
8.9 练习 111
9 数理逻辑 112
9.1 要点 112
9.1.1 布尔基项语言 113
9.1.2 命题表达式语言 113
9.1.3 谓词表达式语言 113
9.1.4 布尔值表达式 114
9.1.5 “chaos”——未定义的表达式求值 114
9.1.6 公理系统和推理规则 114
9.1.7 证明系统 115
9.1.8 有关两个公理系统的注解 116
9.1.9 “if...then...else...end”联结词 116
9.1.10 讨论 117
9.2 证明论和模型论 117
9.2.1 句法 117
9.2.2 语语义 118
9.2.3 句法和语义 118
9.2.4 形式逻辑：句法和语义 118
9.2.5 和证明相关的问题 121
9.2.6 联系证明论和模型论 121
9.2.7 讨论 123
9.3 布尔基项语言 123
9.3.1 句法和语义 123
9.3.2 联结词：～，∧，∨，？，＝，≠，≡ 124
9.3.3 三值逻辑 125
9.3.4 基项和它们的求值 127
9.3.5 “句法”和“语义的语义” 130
9.3.6 讨论 131
9.4 命题逻辑语言 131
9.4.1 命题表达式，PRO 131
9.4.2 例子 132
9.4.3 命题求值，Eval_PRO 133
9.4.4 二值命题演算 134
9.4.5 讨论 136
9.5 谓词逻辑语言 136
9.5.1 动机 136
9.5.2 非形式介绍 137
9.5.3 例 138
9.5.4 量词和量化表达式 140
9.5.5 谓词表达式的句法，PRE 142
9.5.6 一个谓词演算 143
9.5.7 谓词表达式求值 145
9.5.8 一阶和高阶逻辑 147
9.5.9 永真、可满足性和模型 148
9.5.10 讨论 149
9.6 公理系统 149
9.6.1 概述 150
9.6.2 公理 150
9.6.3 公理系统 151
9.6.4 一致性和完全性 151
9.6.5 面向性质的规约 152
9.6.6 讨论 157
9.7 总结 157
9.8 文献评注 158
9.9 练习 159
Ⅲ 简单RSL 161
概要 161
RSL与VDM-SL、Z以及B 161
句法上什么构成了规约 162
一个关于RSL的“标准” 162
RSL工具 163
10 RSL中的原子类型和值 165
10.1 引言 165
10.1.1 数学与企业建模 165
10.1.2 “原始的”模型构造块 166
10.2 RSL中的数 166
10.2.1 三种数的类型 166
10.2.2 RSL中数的操作 167
10.3 枚举标记 167
10.3.1 动机 167
10.3.2 一般理论 167
10.3.3 标识上的操作 169
10.3.4 抽象模型中的枚举标记 169
10.3.5 用枚举标记来建模 170
10.4 字符和文本 171
10.4.1 动机 171
10.4.2 字符和文本数据类型 171
10.5 标识符与一般标记 172
10.5.1 标识符 172
10.5.2 一般标记上的操作 173
10.5.3 一般标记 173
10.6 讨论 174
10.6.1 概要 174
10.6.2 对原子实体建模 174
10.7 练习 175
11 RSL中的函数定义 177
11.1 函数类型 177
11.1.1 函数类型的句法 177
11.1.2 →和？的非形式语义 178
11.2 面向模型的显式定义 178
11.3 面向模型的公理定义 179
11.4 面向模型的前置／后置条件定义 180
11.5 面向性质的公理定义 181
11.6 面向性质的代数定义 182
11.7 RSL函数定义风格的小结 183
11.8 讨论 184
11.9 练习 184
12 面向性质与面向模型的抽象 186
12.1 抽象 187
12.1.1 关键问题 187
12.1.2 抽象与规约 187
12.1.3 论抽象 188
12.2 面向性质的抽象 189
12.2.1 面向性质的规约的语用 189
12.2.2 面向性质的规约的符号关系学 190
12.2.3 面向性质的规约的语义 193
12.2.4 讨论 193
12.3 模型与性质抽象 193
12.3.1 表示与操作抽象 194
12.3.2 面向性质与面向模型的抽象 194
12.3.3 定义 195
12.3.4 表示抽象的例子 195
12.3.5 操作抽象的例子 198
12.3.6 讨论 200
12.4 面向模型的抽象 201
12.4.1 后续六章的一个极短概述 201
12.4.2 模型与模型 202
12.4.3 不充分规约 202
12.4.4 确定性和不确定性 203
12.4.5 为什么需要宽松规约 204
12.4.6 讨论 204
12.5 原则、技术与工具 204
12.5.1 面向性质与面向模型的规约 205
12.5.2 面向性质的规约的风格 205
12.5.3 面向模型的规约的风格 206
12.5.4 隐函数和显函数 207
12.5.5 请不要混淆！ 207
12.5.6 有关观测器函数的注释 208
12.6 练习 210
13 RSL中的集合 212
13.1 集合：关键问题 213
13.2 集合数据类型 213
13.2.1 集合类型：定义和表达式 213
13.2.2 集合值表达式 214
13.2.3 集合绑定模式与匹配 219
13.2.4 非确定性 220
13.3 基于集合的抽象的例子 220
13.3.1 表示Ⅰ 220
13.3.2 文件系统Ⅰ 221
13.3.3 表示Ⅱ 222
13.4 使用集合进行抽象和建模 223
13.4.1 网络建模 223
13.4.2 伪层次建模 225
13.4.3 对电话系统的建模 227
13.5 集合的归纳定义 231
13.5.1 集合类型的归纳定义 231
13.5.2 集合值的归纳定义 232
13.6 关于变化的集合的注释 234
13.7 原则、技术和工具 235
13.8 讨论 236
13.9 文献评注 236
13.10 练习 236
14 RSL中的笛卡尔 240
14.1 笛卡尔：关键问题 240
14.2 笛卡尔数据类型 241
14.2.1 笛卡尔类型和笛卡尔表达式 241
14.2.2 笛卡尔值表达式 242
14.2.3 笛卡尔操作，Ⅰ 243
14.2.4 笛卡尔绑定模式和匹配 243
14.2.5 笛卡尔操作，Ⅱ 244
14.3 笛卡尔抽象的例子 244
14.3.1 件系统Ⅱ 244
14.3.2 库拉托夫斯基（Kuratowski）：对和集合 245
14.4 用笛卡尔进行抽象与建模 247
14.4.1 句法结构建模 247
14.4.2 笛卡尔“let...in...end”绑定 251
14.4.3 语义结构建模 252
14.4.4 笛卡尔：初步的讨论 254
14.5 归纳笛卡尔定义 255
14.5.1 归纳笛卡尔类型定义 255
14.5.2 笛卡尔值的归纳定义 255
14.6 讨论 257
14.6.1 概述 257
14.6.2 原则、技术和工具 258
14.7 练习 258
15 RSL中的列表 262
15.1 与列表相关的一些观点 262
15.2 列表数据类型 263
15.2.1 列表类型 263
15.2.2 列表值表达式 264
15.2.3 列表的绑定模式与匹配 267
15.2.4 列表：确定性和非确定性的回顾 268
15.3 基于列表的抽象的小例子 268
15.3.1 表示 268
15.3.2 堆栈和队列 269
15.3.3 文件系统Ⅲ 270
15.3.4 排序算法 272
15.4 使用列表进行抽象与建模 273
15.4.1 使用列表对书进行建模 273
15.4.2 “上下文中的关键字（KeyWord-In-Context,KWIC）”的建模 274
15.5 列表的归纳定义 279
15.5.1 列表类型的归纳定义 279
15.5.2 列表值的归纳定义 280
15.6 列表抽象和模型的回顾 281
15.7 列表讨论 282
15.8 练习 282
16 RSL中的映射 286
16.1 关键问题 286
16.2 映射数据类型 287
16.2.1 映射类型：定义和表达式 287
16.2.2 映射值表达式 288
16.2.3 映射的绑定模式与匹配 291
16.2.4 非确定性 292
16.3 基于映射抽象的例子 292
16.3.1 排序 292
16.3.2 等价关系 292
16.4 使用映射进行抽象与建模 293
16.4.1 图 293
16.4.2 结构化的表 295
16.4.3 层次结构 297
16.4.4 关系文件系统（Ⅳ）和数据库 300
16.4.5 复杂指针数据结构 303
16.4.6 数据结构的良构性 312
16.4.7 讨论 316
16.5 映射的归纳定义 316
16.5.1 映射类型的归纳定义 316
16.5.2 映射值的归纳定义 317
16.6 映射抽象和建模的回顾 319
16.7 映射：讨论 321
16.8 练习 321
17 RSL中的高阶函数 325
17.1 函数：关键问题 325
17.2 使用基于函数的抽象的例子 326
17.2.1 泛函 326
17.2.2 讨论 327
17.3 用函数进行抽象与建模 327
17.3.1 函数作为概念 327
17.3.2 操作符提升 330
17.4 函数的归纳定义 336
17.4.1 函数类型的归纳定义 336
17.4.2 函数值的归纳定义 337
17.5 函数抽象与建模的回顾 337
17.6 讨论 338
17.7 练习 338
Ⅳ 规约类型 341
18 RSL中的类型 341
18.1 关键问题 341
18.2 类型范畴 342
18.2.1 抽象类型：分类 342
18.2.2 具体类型 342
18.2.3 讨论 343
18.3 枚举标记类型的回顾 343
18.4 记录：构造器和析构器 344
18.4.1 概要 344
18.4.2 变体记录值的归纳公理 345
18.4.3 一个例子 346
18.5 联合类型的定义 347
18.6 短记录类型的定义 347
18.7 类型表达式，回顾 348
18.8 类型 348
18.9 类型定义，回顾 349
18.10 关于递归类型定义 349
18.11 讨论 349
18.11.1 概要 349
18.11.2 原则、技术和工具 350
18.12 文献评注 350
18.13 练习 350
Ⅴ 规约程序设计 353
关于规约程序设计 353
关于问题与练习 354
19 应用式规约程序设计 355
19.1 作用域与绑定 355
19.1.1 绑定模式——非形式说明 356
19.1.2 “let”结构的作用域和绑定［1］ 357
19.1.3 函数定义作用域与绑定［2］ 358
19.1.4 “case”结构的作用域和绑定［3］ 358
19.1.5 内涵：作用域和绑定［4］ 359
19.1.6 量化：作用域和绑定［5］ 360
19.2 直观理解 360
19.2.1 简单“let a=εd in εb(a)end” 360
19.2.2 递归“let f（a）＝εd(f)in εb(f,a)end” 360
19.2.3 直谓“let a:A·ρ（a）in ε（a）end” 361
19.2.4 多个“let ai＝εdi in εb(ai)end” 361
19.2.5 文字和标识符 362
19.3 操作符／操作数表达式 362
19.4 枚举和内涵表达式 363
19.5 条件表达式 363
19.6 绑定、确定类型、模式和匹配 365
19.6.1 问题 365
19.6.2 绑定和模式的本质 366
19.6.3 绑定模式 367
19.6.4 给定类型 371
19.6.5 选择模式和绑定 372
19.6.6 总结 378
19.7 回顾和讨论 378
19.7.1 概述 378
19.7.2 原则和技术 378
19.8 文献评注 379
19.9 练习 379
20 命令式规约程序设计 388
20.1 直观理解 388
20.2 命令式组合子：一个λ演算 389
20.2.1 ［0］“变量”声明 389
20.2.2 ［1］赋值：“var:=expression” 391
20.2.3 ［9］ 状态表达式 391
20.2.4 ［2］“skip”：无动作 391
20.2.5 ［3］ 语句序列（；） 391
20.2.6 ［4］“if...then...else...end” 391
20.2.7 ［5-6］“while...do...end”和“do...until...end” 392
20.2.8 ［7］“case...of...end” 392
20.2.9 ［8］“for...in...do...end” 392
20.3 变量引用：指针 393
20.3.1 简单引用的介绍 393
20.3.2 动态分配和引用 393
20.3.3 讨论：先语义，后句法 398
20.3.4 讨论：类型同态 398
20.3.5 状态的概念 398
20.4 函数定义和表达式 399
20.4.1 Unit类型表达式，Ⅰ 399
20.4.2 命令式函数 399
20.4.3 读／写访问描述 400
20.4.4 局部变量 400
20.4.5 Unit类型表达式，Ⅱ 400
20.4.6 纯表达式 401
20.4.7 只读表达式 401
20.4.8 等价（≡）和相等（＝） 402
20.5 转化：应用式到命令式 403
20.5.1 应用式到命令式的转化 403
20.5.2 递归到迭代的转化 404
20.5.3 应用式到命令式的模式 405
20.5.4 正确性、原则、技术、工具 412
20.6 配置建模的风格 412
20.6.1 应用式上下文和状态 412
20.6.2 应用式上下文和命令式状态 416
20.6.3 命令式上下文和状态 418
20.6.4 顺序模型的总结 421
20.7 回顾和讨论 421
20.7.1 回顾 421
20.7.2 讨论 421
20.8 文献评注 422
20.8.1 计算理论 422
20.8.2 λ演算的类型理论 422
20.8.3 源程序转换著作 422
20.8.4 命令式程序设计原理 423
20.9 练习 423
21 并发式规约程序设计 426
21.1 行为和进程抽象 427
21.1.1 引言 427
21.1.2 关于进程和其他的抽象 427
21.2 直观介绍 428
21.2.1 说明性的会合场景 428
21.2.2 图和记法总结 431
21.2.3 关于迹语义 432
21.2.4 一些描述：进程，等等 433
21.2.5 进程建模原则 434
21.2.6 非形式的例子 435
21.2.7 一些建模评论——题外话 439
21.2.8 例（续） 439
21.2.9 一些系统的通道格局 441
21.2.10 并发概念——总结 441
21.3 通信顺序进程，CSP 443
21.3.1 导言：进程和事件 443
21.3.2 进程组合子等等 444
21.3.3 讨论 447
21.4 RSL/CSP进程组合子 447
21.4.1 类RSL通道 447
21.4.2 RSL通信子句 448
21.4.3 RSL进程 448
21.4.4 并行进程组合子 450
21.4.5 非确定性外部选择 451
21.4.6 非确定性内部选择 451
21.4.7 互锁组合子 451
21.4.8 总结 452
21.4.9 提示 452
21.5 翻译模式 452
21.5.1 阶段Ⅰ：应用式模式 453
21.5.2 阶段Ⅱ：简单重构 453
21.5.3 阶段Ⅲ：引入并行 453
21.5.4 阶段Ⅳ：简单重构 454
21.5.5 阶段关系 455
21.5.6 阶段Ⅴ：命令式重构 455
21.5.7 一些评论 456
21.6 并行和并发：讨论 456
21.6.1 CSP和RSL/CSP 456
21.6.2 建模技巧 456
21.7 文献评注 457
21.8 练习 457
Ⅵ 其他 465
22 其他 465
22.1 我们讨论了什么 465
22.2 下一个讨论什么 465
22.3 下一个的下一个讨论什么 465
22.4 提示 466
22.5 “轻量级”形式方法 467
22.6 文献评注 467
Ⅶ 附录 471
A 共同练习题目 471
A.1 运输网络 471
A.2 集装箱物流 471
A.3 金融服务行业 472
A.4 练习参考总结 473
B 术语表 474
B.1 参考列表的种类 475
B.1.1 术语 475
B.1.2 词典 475
B.1.3 百科全书 475
B.1.4 本体论 475
B.1.5 分类学 475
B.1.6 术语学 476
B.1.7 类属词典 476
B.2 印刷格式和拼写 476
B.3 术语表 476
参考文献 545