这一方法的数学基础提供了一种精确性,所提出的记法形式完全排除了日常语言的歧义性。与此同时,这一进程对于产业界的使用而言又是足够简单的。"产业界的"事实上是一个很关键的词语。
形式化方法的一般性目标是为问题的规范描述提供正确性基础。在这里,我们可以看到怎样能发现一个解,一步一步地,通过一个受到连续监控的进程。对其中每一步合法性的数学验证与精化活动如此紧密地捆绑在一起,使人根本无法将设计决策与检查过程分离。想象力得到了精确性的极大帮助! 那么,效率怎么样?设计过程会不会太长?做设计的人们能胜任这种工作吗?机器的能力够不够实现这种方法?对于这些的回答都很容易给出。让我来告诉你们。
我的公司从六十年代开始涉足于铁路控制系统的实现,这种工作必须满足极高的安全性要求。在我们开始使用编程逻辑不久(七十年代末),我们就不得不去解决软件的正确性问题。与其他方法一起,我们选择使用了由C.A.R. Hoare提出的程序证明方法。在1986年,J.-R. Abrial给我们介绍了B方法,我们决定学习和使用它。当时还不存在工具,我们在对工具开发的贡献是用我们的应用,提供了一个真实世界的测试实例,并建议了一些改进。现在有关的工具已经能够从市场上找到,因此这个方法也能以其最有效的方式使用了。那么,我们学到了什么呢?
Pierre Chapront
技术主管
GEC-ALSTHOM Transport