软件工程卷 1 抽象与建模PDF电子书下载

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