实际上，人们早已开始从各种角度研究软件的开发方法和途径，研究软件开发的本质和规律性，总的目标就是希望改变目前这种基于个人技术、缺乏科学指导的软件开发方式，为将来的软件开发过程和作为其产品的软件系统提供更坚实的科学基础。软件形式化方法就是这样一个研究领域。经过几十年的努力，软件形式化方法的研究已经取得了许多重要成果，一些成果已经被应用于实际的软件开发工作，取得了很好的效果。

本书作者Jean-Raymond Abrial在软件形式化方法及其应用领域中做出了非常重要的贡献。Jean-Raymond Abrial从1970年代开始研究数据结构和程序的形式化问题，他1970年代后期在牛津大学程序设计研究组（PRG）访问期间做了规范语言Z的开创性工作。后来Z被PRG和其他研究组织广泛研究和发展，现已成为许多计算机科学技术课程和教育项目的基础，并在英国及全欧洲的工业界得到应用，用于描述复杂软件系统的规范，支持严格化的软件系统开发过程。为使形式化方法与软件开发更平滑地衔接，Jean-Raymond Abrial从1980年代前期开始了B方法的研究，目的是希望为实际软件开发过程提供一个坚实的数学基础。在B方法的研究和开发中，Jean-Raymond Abrial及其合作者不仅关心软件的严格规范描述问题，而且特别关注从严格规范到最终程序的演化过程（一般称为精化，refinement），以及对这一过程的自动支持。B方法的开发从其早期开始就是在与工业界实际应用一起进步的，在其发展过程中，人们就已经用它作为工具开发了一系列关键性的应用软件系统。一个早期的重要实例是巴黎地铁列车的信号系统，这一系统为减少列车间距、提高整个地铁系统的安全性做出了显著贡献。这本《B方法》就是Jean-Raymond Abrial对B方法的总结整理。

B方法是一种用于描述、设计计算机软件的严格方法，其作用一直延伸到代码生成，人们已经实现了一些工具系统，支持基于B方法的软件开发的全过程。本书完整地介绍了B方法的数学理论基础，精确定义了B方法中使用的规范语言形式，还给出了许多运用B方法进行软件开发的例子。其中一些例子有一定规模和很强的实际背景，有些例子就是实际系统的简化版本。从这本书的阅读中，我们可以看到一个复杂的软件系统，可能怎样从一段有关其功能的严格描述中逐步演化出来，如何在这种演化中维持某些不变性，怎样保证后面做出的更加细节的描述不破坏已有的定义和已经证明的性质，如何自动地产生出这一过程中的"证明义务"。实际上，在今天软件开发过程中，人们也在不自觉地做着这些事情，基本上是靠开发者的直觉和朴素技术去控制和解决问题。这种缺乏科学指导的不严格的方式，是软件开发过程中产生错误的一个重要原因。因此，从某种角度看，B方法（以及其他严格的软件开发方法）也就是希望把人们在软件开发中的实际工作过程整理清楚，为其建立坚实的理论基础，将其规范化和严格化。

常常可以听到有关"软件形式化方法有什么用"的质问，我们认为这实际上是一个错误的问题。任何不幼稚的计算机工作者都不会期望能开发出某种新技术或者新方法，一劳永逸地解决软件领域的问题。计算机系统软件系统是人类有史以来制造出的最复杂的产品，其成百万成千万行代码的巨大规模，其各组成部分之间可能存在的错综复杂的直接和间接交互作用方式，其静态结构与动态行为之间难以琢磨的关系。人类从未有过制造和把握如此复杂的系统的需要和经验。另一方面，我们需要开发出许许多多的软件，以满足千变万化、层出不穷实际需要，这些工作又常常必须在较低开发成本和较短开发周期的条件下完成，因此就不可能像开发基础硬件那样组织一支最优秀的庞大队伍，不可能投入足够的金钱和时间。这些造成的结果就是软件的复杂性问题将永远陪伴着我们。

由于这些情况，任何有助于我们理解、控制、管理软件系统复杂性的理论、技术或方法都是非常有价值的。今天软件工作者们最重要的努力方向就是去克服或缓解软件复杂性的障碍。他们在许多层次上工作：通过高层管理手段组织软件开发活动；通过严格的工作规范，企图深入控制软件开发的整个过程；通过安排丰富而烦琐的人际信息交互活动，设法使在需求、设计和各个后续阶段引进的错误和不良结构可能及早被发现；通过不同抽象技术，设法隔离各个层次各个部件内部的复杂性，提供层次间或者部件间的清晰界面；通过研究各种程序开发模型及其支持技术，使软件工作中的一些模式和难点能够被屏蔽在模型之中，得到模型的充分支持；通过各种软件的组件形式尽可能地利用已有工作成果，降低开发新软件的代价和复杂性；通过开发合适的语言和其他表述形式，以满足在各个层次上严格而方便地描述软件及其不同侧面的需要；通过各种技术手段和工具，对软件开发过程提供尽可能多的支持，或者支持人们对开发结果进行更深入的分析；通过人员的训练，提高参与软件工作的每个个人的认识能力和工作能力，使他们能够成为软件质量的支点而不是潜在的破坏者；如此等等。软件形式化方法可能在许多层次上起作用。

实际上，软件形式化方法正在逐步渗入了我们的日常软件开发活动。各种所谓的"无差错"或者"干净"软件开发技术，貌似新颖的"基于契约的软件开发"等等，实际上不过是软件形式化方法研究成果的实践性版本。"断言"，"前条件和后条件"，"不变式"等等术语已经在我们周围不绝于耳。一些国家和部门的软件开发规范已经明确提出，关键性软件的开发过程必须有软件形式化方法的参与。我们相信，终归会有一天，不知道什么是循环不变式或者数据不变式的人，将没有资格参加任何关键软件的开发工作。到了那个时候，软件的质量一定会提高到一个新水平。每个关心自己的事业和个人发展的计算机专业工作者，都必须重视这些情况。我们也希望本书的出版将能为国内计算机教育和实践提供一些参考。

作为译者，我非常感谢电子工业出版社支持出版这本形式化方法的重要著作，感谢周宏敏编辑为本书付出的辛勤劳动。最后还要感谢夏萍和丛欣对我持之以恒的支持和帮助。

裘宗燕
北京大学数学学院信息科学系
2004年5月