简-埃蒙德·阿布瑞尔（Jean-Raymond Abrial） 法国计算机科学家，国际知名的形式化方法和软件工程专家，欧洲科学院院士。20世纪80年代，他先后开发了著名的Z语言和B方法。2000年以后，他开发了Event-B方法，并领导一个国际团队，在欧盟项目支持下，为Event-B开发了公开免费的Rodin平台。这些语言和方法被国际形式化方法领域广泛接受和使用，并被开发工作者应用于软件和其他系统的实际开发工作。阿布瑞尔教授长期致力于推动和参与形式化方法的工业应用，指导了B方法在轨道交通领域的*早开发工作，在相关领域做出了卓越的贡献。阿布瑞尔教授与国内一些高校和研究单位有长期而密切的合作关系，并于2016年获得了中华人民共和国国务院颁发的“中华人民
共和国国际科学技术合作奖”。

这本实用的教科书适用于形式化方法的入门课程或高级课程。本书以B形式化方法的一个扩展Event-B作为工具，展示了一种完成系统建模和设计的数学方法。
简-埃蒙德·阿布瑞尔（Jean-Raymond Abrial）是国际著名计算机科学家，曾任苏黎世联邦理工学院客座教授，他基于精化的思想提出了一种系统化的方法，教读者如何逐步构造出所期望的模型，并通过严格的证明完成对所构造模型做系统化的推理。本书将介绍如何根据实际需要去构造各种程序，以及如何更为普遍地构造各种离散系统的模型。本书提供了大量的示例，这些示例源自计算机系统开发的各个领域，包括顺序程序、并发程序和电子线路等。
本书还包含了大量具有不同难度的练习和开发项目。书中的每个例子都用Rodin平台工具集证明过。
本书适合作为高等院校计算机、软件工程、网络工程、信息安全等专业高年级本科生、研究生的教材，也可供相关领域的研究人员和技术人员参考。

第 1章　引言 1
1．1　动机 1
1．2　各章概览 2
1．3　如何用这本书 6
1．4　形式化方法 8
1．5　一个小迂回：蓝图 9
1．6　需求文档 10
1．6．1　生命周期 10
1．6．2　需求文档的困难 10
1．6．3　一种有用的比较 11
1．7　本书中使用的“形式化方法”的定义 12
1．7．1　复杂系统 12
1．7．2　离散系统 13
1．7．3　测试推理与模型（蓝图）推理 13
1．8　有关离散模型的非形式化概览 14
1．8．1　状态和迁移 14
1．8．2　操作性解释 14
1．8．3　形式化推理 15
1．8．4　管理闭模型的复杂性 15
1．8．5　精化 15
1．8．6　分解 16
1．8．7　泛型开发 16
1．9 参考资料 17
第 2章　控制桥上的汽车 18
2．1　引言 18
2．2　需求文档 18
2．3　精化策略 20
2．4　初始模型：限制汽车的数量 20
2．4．1　引言 20
2．4．2　状态的形式化 21
2．4．3　事件的形式化 22
2．4．4　前-后谓词 23
2．4．5　证明不变式的保持性质 23
2．4．6　相继式 25
2．4．7　应用不变式保持性的规则 25
2．4．8　证明义务的证明 26
2．4．9　推理规则 27
2．4．10　元变量 29
2．4．11　证明 29
2．4．12　更多推理规则 30
2．4．13　改造两个事件：引进卫 31
2．4．14　改造的不变式保持规则 31
2．4．15　重新证明不变式的保持性 32
2．4．16　初始化 33
2．4．17　初始化事件init的不变式建立规则 33
2．4．18　应用不变式建立规则 34
2．4．19　证明初始化的证明义务：更多推理规则 34
2．4．20　无死锁 35
2．4．21　无死锁规则 35
2．4．22　应用无死锁证明义务规则 35
2．4．23　更多推理规则 36
2．4．24　证明无死锁的证明义务 37
2．4．25　对初始模型的总结 38
2．5　第 一次精化：引入单行桥 38
2．5．1　引言 38
2．5．2　状态的精化 39
2．5．3　精化抽象事件 40
2．5．4　重温前-后谓词 40
2．5．5　精化的非形式化证明 41
2．5．6　证明抽象事件的正确精化 42
2．5．7　应用精化规则 43
2．5．8　精化初始化事件init 45
2．5．9　初始化事件init精化正确性的证明义务规则 46
2．5．10　应用初始化精化的证明义务规则 46
2．5．11　引入新事件 46
2．5．12　空动作skip 47
2．5．13　证明两个新事件的正确性 47
2．5．14　证明新事件的收敛性 49
2．5．15　应用非收敛证明义务规则 50
2．5．16　相对无死锁 51
2．5．17　应用相对无死锁证明义务规则 51
2．5．18　更多推理规则 52
2．5．19　第 一个精化的总结 54
2．6　第二次精化：引入交通灯 55
2．6．1　精化状态 55
2．6．2　精化抽象事件 56
2．6．3　引进新事件 56
2．6．4　叠加：调整精化规则 57
2．6．5　证明事件的正确性 58
2．6．6　更多逻辑推理规则 58
2．6．7　试探性的证明和解 58
2．6．8　新事件的收敛性 64
2．6．9　相对无死锁 67
2．6．10　第二个精化的总结 68
2．7　第三次精化：引入车辆传感器 70
2．7．1　引言 70
2．7．2　精化状态 72
2．7．3　精化控制器里的抽象事件 75
2．7．4　在环境里增加新事件 77
2．7．5　新事件的收敛性 78
2．7．6　无死锁 78
第3章　冲压机控制器 79
3．1　非形式描述 79
3．1．1　基本设备 79
3．1．2　基本命令和按钮 80
3．1．3　基本用户动作 80
3．1．4　用户工作期 80
3．1．5　危险：控制器的必要性 80
3．1．6　安全门 81
3．2　设计模式 81
3．2．1　动作和反应 82
3．2．2　第 一种情况：一个简单的动作反应模式，无反作用 83
3．2．3　第二种情况：一个简单的动作模式，一次重复动作和反应 86
3．3　冲压机的需求 90
3．4　精化策略 91
3．5　初始模型：连接控制器和电动机 92
3．5．1　引言 92
3．5．2　建模 92
3．5．3　事件的总结 94
3．6　第 一次精化：把电动机按钮连接到控制器 94
3．6．1　引言 94
3．6．2　建模 95
3．6．3　加入“假”事件 99
3．6．4　事件的总结 100
3．7　第二次精化：连接控制器到离合器 100
3．8　另一个设计模式：两个强反应的弱同步 101
3．8．1　引言 101
3．8．2　建模 103
3．9　第三次精化：约束离合器和电动机 108
3．10　第四次精化：连接控制器到安全门 110
3．10．1　拷贝 110
3．10．2　事件的总结 110
3．11　第五次精化：约束离合器和安全门 110
3．12　另一设计模式：两个强反应的强同步 111
3．12．1　引言 111
3．12．2　建模 112
3．13　第六次精化：离合器和安全门之间的更多约束 117
3．14　第七次精化：把控制器连接到离合器按钮 118
3．14．1　拷贝 118
3．14．2　事件的总结 118
第4章　简单文件传输协议 120
4．1　需求 120
4．2　精化策略 120
4．3　协议的初始模型 121
4．3．1　状态 122
4．3．2　一些数学表示法 122
4．3．3　事件 125
4．3．4　证明 125
4．4　协议的第 一次精化 127
4．4．1　非形式化的说明 127
4．4．2　状态 128
4．4．3　更多数学符号 128
4．4．4　事件 130
4．4．5　精化证明 131
4．4．6　事件receive的收敛性证明 134
4．4．7　相对无死锁证明 135
4．5　协议的第二次精化 135
4．5．1　状态和事件 135
4．5．2　证明 137
4．6　协议的第三次精化 137
4．6．1　状态 137
4．6．2　事件 138
4．6．3　全称量化谓词的推理规则 138
4．7　对开发的回顾 139
4．7．1　动机和预期事件的引入 139
4．7．2　初始模型 140
4．7．3　第 一次精化 140
4．7．4　第二次精化 141
4．7．5　第三次精化 141
4．8　参考资料 142
第5章　Event-B建模语言和证明义务规则 143
5．1　Event-B表示法 143
5．1．1　引言：机器和上下文 143
5．1．2　机器和上下文的关系 143
5．1．3　上下文的结构 144
5．1．4　上下文的例子 145
5．1．5　机器的结构 145
5．1．6　机器的例子 146
5．1．7　事件 147
5．1．8　动作 147
5．1．9　事件的例子 149
5．2　证明义务规则 150
5．2．1　引言 150
5．2．2　不变式保持证明义务规则：INV 151
5．2．3　可行性证明义务规则：FIS 153
5．2．4　卫加强证明义务规则：GRD 153
5．2．5　卫归并证明义务规则：MRG 154
5．2．6　模拟证明义务规则：SIM 155
5．2．7　数值变动式证明义务规则：NAT 158
5．2．8　有穷集变动式证明义务规则：FIN 158
5．2．9　变动量证明义务规则：VAR 159
5．2．10　非确定性见证证明义务规则：WFIS 161
5．2．11　定理证明义务规则：THM 162
5．2．12　良好定义证明义务规则：WD 162
第6章　有界重传协议 163
6．1　有界重传协议的非形式说明 163
6．1．1　正常行为 163
6．1．2　不可靠的通信 163
6．1．3　协议流产 164
6．1．4　交替位 164
6．1．5　协议的最后情况 164
6．1．6　BRP的伪代码描述 165
6．1．7　有关伪代码的说明 167
6．2　需求文档 167
6．3　精化策略 168
6．4　初始模型 169
6．4．1　状态 169
6．4．2　事件 169
6．5　第 一次和第二次精化 170
6．5．1　状态 170
6．5．2　第 一次精化的事件 170
6．5．3　第二次精化的事件 171
6．6　第三次精化 171
6．6．1　状态 172
6．6．2　事件 172
6．6．3　事件之间的同步 173
6．7　第四次精化 173
6．7．1　状态 173
6．7．2　事件 174
6．7．3　事件的同步 175
6．8　第五次精化 176
6．8．1　状态 176
6．8．2　事件 177
6．8．3　事件的同步 180
6．9　第六次精化 181
6．10　参考资料 181
第7章　一个并发程序的开发1 182
7．1　分布式和并发程序的比较 182
7．1．1　分布式程序 182
7．1．2　并发程序 182
7．2　提出的实例 183
7．2．1　非形式的说明 183
7．2．2　非并发的场景展示 185
7．2．3　定义原子性 186
7．3　交错 187
7．3．1　问题 187
7．3．2　计算不同交错的数目 188
7．3．3　结果 189
7．4　并发程序的规范描述 190
7．4．1　写和读的轨迹 190
7．4．2　轨迹之间的关系 190
7．4．3　不变式的总结 193
7．4．4　事件 193
7．5　精化策略 194
7．5．1　最终精化的梗概 194
7．5．2　精化的目标 196
7．6　第 一次精化 196
7．6．1　读者状态 196
7．6．2　读事件 197
7．6．3　写者状态 198
7．6．4　写事件 198
7．7　第二次精化 200
7．7．1　状态 200
7．7．2　事件和新增的不变式 200
7．8　第三次精化 203
7．8．1　状态 203
7．8．2　事件 203
7．9　第四次精化 204
7．9．1　状态 204
7．9．2　事件 205
7．10　参考资料 206
第8章　电路的开发 207
8．1　引言 207
8．1．1　同步电路 207
8．1．2　电路与其环境的耦合 208
8．1．3　耦合的动态观点 208
8．1．4　耦合的静态观点 209
8．1．5　协调性条件 209
8．1．6　一个警告 210
8．1．7　电路的最终构造 210
8．1．8　一个非常小的示例 213
8．2　第 一个例子 214
8．2．1　非形式的规范描述 214
8．2．2　初始模型 215
8．2．3　精化电路以减少其非确定性 218
8．2．4　通过改变数据空间来精化电路 220
8．2．5　构造最后的电路 222
8．3　第二个例子：仲裁器 225
8．3．1　非形式的规范描述 225
8．3．2　初始模型 226
8．3．3　第 一次精化：让电路生成二进制输出 229
8．3．4　第二次精化 231
8．3．5　第三次精化：消除电路的非确定性 233
8．3．6　第四次精化：构造最后的电路 234
8．4　第三个例子：一种特殊的道路交通灯 234
8．4．1　非形式的规范描述 235
8．4．2　关注点分离的方法 235
8．4．3　优先权电路：初始模型 236
8．4．4　最后的Priority电路 238
8．5　Light电路 240
8．5．1　一个抽象：Upper电路 241
8．5．2　精化：加入Lower电路 242
8．6　参考资料 245
第9章　数学语言 246
9．1　相继式演算 246
9．1．1　定义 246
9．1．2　一个数学语言的相继式 248
9．1．3　初始理论 248
9．2　命题语言 249
9．2．1　语法 249
9．2．2　初始理论的扩充 250
9．2．3　派生规则 250
9．2．4　方法论 252
9．2．5　命题语言的扩充 252
9．3　谓词语言 253
9．3．1　语法 253
9．3．2　谓词和表达式 254
9．3．3　全称量词的推理规则 254
9．4　相等谓词 256
9．5　集合论语言 257
9．5．1　语法 258
9．5．2　集合论公理 258
9．5．3　基本集合运算符 259
9．5．4　基本集合运算符的推广 260
9．5．5　二元关系运算符 261
9．5．6　函数运算符 264
9．5．7　各种箭头的总结 265
9．5．8　lambda抽象和函数调用 265
9．6　布尔和算术语言 266
9．6．1　语法 266
9．6．2　皮阿诺公理和递归定义 267
9．6．3　算术语言的扩充 267
9．7　高级数据结构 269
9．7．1　反自反的传递闭包 269
9．7．2　强连通图 270
9．7．3　无穷表 271
9．7．4　有穷表 274
9．7．5　环 276
9．7．6　无穷树 277
9．7．7　有穷深度树 280
9．7．8　自由树 281
9．7．9　良定义条件和有向无环图 283
第 10章　环形网络上选领导 284
10．1　需求文档 284
10．2　初始模型 286
10．3　讨论 286
10．3．1　第 一个尝试 286
10．3．2　第二个尝试 287
10．3．3　第三个尝试 287
10．3．4　解的非形式化展示 287
10．4　第 一次精化 288
10．4．1　状态：环的形式化 288
10．4．2　状态：变量 289
10．4．3　事件 289
10．5　证明 289
10．5．1　事件elect的证明 290
10．5．2　事件accept的证明 291
10．5．3　事件reject的证明 293
10．5．4　新事件不发散的证明 293
10．5．5　无死锁的证明 293
10．6　参考资料 294
第 11章　树形网络上的同步 295
11．1　引言 295
11．2　初始模型 296
11．2．1　状态 296
11．2．2　事件 297
11．2．3　证明 297
11．3　第 一次精化 298
11．3．1　状态 298
11．3．2　事件 300
11．3．3　证明 300
11．4　第二次精化 301
11．5　第三次精化 303
11．5．1　事件ascending的精化 303
11．5．2　事件descending的精化 304
11．5．3　证明定理thm3_4 306
11．5．4　证明不变式inv3_3的保持性 306
11．6　第四次精化 308
11．7　参考资料 310
第 12章　移动代理的路由算法 311
12．1　问题的非形式化描述 311
12．1．1　抽象的非形式化描述 311
12．1．2　第 一个非形式化的精化 312
12．1．3　第二个非形式化的精化 312
12．1．4　第三个非形式化的精化：解 314
12．2　初始模型 315
12．2．1　状态 315
12．2．2　事件 316
12．2．3　证明 317
12．3　第 一次精化 318
12．3．1　状态 318
12．3．2　事件 319
12．3．3　证明 320
12．4　第二次精化 320
12．4．1　状态 320
12．4．2　事件 322
12．4．3　证明 323
12．5　第三次精化：数据精化 324
12．5．1　状态 324
12．5．2　事件 324
12．5．3　证明 325
12．6　第四次精化 325
12．7　参考资料 325
第 13章　在连通图网络上选领导 326
13．1　初始模型 326
13．1．1　状态 326
13．1．2　事件 327
13．2　第 一次精化 327
13．2．1　定义自由树 327
13．2．2　扩充状态 327
13．2．3　事件的第 一次精化 328
13．2．4　第 一次精化的证明 329
13．3　第二次精化 329
13．3．1　第二次精化的状态 329
13．3．2　事件 329
13．3．3　证明 330
13．4　第三次精化：竞争问题 330
13．4．1　引言 330
13．4．2　处理竞争的状态 331
13．4．3　处理竞争的事件 332
13．5　第四次精化：简化 332
13．6　第五次精化：引入基数 333
第 14章　证明义务的数学模型 335
14．1　引言 335
14．2　不变式保持性的证明义务规则 335
14．3　观察离散迁移系统的演化：迹 337
14．3．1　第 一个例子 338
14．3．2　迹 338
14．3．3　迹的特征 339
14．3．4　演化图 339
14．3．5　数学表示 339
14．4　用迹表示简单精化 340
14．4．1　第二个例子 340
14．4．2　比较这两个例子 341
14．4．3　简单精化：非形式化的方法 342
14．4．4　简单精化：形式化定义 342
14．4．5　考虑个别的事件 343
14．4．6　外部变量和内部变量 344
14．4．7　外部集合 345
14．5　广义精化的集合论表示 345
14．5．1　引言 346
14．5．2　精化的形式化定义 347
14．5．3　精化的充分条件：前向模拟 347
14．5．4　精化的另一充分条件：反向模拟 352
14．5．5　迹的精化 352
14．6　打破抽象和具体事件之间的一对一关系 353
14．6．1　分裂抽象事件 353
14．6．2　合并几个抽象事件 353
14．6．3　引进新事件 354
第 15章　顺序程序的开发 357
15．1　开发顺序程序的一种系统化方法 357
15．1．1　顺序程序的组成部分 357
15．1．2　把顺序程序分解为独立的事件 358
15．1．3　方法梗概 359
15．1．4　顺序程序的规范：前条件和后条件 359
15．2　一个非常简单的例子 360
15．2．1　规范 360
15．2．2　精化 361
15．2．3　推广 362
15．3　合并规则 362
15．4　例：排序数组里的二分检索 363
15．4．1　初始模型 363
15．4．2　第 一次精化 364
15．4．3　第二次精化 365
15．4．4　合并 366
15．5　例：自然数数组中的最小值 366
15．5．1　初始模型 366
15．5．2　第 一次精化 367
15．6　例：数组划分 367
15．6．1　初始模型 367
15．6．2　第 一次精化 368
15．6．3　合并 370
15．7　例：简单排序 370
15．7．1　初始模型 370
15．7．2　第 一次精化 371
15．7．3　第二次精化 371
15．7．4　合并 373
15．8　例：数组反转 373
15．8．1　初始模型 373
15．8．2　第 一次精化 374
15．9　例：链接表反转 375
15．9．1　初始模型 375
15．9．2　第 一次精化 376
15．9．3　第二次精化 377
15．9．4　第三次精化 378
15．9．5　合并 378
15．10　例：计算平方根的简单数值程序 378
15．10．1　初始模型 379
15．10．2　第 一次精化 379
15．10．3　第二次精化 379
15．11　例：内射数值函数的逆 380
15．11．1　初始模型 380
15．11．2　第 一次精化 381
15．11．3　第二次精化 382
15．11．4　实例化 383
15．11．5　第 一次实例化 383
15．11．6　第二次实例化 384
第 16章　位置访问控制器 385
16．1　需求文档 385
16．2　讨论 387
16．2．1　控制的共享 387
16．2．2　闭模型的构造 387
16．2．3　设备的行为 388
16．2．4　处理安全问题 388
16．2．5　同步问题 388
16．2．6　边界的功能 388
16．3　系统的初始模型 389
16．4　第 一次精化 390
16．4．1　状态和事件 390
16．4．2　无死锁 391
16．4．3　第 一个解 392
16．4．4　第二个解 393
16．4．5　无死锁的修正 393
16．5　第二次精化 394
16．5．1　状态和事件 394
16．5．2　同步 396
16．5．3　证明 396
16．5．4　读卡器持续阻塞的危险 396
16．5．5　避免持续阻塞的提议 396
16．5．6　最后的决定 397
16．6　第三次精化 397
16．6．1　引进读卡器 397
16．6．2　与通信网络有关的假设 398
16．6．3　变量和不变式 398
16．6．4　事件 399
16．6．5　同步 400
16．6．6　证明 400
16．7　第四次精化 400
16．7．1　与物理门有关的决策 400
16．7．2　变量和不变式：绿色链 401
16．7．3　变量和不变式：红色链 401
16．7．4　事件 402
16．7．5　同步 404
第 17章　列车系统 406
17．1　非形式的引言 406
17．1．1　非形式描述的方法论约定 407
17．1．2　行车调度员控制下的轨道网络 407
17．1．3　网络的特殊组件：道岔和交叉点 407
17．1．4　阻塞的概念 409
17．1．5　通路的概念 409
17．1．6　信号的概念 411
17．1．7　通路和阻塞保持 412
17．1．8　安全性条件 414
17．1．9　运行条件 415
17．1．10　列车的假设 415
17．1．11　事故 416
17．1．12　实例 417
17．2　精化策略 420
17．3　初始模型 420
17．3．1　状态 420
17．3．2　事件 425
17．4　第 一次精化 427
17．4．1　状态 427
17．4．2　事件 429
17．5　第二次精化 431
17．5．1　状态 432
17．5．2　事件 432
17．6　第三次精化 433
17．6．1　状态 433
17．6．2　事件 433
17．7　第四次精化 434
17．8　总结 436
17．9　参考资料 437
第 18章　一些问题 438
18．1　练习 438
18．1．1　银行 438
18．1．2　生日记录册 438
18．1．3　有一行为0的数值矩阵 439
18．1．4　有序矩阵检索 439
18．1．5　名人问题 439
18．1．6　在两个有交集的有穷数值集合里找公共元素 440
18．1．7　简单的访问控制系统 441
18．1．8　简单的图书馆 441
18．1．9　简单的电路 441
18．1．10　闹钟 442
18．1．11　连续信号的分析 442
18．2　项目 443
18．2．1　旅馆的电子钥匙系统 443
18．2．2　Earley分析器 444
18．2．3　Schorr-Wait算法 446
18．2．4　线性表封装 447
18．2．5　队列的并发访问 447
18．2．6　几乎线性的排序 448
18．2．7　终止性检查 449
18．2．8　分布式互斥 449
18．2．9　电梯 452
18．2．10　业务交易协议 453
18．3　数学的开发 454
18．3．1　良构集合和关系 454
18．3．2　不动点 456
18．3．3　递归 457
18．3．4　传递闭包 457
18．3．5　过滤器和超过滤器 458
18．3．6　拓扑 458
18．3．7　Cantor-Bernstein定理 460
18．3．8　Zermelo定理 460
18．4　参考资料 462