问阻碍广泛采用正式方法的障碍是什么？

EN

工程师是一个能用一美元做任何白痴用10美元都能做的事的人。

资源限制，预算限制，时间限制，这些都很重要。

使用形式化方法开发软件通常要花费更多的钱，并且比不使用它花费的时间长得多。而且，对于许多项目来说，最困难的部分是理解业务需求。在这种情况下，使用正式方法可以为您提供证据，证明您的代码100%符合您对业务需求的不完整和不正确的理解。

因此，正式方法、证明、程序验证和类似技术的使用通常仅限于“重要的东西”，即航空电子软件、医疗设备控制系统、发电厂等。

编程还是不编程？

要解决软件产品的问题，在了解了需求之后，可以使用编程语言编写程序，也可以使用正式语言指定程序，并使用代码生成工具。后者只是增加了一个抽象级别。

做正确的事情还是做正确的事情？

正式的方法为您提供了一个证明您的软件按照规范工作的证据。所以你的产品做得对。但它能做正确的事情吗？

您正在工作的需求可能是不完整的或不明确的。他们甚至可能是辆马车。在最坏的情况下，真正的需求甚至没有被表达出来。但是一张图片值一千字，只是谷歌的“客户想要什么”的图片，比如这篇文章的图片：

--手续成本--

在一个完美的世界里，你会从一开始就有完整的详细和完美的需求。然后，您可以完全指定您的软件。如果您选择正式的方式，您的代码将自动生成，这样您的工作效率就会更高。生产率的提高将抵消正式工具的成本。现在每个人都会使用正式的方法。那为什么不呢？

在实践中，这很少是现实！这就是为什么这么多瀑布项目失败的原因，以及为什么迭代法开发方法(敏捷、RAD等)起了带头作用:它们可以处理不完整和不完美的需求、设计和实现，并对它们进行细化，直到它们变得很好。

重点来了。对于形式化方法，每次迭代都需要有一个完全一致的形式化规范。这需要仔细的思考和额外的工作，因为形式逻辑是不宽容的，也不喜欢不完整的想法。在这种约束下，简单的丢弃实验变得昂贵。每一次迭代都会导致回溯(例如，一个不起作用的想法，或者一个被误解的要求)，也是如此。

在实践中

当由于法律或合同原因而不必使用正式方法时，您也可以在没有正式系统的情况下实现非常高的质量，例如通过使用基于合同的编程和其他良好做法(例如代码评审、TDD等)。您将无法证明您的软件工作，但您的用户将享受工作软件更快。

更新:测量工作量

在2018年10月的“ACM的来文”杂志上，有一篇关于在现实世界中正式验证的软件的有趣文章，并对此做出了一些估计。

有趣的是(基于军事设备的OS开发)，生产经过正式验证的软件需要比传统的工程技术花费3.3倍的精力。所以它真的很昂贵。

另一方面，与传统的工程软件相比，以这种方式获得高安全性软件所需的工作量是传统工程软件的2.3倍，如果您将这些软件添加到高安全级别(EAL 7)认证的话。因此，如果您有很高的可靠性或安全性要求，那么肯定有一个正式的业务案例。

seL4设计和代码开发花了两年时间。把这些年来所有的血清特异性证明加在一起，总共是18个人年，总共有8,700行C代码。相比之下，L4家族的另一个微内核--开心果L4Ka::Pistachio的大小与seL4相当，需要6年时间才能开发出来，而且没有提供明显的保证。这意味着在验证软件和传统工程软件之间只有一个3.3因素。根据Colbert和Boehm的估算方法，8对8700行C代码进行传统的通用标准EAL7认证需要超过45.9人年。这意味着正式的二进制级实现验证已经超过了2.3的因素，比公共标准的最高认证级别要低得多，但却提供了更强的保证。

任何语言中的每一个程序都可以被认为是一种正式的规范(相当于某种车床)。用于验证形式正确性的任何更高级别的“形式规范”也只是另一个程序。但是它(通常)是一个糟糕的，不完整的，模糊的，没有充分考虑的程序。而且并不是巧合，通常是由不知道如何编程的人编写的(他们通常是领域专家)。

因此，证明一个程序是兼容的(产生相同的答案，或者不管你如何描述它)与它的更高层次的形式要求是一致的，不变的归结于如何解决更高级别的形式规范中的歧义。这样做是没有好的一般目的的。

将高层需求映射到较低级别的详细信息是真正编程的要点。毫不奇怪，程序员正在进行的核心工作--阅读和解释规范--不能用挥手来代替，并说：“现在，看看这个示例程序是否遵守了这个高级的形式规范”。

即使在逻辑编程的早期，这个概念似乎很有希望(因为高级规范和实际底层程序都可以用同一种语言编写)，这个核心问题仍然难以解决。