B方法PDF电子书下载

第一部分 数学 1

第1章 数学推理 1

1.1 形式推理 1

1.1.1 相继式和谓词 1

1.1.2 推理规则 2

1.1.3 证明 3

1.1.4 基本规则 3

1.2 命题演算 5

1.2.1 基本断言的记法形式 5

1.2.2 命题逻辑的推理规则 6

1.2.3 一些证明 8

1.2.4 一个证明过程 14

1.2.5 扩充记法形式 16

1.2.6 一些经典结果 18

1.3 谓词演算 18

1.3.1 量化谓词和代换的记法形式 18

1.3.2 全称量化公式 20

1.3.3 非自由性 20

1.3.4 代换 21

1.3.5 谓词演算的推理规则 23

1.3.6 若干证明 23

1.3.7 扩充的证明过程 24

1.3.8 存在量化公式 25

1.3.9 一些经典结果 26

1.4 等式 27

1.5 有序对 30

1.6 练习 33

第2章 集合形式 35

2.1 基本集合结构 36

2.1.1 语法 36

2.1.2 公理 38

2.1.3 性质 39

2.2 类型检查 41

2.3 派生结构 46

2.3.1 定义 46

2.3.2 实例 46

2.3.3 类型检查 47

2.3.4 性质 48

2.4 二元关系 49

2.4.1 二元关系结构：第一组 49

2.4.2 二元关系结构：第二组 51

2.4.3 二元关系结构的实例 52

2.4.4 二元关系结构的类型检查 53

2.5 函数 54

2.5.1 函数构造：第一组 55

2.5.2 函数构造：第二组 57

2.5.3 函数构造的示例 57

2.5.4 函数求值的性质 58

2.5.5 函数构造的类型检查 60

2.6 分类的性质 60

2.6.1 有关成员关系的法则 61

2.6.2 单调性法则 62

2.6.3 包含法则 63

2.6.4 相等法则 64

2.7 例子 77

2.8 练习 81

参考文献 82

第3章 数学对象 83

3.1 广义的交和并 83

3.2 构造数学对象 88

3.2.1 非形式的引言 88

3.2.2 不动点 88

3.2.3 归纳原理 92

3.3 一个集合的有穷子集的集合 96

3.4 有穷集合和无穷集合 98

3.5.1 定义 99

3.5 自然数 99

3.5.2 皮阿诺“公理” 101

3.5.3 最小值 105

3.5.4 强归纳原理 108

3.5.5 最大值 109

3.5.6 自然数上的递归函数 109

3.5.7 算术 111

3.5.8 关系的迭代 115

3.5.9 有穷集的势 115

3.5.10 关系的传递闭包 116

3.6 整数 117

3.7 有穷序列 119

3.7.1 归纳构造 119

3.7.2 直接构造 121

3.7.3 序列上的运算 121

3.7.4 排序及相关问题 125

3.7.5 整数序列的字典序 129

3.8 有穷树 129

3.8.1 非形式的介绍 129

3.8.2 形式化构造 130

3.8.3 归纳 132

3.8.4 递归 134

3.8.5 运算 136

3.8.6 树的表达 137

3.9 标记树 140

3.9.1 直接定义 140

3.9.2 归纳定义 140

3.9.3 归纳 142

3.9.4 递归 142

3.9.5 递归定义的运算 143

3.10 二叉树 144

3.10.1 直接的运算 144

3.9.6 直接定义的运算 144

3.10.2 归纳 145

3.10.3 递归 145

3.10.4 递归定义的运算 145

3.11 良构关系 146

3.11.1 定义 147

3.11.2 在良构集上通过归纳进行证明 147

3.11.3 在良构集上的递归 148

3.11.4 良构性的证明 151

3.11.5 一个良构关系实例 152

3.11.6 非经典递归的其他实例 152

3.12 练习 153

第二部分 抽象机 156

第4章 抽象机引论 156

4.1 抽象机 157

4.2 静态行为——描述状态 157

4.3 动态行为——描述操作 158

4.4 将前－后谓词作为规范 159

4.5 证明义务 159

4.6 代换作为规范 160

4.7 前条件代换（终止性） 161

4.8 参数化和初始化 162

4.9 带有输入参数的操作 164

4.10 带有输出参数的操作 165

4.11 规范的宽松风格和防御风格 165

4.12 多重简单代换 167

4.13 条件代换 168

4.14 约束选择代换 168

4.15 卫式代换（可行性） 169

4.16 没有任何作用的代换 170

4.17 上下文信息——集合和常量 170

4.18 无约束选择代换 173

4.19 显式定义 176

4.20 断言 179

4.21 具体变量和抽象常量 180

4.22 练习 181

参考文献 182

第5章 抽象机的定义 183

5.1 广义代换 183

5.1.1 语法 183

5.1.2 类型检查 186

5.1.3 公理 187

5.2 抽象机 188

5.2.1 语法 188

5.2.3 类型检查 189

5.2.2 可见性规则 189

5.2.4 关于常量 191

5.2.5 证明义务 192

5.2.6 关于给定集合和预定义常量 193

参考文献 194

第6章 抽象机理论 195

6.1 规范型 195

6.2 两个有用的性质 198

6.3 终止性、可行性和前－后谓词 199

6.3.1 终止性 199

6.3.2 可行性 201

6.3.3 前－后谓词 202

6.4 集合论模型 204

6.4.1 第一个模型——一个集合和一个关系 204

6.4.2 第二个模型——集合变换器 206

6.4.3 各种结构的集合论解释 209

6.5 练习 210

第7章 大型抽象机 212

7.1 多重广义代换 212

7.1.1 定义 212

7.1.2 基本性质 213

7.1.3 主要结果 215

7.2 规范的递增描述 216

7.2.1 非形式的介绍 216

7.2.2 操作调用 217

7.2.3 INCLUDES子句 219

7.2.4 可见性规则 220

7.2.5 传递性 220

7.2.6 机器的重命名 221

7.2.7 PROMOTES和EXTENDS子句 221

7.2.8 实例 221

7.3 递增的规范描述和规范共享 222

7.3.1 非形式的介绍 222

7.3.3 可见性规则 223

7.3.2 USES子句 223

7.3.4 传递性 224

7.3.5 机器重命名 224

7.4 形式定义 224

7.4.1 语法 224

7.4.2 类型检查 225

7.4.3 INCLUDES子句的证明义务 229

7.4.4 USES子句的证明义务 231

7.5 练习 233

8.1.1 非形式的规范 234

8.1 一个货单系统 234

第8章 抽象机的实例 234

8.1.2 机器Client 235

8.1.3 机器Product 236

8.1.4 机器Invoice 238

8.1.5 机器Invoice_System 241

8.2 电话交换机 242

8.2.1 非形式的规范 242

8.2.2 机器Simple_Exchange 244

8.2.3 机器Exchange 247

8.3 电梯控制系统 249

8.3.1 非形式的规范 249

8.3.2 机器Lift 250

8.3.3 活性（liveness）的证明 254

8.3.4 活性证明义务的表述 255

8.4 练习 257

参考文献 257

第三部分 程序设计 258

第9章 顺序和循环 258

9.1 顺序 258

9.1.1 语法 258

9.1.2 公理 258

9.1.3 基本性质 259

9.2.1 引论 261

9.2 循环 261

9.2.2 定义 262

9.2.3 循环终止的解释 264

9.2.4 循环的前－后关系的解释 267

9.2.5 循环终止的实例 268

9.2.6 不变式定理 268

9.2.7 变动量定理 269

9.2.8 变动量和不变式定理的进一步实用化 271

9.2.9 传统循环 272

9.3 练习 277

10.0.1 重用前面的算法 280

第10章 程序设计实例 280

10.0 方法学 280

10.0.2 循环结构的证明规则 282

10.0.3 顺序结构的证明规则 283

10.1 无约束搜索 283

10.1.1 引言 283

10.1.2 比较两个序列 286

10.1.3 计算一个函数的自然数逆 290

10.1.4 自然数的除法 292

10.1.5 递归函数的特殊情况 294

10.1.6 给定底的对数 296

10.1.7 整数平方根 297

10.2 有约束搜索 298

10.2.1 引言 298

10.2.2 线性搜索 300

10.2.3 在数组中的线性搜索 302

10.2.4 在矩阵里的线性检索 303

10.2.5 二分搜索 304

10.2.6 再论单调函数 307

10.2.7 数组里的二分搜索 311

10.3 自然数 314

10.3.1 基本模式 314

10.3.3 扩展基本模式 315

10.3.2 自然数求幂 315

10.3.4 对序列求和 317

10.3.5 子数列移位 318

10.3.6 向排序的数组中插入 320

10.4 序列 321

10.4.1 引言 321

10.4.2 累计序列里的元素 323

10.4.3 数的基数表示 325

10.4.4 将自然数转换为基数表示 326

10.4.5 二元运算的快速计算 329

10.4.6 左递归和右递归 332

10.4.7 过滤器 335

10.5 树 343

10.5.1 公式的记法 343

10.5.2 将树变换到公式 344

10.5.3 从树变换到波兰表示串 346

10.5.4 将公式变换到波兰表示串 347

10.6 练习 353

参考文献 355

11.1.1 非形式的讨论 356

11.1 广义代换的精化 356

第11章 精化 356

第四部分 精化 356

11.1.2 形式定义 357

11.1.3 广义代换的相等 358

11.1.4 单调性 358

11.1.5 广义赋值的精化 359

11.2 抽象机的精化 361

11.2.1 非形式的讨论 361

11.2.2 形式定义 364

11.2.3 充分条件 364

11.2.4 单调性 368

11.2.5 实例重温 372

11.2.6 最后的润色 373

11.2.7 精化条件的直观解释 378

11.2.8 对小例子的应用 379

11.3 形式定义 380

11.3.1 语法 380

11.3.2 类型检查 381

11.3.3 证明义务 384

11.4 练习 386

参考文献 392

12.1.1 引言 394

12.1 精化的实现 394

第12章 构造大型抽象机 394

12.1.2 有关引入的实际考虑 397

12.1.3 IMPLEMENTATION结构 399

12.1.4 IMPORTS 子句 400

12.1.5 可见性规则 401

12.1.6 机器重命名 401

12.1.7 VALUES 子句 401

12.1.8 IMPORTS和INCLUDES子句的比较 403

12.1.9 PROMOTES和EXTENDS子句 403

12.1.10 再论具体常量和具体变量 403

12.1.11 在实现中允许出现的各种结构 404

12.2 共享 409

12.2.1 引言 409

12.2.2 SEES子句 412

12.2.3 可见性 412

12.2.4 传递性和循环定义 413

12.2.5 机器重命名 413

12.2.6 USES 子句和SEES子句的比较 414

12.3 再论循环结构 414

12.4 多重精化和实现 414

12.5 递归定义的操作 416

12.5.1 引言 417

12.5.3 证明规则 419

12.5.2 语法 419

12.6 形式证明 421

12.6.1 一个IMPLEMENTATION的语法 421

12.6.2 对 IMPORTS 子句的类型检查 422

12.6.3 对SEES子句的类型检查 423

12.6.4 一个IMPLEMENTATION的证明义务 423

12.6.5 对SEES子句的证明义务 426

13.1 一个基本机器库 427

13.1.1 机器BASIC_CONSTANTS 427

第13章 精化的实例 427

13.1.2 机器BASIC_IO 428

13.1.3 机器BASIC_BOOL 428

13.1.4 机器BASIC_enum 429

13.1.5 机器BASIC_FILE_VAR 429

13.2 实例研究：数据库系统 430

13.2.1 有关文件的机器 432

13.2.2 有关对象的机器 440

13.2.3 一个数据库 445

13.2.4 界面 450

13.3.2 机器SEQUENCE_VAR 457

13.3.1 机器ARRAY_VAR 457

13.3 一个实用的抽象机库 457

13.3.3 机器SET_VAR 458

13.3.4 机器ARRAY_ECTION 458

13.3.5 机器SEQUENCE_COLLECTION 458

13.3.6 机器SET ECTION 459

13.3.7 机器TREE_VAR 459

13.4 实例研究：锅炉控制系统 463

13.4.1 引言 463

13.4.2 非形式的规范 464

13.4.3 系统分析 467

13.4.4 系统集成 473

13.4.5 形式化规范和设计 475

13.4.6 最后的体系结构 485

13.4.7 修改初始规范 486

参考文献 488

附录 489

附录A 记法综述 489

附录B 语法 493

附录C 定义 500

附录D 可见性规则 510

附录E 规则和公理 514

附录F 证明义务 520