序言

本书远远强于一本新的程序设计手册,它介绍了一种方法,将程序的设计包括在一个全局性的进程之中,这一进程从对问题的理解开始,一直到验证其解答的合法性。

这一方法的数学基础提供了一种精确性,所提出的记法形式完全排除了日常语言的歧义性。与此同时,这一进程对于产业界的使用而言又是足够简单的。"产业界的"事实上是一个很关键的词语。

形式化方法的一般性目标是为问题的规范描述提供正确性基础。在这里,我们可以看到怎样能发现一个解,一步一步地,通过一个受到连续监控的进程。对其中每一步合法性的数学验证与精化活动如此紧密地捆绑在一起,使人根本无法将设计决策与检查过程分离。想象力得到了精确性的极大帮助! 那么,效率怎么样?设计过程会不会太长?做设计的人们能胜任这种工作吗?机器的能力够不够实现这种方法?对于这些的回答都很容易给出。让我来告诉你们。

我的公司从六十年代开始涉足于铁路控制系统的实现,这种工作必须满足极高的安全性要求。在我们开始使用编程逻辑不久(七十年代末),我们就不得不去解决软件的正确性问题。与其他方法一起,我们选择使用了由C.A.R. Hoare提出的程序证明方法。在1986年,J.-R. Abrial给我们介绍了B方法,我们决定学习和使用它。当时还不存在工具,我们在对工具开发的贡献是用我们的应用,提供了一个真实世界的测试实例,并建议了一些改进。现在有关的工具已经能够从市场上找到,因此这个方法也能以其最有效的方式使用了。那么,我们学到了什么呢?

对于将软件用于与安全有关的应用领域而言,对于这一方法的使用已经成为我们增强自己信心的决定性因素。进一步说,新的国际标准也建议在安全攸关软件的规范描述和设计方面使用形式化方法。 感谢J.-R. Abrial使我们有了一种构造正确软件的产业界的方法。我们相信本书将使其读者们确信,采用这一方法能使他们节约金钱。

Pierre Chapront
技术主管
GEC-ALSTHOM Transport