本书是有关B方法的最重要的著作，由B方法的发明人J—R Abrial撰写。B方法是目前国际上最受重视的实用性软件形式化方法之一，人们用它编写软件系统规范，进行系统设计和编程；B方法已被用在一些极其重要的软件项目中并取得了很大成功。本书由4部分组成，内容涵盖了B方法的所有方面，这些部分分别介绍B方法所用的数学基础，用B方法描述软件系统规范的语言记法，基本程序结构和程序实例，系统模块化、分层设计和精化。本书适用于汁算机科学工作者、软件系统开发工作者和计算机专业的学生，可作为高校有关软件形式化方法和软件系统设计课程的教材，或者作为B方法的标准参考手册。
第1章 数学推理
第2章 集合形式
第3章 数学对象
第4章 抽象机引论
第5章 抽象机的定义
第6章 抽象机理论
第7章 大型抽象机
第8章 抽象机的实例
第9章 顺序和循环
第10章 程序设计实例
第11章 精化
第12章 构造大型抽象机
第13章 精化的实例
附录A 记法综述
附录B 语法
附录C 定义
附录D 可见性规则
附录E 规则和公理
附录F 证明义务
随着计算机应用逐步渗透到社会生产生活的各个领域，我们今天看到了一种非常奇特白现象：一方面，计算机已被看做是现代科学技术开发出的最强有力的工具，是“用之万事而皆灵”的魔杖。计算机的介入改造了所有的行业和部门，不断改变着我们的工作和生活方式，是否应用了计算机已经成了评判一个行业是否现代化的最重要标志。另一方面，促成这种变化的领域本身的情况却很不令人乐观。计算机系统的不可靠也已成为人所共知的事实。在听到“是计算机系统出了问题”时，世人都已经习惯于视如天命而自认倒霉，再也没有进一步去追究责任的兴趣和意愿了。看到计算机系统正在越来越多地控制着我们周围的环境，一些系统的失误可能给人们的生命财产造成巨大损失时，作为计算机工作者难道不该不寒而栗?难道我们的软件开发工作就应该永远停留在这样的水平?系统的质量就应该永远这样没有保证吗?
实际上，人们早已开始从各种角度研究软件的开发方法和途径，研究软件开发的本质和规律性，总的目标就是希望改变目前这种基于个人技术、缺乏科学指导的软件开发方式，为将来的软件开发过程和作为其产品的软件系统提供更坚实的科学基础。软件形式化方法就是这样一个研究领域。经过几十年的努力，软件形式化方法的研究已经取得了许多重要成果，一些成果已经被应用于实际的软件开发工作，取得了很好的效果。
本书作者J-RAbrial在软件形式化方法及其应用领域中做出了非常重要的贡献。J-RAbrial从20世纪70年代开始研究数据结构和程序的形式化问题，他于20世纪70年代后期在牛津大学程序设计研究组(PRG)访问期间做丁规范语言Z的开创性工作。后来Z被PRG和其他研究组织广泛研究和发展，现已成为许多计算机科学技术课程和教育项目的基础，并在英国及全欧洲的工业界得到应用，用于描述复杂软件系统的规范，支持严格化的软件系统开发过程。为使形式化方法与软件开发更平滑地衔接，J-RAbrial从20世纪80年代前期开始了B方法的研究，目的是希望为实际软件开发过程提供一个坚实的数学基础。在B方法的研究和开发中，J-RAbrial及其合作者不仅关心软件的严格规范描述问题，而且特别关注从严格规范到最终程序的演化过程(一般称为精化，refinement)，以及对这一过程的自动支持。B方法的开发从其早期开始就是与工业界的实际应用一起进步的，在其发展过程中，人们就已经用它作为工具开发了一系列关键性的应用软件系统。一个早期的重要实例是巴黎地铁列车的信号系统，这一系统为减少列车间距、提高整个地铁系统的安全性做出了显著贡献。这本《B方法》就是J-RAbrial对B方法的总结整理。
B方法是一种用于描述、设计计算机软件的严格方法，其作用一直延伸到代码生成，人们已经实现了一些工具系统，支持基于B方法的软件开发的全过程。本书完整地介绍了B方法的数学理论基础，精确定义了B方法中使用的规范语言形式，还给出了许多运用B方法进行软件开发的例子。其中一些例子有一定规模和很强的实际背景，有些例子就是实际系统的简化版本。从这本书的阅读中，我们可以看到一个复杂的软件系统可以怎样从一段有关其功能的严格描述中逐步演化出来，如何在这种演化过程中维持某些不变性，怎样保证后面做出的更加细节的描述不破坏已有的定义和已经证明的性质，如何自动地产生出这一过程中的“证明义务”。实际上，在今天的软件开发过程中，人们也在不自觉地做着这些事情，基本上是靠开发者的直觉和朴素技术去控制和解决问题。这种缺乏科学指导的不严格的方式，是软件开发过程中产生错误的一个重要原因。因此，从某种角度看，B方法(以及其他严格的软件开发方法)也就是希望把人们在软件开发中的实际工作过程整理清楚，为其建立坚实的理论基础，将其规范化和严格化。
我们常常可以听到有关“软件形式化方法有什么用”的质问，我们认为这实际上是一个错误的问题。任何不幼稚的计算机工作者都不会期望能开发出某种新技术或者新方法，一劳永逸地解决软件领域的问题。计算机软件系统是人类有史以来制造出的最复杂的产品，可具有成百万甚至成千万行代码的巨大规模，其各组成部分之间可能存在的错综复杂的直接和间接交互作用方式，其静态结构与动态行为之间构成难以琢磨的关系。我们还没有过制造和把握如此复杂的系统的需要和经验。另一方面，我们需要开发出许许多多的软件，以满足千变万化、层出不穷的实际需要，这些工作又常常必须在较低开发成本和较短开发周期的条件下完成，因此就不可能像开发基础硬件那样组织一支最优秀的庞大队伍，不可能投入足够的金钱和时间。所有这些因素造成的结果就是软件的复杂性问题将永远陪伴着我们。
由于这些情况，任何有助于我们理解、控制、管理软件系统复杂性的理论、技术或方法都是非常有价值的。今天，软件工作者们最重要的努力方向就是去克服或缓解软件复杂性的障碍。他们在许多层次上工作：通过高层管理手段组织软件开发活动；通过严格的工作规范，企图深入控制软件开发的整个过程；通过安排丰富而烦琐的人际信息交互活动，设法使在需求、设计和各个后续阶段引进的错误和不良结构可能及早被发现；通过不同抽象技术，设法隔离各个层次、各个部件内部的复杂性，提供层次间或者部件间的清晰界面；通过研究各种程序开发模型及其支持技术，使软件工作中的一些模式和难点能够被屏蔽在模型之中，得到模型的充分支持；通过各种软件的组件形式尽可能地利用已有工作成果，降低开发新软件的代价和复杂性；通过开发合适的语言和其他表述形式，以满足在各个层次上严格而方便地描述软件及其不同侧面的需要；通过各种技术手段和工具，对软件开发过程提供尽可能多的支持，或者支持人们对开发结果进行更深入的分析；通过人员的训练，提高参与软件工作的每个人的认识能力和工作能力，使他们能够成为软件质量的支点而不是潜在的破坏者；如此等等。软件形式化方法可能在许多层次上起作用。
实际上，软件形式化方法正在逐步渗入我们的日常软件开发活动。各种所谓的“无差错”或者“干净”软件开发技术，貌似新颖的“基于契约的软件开发”等，实际上不过是软件形式化方法研究成果的实践性版本。“断言”、“前条件和后条件”、“不变式”等术语已经在我们周围不绝于耳。一些国家和部门的软件开发规范已经明确提出，关键性软件的开发过程必须有软件形式化方法的参与。我们相信，终归会有一天，不知道什么是循环不变式或者数据不变式的人，将没有资格参加任何关键软件的开发工作。到了那个时候，软件的质量一定会提高到一个新水平。每个关心自己的事业和个人发展的计算机专业工作者，都必须重视这些情况。我们也希望本书的出版将能为国内计算机教育和实践提供一些参考。
作为译者，我非常感谢电子工业出版社支持出版这本形式化方法的重要著作，感谢周宏敏编辑为本书付出的辛勤劳动。最后还要感谢夏萍和丛欣对我持之以恒的支持和帮助。
裘宗燕
北京大学数学学院信息科学系
2004年5月
本书是一个长篇论述，按照我的见解，它要解释的是程序设计的工作(无论是大是小)将可能怎样通过回归数学而取得成功。
对于这一说法，我的第一层意思是，有关一个程序要做什么的精确数学定义必须首先给出，并将其作为其构造的本原。如果缺乏这种定义，或者它过于复杂，我们或许会怀疑将来做出的程序能否真正表示什么东西。我的信念是，抽象地说，一个程序根本就不表示任何东西。要说一个程序表示了些什么，只能是相对于某个在它之前就有的意图，无论这一意图是以这种或者那种形式表示的。在这一点上我并不反对某些人，他们可能感到用“英语”这个词代替“数学”就更舒服一些。我只是怀疑，能不能交给这样的人一件更困难的工作。
我还认为，这种“回归数学”应该表现在一个真正的程序构造过程中，其中的工作就是要给程序一种定义良好的意义。这里的想法是让程序构造的技术过程伴随着一个证明构造的类似过程，由它保证所提供的程序与其预期的意义相符。
同时关注一个程序的体系结构及其证明其实是非常有效的。例如，当证明变得非常难搞时，多半程序也会是那样；而构造证明的各种成分(抽象、实例化、分解)也与构造程序中的那些东西很类似。理想地说，在一个程序的结构与其正确性的证明之间的关系应该非常紧密，以致我们根本无法查清两者中究竟哪一个是从另一个派生出来的。而后我们就可以很合理地说，构造一个程序不过就是构造一个证明。
今天只有很少的程序是按照这种方式描述和构造出来的。那么，这是不是正好对应着另一个事实，即今天有那么多的程序都是极其脆弱的呢?
第二书店&China-pub战略联盟提供专业服务
第二书店联系方式 010-64348411 webmaster@dearbook.com