软件工程卷 1 抽象与建模PDF|Epub|txt|kindle电子书版本网盘下载

软件工程卷 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 自然数：Nat36

2.3.2 整数：Int37

2.3.3 实数：Real38

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 不动点操作符Y95

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-199598

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 命题表达式，PRO131

9.4.2 例子132

9.4.3 命题求值，Eval_PRO133

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 谓词表达式的句法，PRE142

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

Ⅲ 简单RSL161

概要161

RSL与VDM-SL、Z以及B161

句法上什么构成了规约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 通信顺序进程，CSP443

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/CSP456

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