Event-B建模系统和软件工程

Event-B建模系统和软件工程
分享
扫描下方二维码分享到微信
打开微信,点击右上角”+“,
使用”扫一扫“即可将网页分享到朋友圈。
作者: [法] (Jean-Raymond Abrial) ,
2019-09
版次: 1
ISBN: 9787115508997
定价: 129.00
装帧: 平装
开本: 16开
纸张: 胶版纸
页数: 462页
  • 这本实用的教科书适用于形式化方法的入门课程或高级课程。本书以B形式化方法的一个扩展Event-B作为工具,展示了一种完成系统建模和设计的数学方法。

    简-埃蒙德·阿布瑞尔(Jean-Raymond Abrial)是国际著名计算机科学家,曾任苏黎世联邦理工学院客座教授,他基于精化的思想提出了一种系统化的方法,教读者如何逐步构造出所期望的模型,并通过严格的证明完成对所构造模型做系统化的推理。本书将介绍如何根据实际需要去构造各种程序,以及如何更为普遍地构造各种离散系统的模型。本书提供了大量的示例,这些示例源自计算机系统开发的各个领域,包括顺序程序、并发程序和电子线路等。

    本书还包含了大量具有不同难度的练习和开发项目。书中的每个例子都用Rodin平台工具集证明过。

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

    共和国国际科学技术合作奖”。 第 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
  • 内容简介:
    这本实用的教科书适用于形式化方法的入门课程或高级课程。本书以B形式化方法的一个扩展Event-B作为工具,展示了一种完成系统建模和设计的数学方法。

    简-埃蒙德·阿布瑞尔(Jean-Raymond Abrial)是国际著名计算机科学家,曾任苏黎世联邦理工学院客座教授,他基于精化的思想提出了一种系统化的方法,教读者如何逐步构造出所期望的模型,并通过严格的证明完成对所构造模型做系统化的推理。本书将介绍如何根据实际需要去构造各种程序,以及如何更为普遍地构造各种离散系统的模型。本书提供了大量的示例,这些示例源自计算机系统开发的各个领域,包括顺序程序、并发程序和电子线路等。

    本书还包含了大量具有不同难度的练习和开发项目。书中的每个例子都用Rodin平台工具集证明过。

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

    共和国国际科学技术合作奖”。
  • 目录:
    第 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
查看详情
12
您可能感兴趣 / 更多
Event-B建模系统和软件工程
财务报告与分析:一种国际化视角
[法]丁远、[法]埃韦尔·施托洛韦、[法]卢克·伯格姆 著
Event-B建模系统和软件工程
解码世界文化中国历史古代史文化世界简史通史历史知识读物书教科书籍史纲媲美DK畅销书
[法]伊莎贝尔·富热尔 著
Event-B建模系统和软件工程
名人传(初中传记阅读指导版!人物传记学得好,就读这本名人传!诺奖大师作品!附赠中考学习手册独立注释册)(三个圈经典文库)
[法]罗曼·罗兰 著;傅雷 译;读客文化 出品
Event-B建模系统和软件工程
苦炼
[法]玛格丽特·尤瑟纳尔
Event-B建模系统和软件工程
莎士比亚传 英文版原版 [法]维克多·雨果 著 经典英语文库入选书目 世界经典文学名著 英语原版无删减 提高英文阅读与写作能力
[法]维克多·雨果 著
Event-B建模系统和软件工程
左拉传
[法]亨利·特罗亚 著;柳鸣九 编;胡尧步 译
Event-B建模系统和软件工程
幽灵王子的诅咒
[法]伊莎贝尔·德唐 著
Event-B建模系统和软件工程
梅洛-庞蒂文集 (第3卷):人道主义与恐怖
[法]梅洛-庞蒂 著;郑琪 译
Event-B建模系统和软件工程
传奇发明史:从火的使用到长生不死(三棱镜译丛)
[法]德尼·古特莱本
Event-B建模系统和软件工程
花点时间好奇一下世界运作的秘密
[法]布鲁斯·贝纳姆兰(Bruce Benamran) 著;章俪萦、李博、韩斌、林达 译
Event-B建模系统和软件工程
全译本列那狐的故事插图版久读不衰的世界经典名著,名家译本可读性更高中少明天书系
[法]玛特·艾·季罗夫人 著;罗新璋 译
Event-B建模系统和软件工程
海底两万里(附名著导读无障碍阅读精编版)/快乐读书汇丛书
[法]儒勒·凡尔纳 著;李亚 译