原著作者为中文版所作的序
译者序v\\[1mm]
前言\hfill vii\\[1mm]
丛书成因viii
丛书的不足ix
着手方法x
软件新观x
“轻量级”形式技术xi
“超级程序设计师”xi
何为软件工程xii
作者的愿望xiii
这几卷在软件工程教育课程中的作用xiii
为什么这么多材料xvi
课程中如何使用这套丛书xvi
本书的简要介绍xvii
本卷的简要介绍xvii
致谢xviii
开篇1
开篇1
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
软件：代码和文档8
软件设计，I8
开发时期、阶段和步骤9
软件设计，II9
1.2.6讨论9
一般问题9
1.3文档10
1.3.1文档种类10
1.3.2时期、阶段和步骤文档11
1.3.3信息文档11
当前情况文档编制11
需要文档编制11
产品概念和措施11
设计概要12
范围和区间描述12
纲要12
合同12
讨论12
1.3.4描述文档13
描述文档种类和类型13
粗略描述13
术语14
叙述14
形式模型15
讨论15
1.3.5分析文档16
粗略描述分析和概念形成16
描述、规定和规约的确认16
规约属性的验证17
开发时期、阶段或步骤变迁的正确性17
讨论18
1.4形式技术和形式工具18
1.4.1关于形式技术和语言18
1.4.2软件工程教材中的形式技术19
1.4.3一些程序设计语言19
1.4.4一些形式规约语言19
关于面向模型的规约语言19
关于面向性质的规约语言20
关于面向性质\面向模型的规约语言20
再论程序设计语言20
规约语言续20
1.4.5目前形式语言的不足21
1.4.6其他的形式工具21
1.4.7为什么要形式技术和形式工具22
一些理由22
轶事和类比证据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
语用25
语义25
句法27
1.6.3规约和程序设计范式28
1.6.4描述、规定和规约28
软件规约、需求规定和领域描述29
1.6.5元语言29
1.6.6总结29
1.7目标和效果29
1.7.1目标29
主要目标29
一些其他的目标30
1.7.2效果30
主要效果30
一些其他的效果30
1.7.3讨论30
1.8文献评注30
1.9练习31
离散数学33
2数35
2.1引言35
2.2数符和数35
2.3数的子集36
2.3.1自然数：\bf Nat36
对一些 结构的解释37
2.3.2整数: \textbf Int37
性质37
\texttt RSL 的整数代数38
2.3.3实数：\textbf Real38
有理数39
实数上的操作39
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\texttt 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\texttt 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
原子实体属性和值59
复合实体属性和值59
讨论61
5.3程序设计语言类型概念62
一些例子62
讨论63
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
本章的结构70
特别注释71
6.2要点71
6.2.1背景71
6.2.2一些函数概念71
函数定义72
函数“映射”（图）73
函数空间和函数基调类型74
函数类别74
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.6Curry 化和 记法82
6.6.1Curry 化82
6.6.2$\lambda $ 记法82
6.6.3Curry 化和 记法的例子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$\lambda $ 演算87
7.1非形式介绍87
7.2“纯” 演算句法88
7.3$\lambda $ 演算的语用89
7.4“纯” 演算语义89
7.4.1自由和约束变量90
7.4.2绑定和辖域90
7.4.3变量的冲突和混淆90
7.4.4代入90
7.4.5$\alpha $ 转换和 $\beta $ 转换规则91
7.4.6$\lambda $ 转换91
7.5名调用和值调用93
7.6Church--Rosser 定理 ------ 非形式版本93
7.7\texttt RSL 记法 93
7.7.1扩展 表达式93
7.7.2\bf “let ... in ... end” 结构94
7.8不动点94
7.8.1要点94
7.8.2非形式概述95
7.8.3不动点操作符 \textbf 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.2Alonzo 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
态射概念105
特定种类的态射105
8.5规约代数106
8.5.1表达代数的句法方式106
8.5.2一个栈代数的例子106
一些 结构的非形式解释107
8.5.3一个队列代数的例子107
一些记法：\bf hide108
8.5.4“类”表达式的语义模型108
8.6代数规约的 句法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
公理和公理系统115
推理规则115
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
关于形式逻辑系统的更多讨论119
关于形式逻辑系统句法的更多讨论119
关于实质蕴涵的意义，$\supset $119
元语言变量120
9.2.5和证明相关的问题121
证明121
定理和形式系统理论121
一致性121
可判定性121
9.2.6联系证明论和模型论121
解释122
模型122
可满足性、衍推：$\models $ 和永真123
可靠性和完全性，$\vdash $ 和 $\models $123
9.2.7讨论123
9.3布尔基项语言123
9.3.1句法和语义123
9.3.2联结词：$\sim $, $\wedge $, $\vee $, $\Rightarrow $, $=$, $\not =$, $\equiv $124
否定，$\sim $124
合取，$\wedge $124
析取，$\vee $125
相等，=125
蕴涵，$\Rightarrow $125
恒等，$\equiv $125
9.3.3三值逻辑125
$\equiv $\ 和 =126
推理规则的形式126
真值和假值的（句法）标志符以及语义值126
布尔联结词的非交换性127
9.3.4基项和它们的求值127
布尔基项的句法，BGT128
布尔基项求值， \sf \CJKfamily heiEval\_BGT129
9.3.5“句法” 和 “语义的语义”130
9.3.6讨论131
9.4命题逻辑语言131
9.4.1命题表达式， \sf \CJKfamily heiPRO131
命题表达式的例子131
命题表达式的句法， \sf \CJKfamily heiPRO131
9.4.2例子132
9.4.3命题求值， \sf \CJKfamily heiEval\_PRO133
9.4.4二值命题演算134
前言134
一些证明概念134
公理和一条推理规则，I135
公理和推理规则，II135
9.4.5讨论136
9.5谓词逻辑语言136
9.5.1动机136
9.5.2非形式介绍137
9.5.3例138
9.5.4量词和量化表达式140
句法140
自由和约束变量141
复合量化表达式141
9.5.5谓词表达式的句法， \sf \CJKfamily heiPRE142
谓词演算的符号142
一个谓词演算的项语言142
一个谓词演算的原子公式语言142
一个谓词演算的良构公式143
谓词表达式的非形式 BNF 语法143
9.5.6一个谓词演算143
公理模式144
推理规则144
9.5.7谓词表达式求值145
求值上下文145
谓词表达式的意义和值146
求值程序， \sf \CJKfamily heiEval\_PRE146
项求值146
公式求值146
9.5.8一阶和高阶逻辑147
9.5.9永真、可满足性和模型148
上下文和解释148
永真和可满足性148
模型149
上下文、解释和模型149
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
定义 \sf \CJKfamily heiS = A\bf -set 的形式公理系统概述154
定义 \sf \CJKfamily heiL = A$^\ast $ 的形式公理系统的概述155
分析句法156
合成句法157
9.6.6讨论157
9.7总结157
9.8文献评注158
9.9练习159
\contentsline part\ III\hskip \betweenumberspace 简单 \texttt RSL161
简单 \texttt RSL161
\vspace *2mm
概要161
\texttt RSL 与 \texttt VDM-SL、Z 以及 \texttt B161
句法上什么构成了规约162
一个关于\texttt RSL的“标准”162
\texttt RSL 工具163
10\texttt RSL 中的原子类型和值165
10.1引言165
10.1.1数学与企业建模165
10.1.2“原始的” 模型构造块166
10.2\texttt RSL\ 中的数166
10.2.1三种数的类型166
自然数： \sf \CJKfamily heiNat166
整数： \sf \CJKfamily heiInt166
实数： \sf \CJKfamily heiReal166
10.2.2\texttt 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
枚举标记和有限状态设备170
枚举标记和 Linux 命令171
10.4字符和文本171
10.4.1动机171
10.4.2字符和文本数据类型171
10.5标识符与一般标记172
10.5.1标识符172
\texttt RSL\ 标识符172
论域标识符173
10.5.2一般标记上的操作173
10.5.3一般标记173
10.6讨论174
10.6.1概要174
10.6.2对原子实体建模174
10.7练习175
11\texttt RSL 中的函数定义177
11.1函数类型177
11.1.1函数类型的句法177
11.1.2$\rightarrow $ 和 \unhbox \voidb@x \hbox $\mathrel \mathop \rightarrow \limits ^\sim $ 的非形式语义178
11.2面向模型的显式定义178
11.3面向模型的公理定义179
11.4面向模型的前置/后置条件定义 180
11.5面向性质的公理定义181
11.6面向性质的代数定义182
11.7\texttt RSL\ 函数定义风格的小结183
11.8讨论184
11.9练习184
12面向性质与面向模型的抽象186
12.1抽象187
12.1.1关键问题187
建模与模型187
12.1.2抽象与规约187
12.1.3论抽象188
\hbox to\hsize \hss ``\rm \CJKfamily kai抽象作为一种基本的工具。''\hss 188
12.2面向性质的抽象189
12.2.1面向性质的规约的语用189
12.2.2面向性质的规约的符号关系学190
非形式文档190
类型和值------非形式描述190
类型和值------形式描述190
操作：192
形式描述192
12.2.3面向性质的规约的语义193
12.2.4讨论193
概要193
原则，技术与工具193
12.3模型与性质抽象193
12.3.1表示与操作抽象194
12.3.2面向性质与面向模型的抽象194
关键问题194
进一步描述194
12.3.3定义195
12.3.4表示抽象的例子195
面向性质的表示196
面向模型的表示197
12.3.5操作抽象的例子198
面向性质的规约198
面向模型的规约200
12.3.6讨论200
概述200
详细说明： \CJKfamily kai``总之，区别到底是什么？''201
12.4面向模型的抽象201
12.4.1后续六章的一个极短概述201
12.4.2模型与模型202
面向性质的规约的模型202
面向模型的规约的模型202
12.4.3不充分规约202
重点202
为什么需要不充分规约？203
12.4.4确定性和不确定性203
确定性表达式203
不确定性表达式203
12.4.5为什么需要宽松规约204
12.4.6讨论204
概要204
数学结构的顺序204
\texttt RSL 语言结构204
12.5原则、技术与工具204
12.5.1面向性质与面向模型的规约205
何时面向性质205
何时面向模型205
12.5.2面向性质的规约的风格205
混合规约风格206
12.5.3面向模型的规约的风格206
混合规约风格207
12.5.4隐函数和显函数207
12.5.5请不要混淆！207
12.5.6有关观测器函数的注释208
第一个原则：假定208
第二个原则：不“自引用”208
第三个原则：标识209
[1] 集合元素标识209
[2] 固定结构元素标识210
[3] 序列元素标识210
12.6练习210
13\texttt RSL 中的集合212
13.1集合：关键问题213
13.2集合数据类型213
13.2.1集合类型：定义和表达式213
13.2.2集合值表达式214
集合的枚举214
集合值操作符/操作数表达式215
集合操作基调和例子215
集合操作符的数学含义216
集合内涵217
集合------确定性和非确定性的回顾218
集合 ------ 模型、值和 $\equiv $\ 操作218
13.2.3集合绑定模式与匹配219
13.2.4非确定性220
13.3基于集合的抽象的例子220
13.3.1表示 I220
13.3.2文件系统 I221
13.3.3表示 II222
13.4使用集合进行抽象和建模223
13.4.1网络建模223
扁平网络的叙述：223
扁平网络的形式化224
超网络的叙述224
超网络的形式化224
13.4.2伪层次建模225
单图的叙述225
单图的形式化225
超图的叙述225
超图的形式化225
13.4.3对电话系统的建模227
\CJKfamily kai状态的叙述227
\CJKfamily kai状态的形式化228
\CJKfamily kai有效状态的叙述228
\CJKfamily kai有效状态的形式化228
\CJKfamily kai用户动作的叙述228
动作类型的形式化228
题外话：类型并和变体记录229
叙述： \CJKfamily kai多方呼叫229
\CJKfamily kai多方呼叫的形式化229
叙述： \CJKfamily kai终止呼叫230
\CJKfamily kai终止呼叫的形式化230
叙述： \CJKfamily kai用户忙230
\CJKfamily kai用户忙的形式化231
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\texttt RSL 中的笛卡尔240
14.1笛卡尔：关键问题240
14.2笛卡尔数据类型241
14.2.1笛卡尔类型和笛卡尔表达式241
14.2.2笛卡尔值表达式242
14.2.3笛卡尔操作，I243
14.2.4笛卡尔绑定模式和匹配243
14.2.5笛卡尔操作，II244
14.3笛卡尔抽象的例子244
14.3.1文件系统 II244
14.3.2库拉托夫斯基（Kuratowski）：对和集合245
14.4用笛卡尔进行抽象与建模247
14.4.1句法结构建模247
叙述------句法（笛卡尔）范畴248
题外话------并类型操作符：$|$248
另一段题外话------笛卡尔文本类型248
形式化------句法（笛卡尔）范畴248
形式化------（笛卡尔的）良构性249
一条迂回之路：\texttt RSL“case”结构249
笛卡尔模式250
笛卡尔模式、拟合和绑定250
\hfill \texttt RSL\ \bf case 结构迂回之路的结束251
14.4.2笛卡尔“\bf let ... \bf in ... \bf end”绑定251
14.4.3语义结构建模252
叙述------语义类型252
程序点252
格局252
程序指针堆栈252
形式化------语义类型252
叙述------计算机程序解释253
形式化------语义函数253
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\texttt RSL\ 中的列表262
15.1与列表相关的一些观点262
15.2列表数据类型263
15.2.1列表类型263
15.2.2列表值表达式264
列表的枚举264
列表值操作符/操作数表达式265
操作符基调及其非形式的含义：265
列表操作的操作式及非形式定义：265
列表的内涵266
15.2.3列表的绑定模式与匹配267
15.2.4列表：确定性和非确定性的回顾268
15.3基于列表的抽象的小例子268
15.3.1表示268
15.3.2堆栈和队列269
15.3.3文件系统 III270
15.3.4排序算法272
15.4使用列表进行抽象与建模273
15.4.1使用列表对书进行建模273
实体叙述273
形式化274
操作叙述274
形式化274
15.4.2“上下文中的关键字（KeyWord-In-Context，KWIC）”的建模274
给定的问题：275
非形式问题描述的讨论：275
一些辅助函数：276
模型：277
15.5列表的归纳定义279
15.5.1列表类型的归纳定义279
15.5.2列表值的归纳定义280
15.6列表抽象和模型的回顾281
15.7列表：讨论282
15.8练习282
16\texttt RSL 中的映射286
16.1关键问题286
16.2映射数据类型287
16.2.1映射类型：定义和表达式287
16.2.2映射值表达式288
映射的枚举288
确定的和非确定的映射值288
映射操作符/操作数表达式288
\textup \CJKfamily kai映射操作基调和例子289
\textup \CJKfamily kai映射操作符的含义289
映射的内涵290
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
\textup \CJKfamily kai描述 ------ 类型295
\textup \CJKfamily kai形式化 ------ 类型296
\textup \CJKfamily kai描述 ------ 不变式296
\textup \CJKfamily kai形式化 ------ 不变式296
16.4.3层次结构297
\textup \CJKfamily kai描述 ------ 层次结构297
\textup \CJKfamily kai形式化 ------ 层次结构297
\textup \CJKfamily kai描述 ------ 路径298
\textup \CJKfamily kai形式化 ------ 路径298
\textup \CJKfamily kai描述 ------ 路径操作299
\textup \CJKfamily kai形式化 ------ 路径操作299
16.4.4关系文件系统 (IV) 和数据库300
16.4.5复杂指针数据结构303
讨论312
16.4.6数据结构的良构性312
讨论315
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\texttt RSL\ 中的高阶函数325
17.1函数：关键问题325
17.2使用基于函数的抽象的例子326
17.2.1泛函326
17.2.2讨论327
17.3用函数进行抽象与建模327
17.3.1函数作为概念327
句法类型327
语义类型：328
语义确立函数328
高阶函数作为指称329
17.3.2操作符提升330
操作符提升的例子330
描述与分析：类型331
形式化：类型332
描述：操作333
讨论335
描述：提升的函数335
形式化：提升的函数336
17.4函数的归纳定义336
17.4.1函数类型的归纳定义336
17.4.2函数值的归纳定义337
17.5函数抽象与建模的回顾337
17.6讨论338
17.7练习338
\contentsline part\ IV\hskip \betweenumberspace 规约类型339
规约类型339
18\texttt 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
非递归记录类型的定义345
递归记录类型的定义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
\contentsline part\ V\hskip \betweenumberspace 规约程序设计353
规约程序设计353
\vspace *2mm
关于规约程序设计353
关于问题与练习354
19应用式规约程序设计355
19.1作用域与绑定355
19.1.1绑定模式 ------ 非形式说明356
19.1.2“let” 结构的作用域和绑定 [1\hbox ]357
19.1.3函数定义作用域与绑定[2\hbox ]358
19.1.4“case”结构的作用域和绑定[3\hbox ]358
19.1.5内涵：作用域和绑定[4\hbox ]359
19.1.6量化：作用域和绑定 [5\hbox ] 360
19.2直观理解360
19.2.1简单“let \textrm a = $\mathcal E_d$ in $\mathcal E_b$\textrm (a) end”360
19.2.2递归“let\ \textrm f(a) = $\mathcal E_d$\textrm (f) in\ $\mathcal E_b$\textrm (f,a) end”360
19.2.3直谓 “let\ \textrm a:A $\bullet \ \mathcal P$\textrm (a) in\ $\mathcal E$\textrm (a) end”361
19.2.4多个 ``let\ \textrm a$_i$ = $\mathcal E_d_i$ in\ $\mathcal E_b$\textrm (a$_i$) end''361
19.2.5文字和标识符362
文字362
标识符362
19.3操作符/操作数表达式362
19.4枚举和内涵表达式363
19.5条件表达式363
19.6绑定、确定类型、模式和匹配365
19.6.1问题365
句法便利问题365
19.6.2绑定和模式的本质366
绑定366
模式366
绑定和模式：明显的不同366
绑定和确定类型367
19.6.3绑定模式367
较早内容回顾367
记录绑定模式368
绑定模式的一般形式369
\rm 注释371
\rm 进一步的介绍371
19.6.4给定类型371
19.6.5选择模式和绑定372
注释373
一些观察377
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
直观理解394
位置和值的类型395
存储不变式395
语义操作396
句法形式396
语义397
20.3.3讨论：先语义，后句法398
20.3.4讨论：类型同态398
20.3.5状态的概念398
20.4函数定义和表达式399
20.4.1\bf Unit 类型表达式， I399
20.4.2命令式函数399
20.4.3读/写访问描述400
20.4.4局部变量400
20.4.5\bf Unit 类型表达式， II400
20.4.6纯表达式401
20.4.7只读表达式401
状态量化 ($\Box $)402
20.4.8等价 ($\equiv $) 和相等 (=)402
等价 （$\equiv $）402
条件等价403
相等 （=）403
20.5转化：应用式到命令式403
20.5.1应用式到命令式的转化403
20.5.2递归到迭代的转化404
20.5.3应用式到命令式的模式405
模式406
20.5.4正确性、原则、技术、工具412
20.6配置建模的风格412
20.6.1应用式上下文和状态412
句法和语义类型412
\textup \CJKfamily kai句法类型413
\textup \CJKfamily kai语义类型：413
辅助函数413
简单解释函数414
复合解释函数414
上下文创建解释函数414
总结、应用式上下文和状态415
20.6.2应用式上下文和命令式状态416
元状态和辅助函数416
简单解释函数416
复合解释函数417
上下文创建解释函数417
总结、应用式上下文和命令式状态418
20.6.3命令式上下文和状态418
元状态418
辅助函数419
简单解释函数419
复合解释函数419
上下文创建解释函数420
总结、命令式上下文和状态420
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$\lambda $ 演算的类型理论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
模式的“会合”规约1--2--3430
模式的“会合”规约 4431
21.2.2图和记法总结431
21.2.3关于迹语义432
21.2.4一些描述：进程，等等433
21.2.5进程建模原则434
构件 $\equiv $进程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
\bf stop：基本进程444
前缀444
定义444
$\unhbox \voidb@x \hbox $\delimiter "4264306 \tmspace -\thinmuskip .1667em\delimiter "5265307 \tmspace -\thinmuskip .1667em\tmspace -\thinmuskip .1667em\tmspace -\thinmuskip .1667em\tmspace -\thinmuskip .1667em\tmspace -\thinmuskip .1667em\tmspace -\thinmuskip .1667em\tmspace +\thickmuskip .2777em\delimiter "4262304 \tmspace -\thinmuskip .1667em\delimiter "5263305 $$： 外部非确定性选择444
$\unhbox \voidb@x \hbox $\delimiter "4264306 \tmspace -\thinmuskip .1667em\delimiter "5265307 $$：内部非确定性选择444
CSP 定律 （I）445
复合事件445
输入和输出445
\unhbox \voidb@x \hbox $\parallel $：并行组合446
共享事件446
CSP 定律（II）446
21.3.3讨论447
21.4\texttt RSL/CSP 进程组合子447
21.4.1类 \texttt RSL 通道447
21.4.2\texttt RSL 通信子句448
简单输入/输入出子句448
21.4.3\texttt RSL 进程448
简单进程定义448
进程及其定义449
进程调用449
数组通道进程定义450
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阶段 I：应用式模式453
21.5.2阶段 II：简单重构453
21.5.3阶段 III：引入并行453
21.5.4阶段IV：简单重构454
21.5.5阶段关系455
21.5.6阶段 V：命令式重构455
21.5.7一些评论456
21.6并行和并发：讨论456
21.6.1\texttt CSP 和 \texttt RSL/CSP456
21.6.2建模技巧456
21.7文献评注457
21.8练习457
其他463
其他463
22其他465
22.1我们讨论了什么465
22.2下一个讨论什么465
22.3下一个的下一个讨论什么465
22.4提示466
22.5 \CJKfamily kai“轻量级”形式方法467
22.6文献评注467
\contentsline part\ VII\hskip \betweenumberspace 附录469
附录469
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
\contentsline chapter参考文献545
