关于形式方法的10个误解 · Buttondown

形式方法Formal-Methods是一个非常有趣和重要的领域，但不是程序员熟悉的领域，这会导致很多误解。这是试图解决其中的一些问题。免责声明，我专注于其中几个工具，但相信我对其余工具足够熟悉，可以准确地呈现它们。

1.形式方法FM是关于证明代码正确

“正确”在 FM 中是一个肮脏的词。在 FM 中，我们验证是否符合规范：对代码属性的严格、明确的描述。“正确性”是客户决定的。我们通常在假设它代表“正确性”的情况下编写规范，因此符合规范意味着“正确”，但这并不总是正确的。如果规范是错误的或不完整的，那么一致性就没有多大意义。

这听起来像是在狡辩，但出于两个原因，这非常重要。首先，它更诚实地说明了 FM 的局限性。您可能会听到 FM 人说“环境超出了证明的范围”。这就是我们对我们可以保证和不能保证的事情非常小心：如果我们的规范没有明确包含环境影响，我们就无法说明我们的程序在环境影响下的行为方式。其次，知道如何编写好的规范与知道如何验证它们一样是 FM 的基础。

事实上，我认为“编写好的规范”是最有用的一般程序员的 FM 学科的一部分。这对于外人来说是非常难的，但是一旦你练习了它就很容易，并且通常非常有用。能够看到一个函数然后“啊，这是规范”对于编写测试、断言、类型等一切都很有用。我还发现，我的研讨会学生需要大量练习，无论他们使用何种特定的形式方法。

2. 形式方法是关于证明代码

诚然，代码是 FM 最常见的目标。但是任何可以“计算编码”的东西都可以被验证。这包括大规模系统设计 (TLA+)、需求 (Alloy)、语言语义 (K)、业务流程 (BPMN)、硬件、本体……大部分重点都放在代码上，因为代码很多，而且人们不太可能意识到他们可以以可验证的方式对其他内容进行编码。真遗憾：除了 FM 之外，我们还有很多工具可以帮助我们编写正确的代码，但几乎没有任何工具可以帮助我们编写正确的其他东西。使其他东西可验证为我们提供了我们没有的工具，我认为这就是形式方法可以最快地发挥最大作用的地方。

3. 形式方法是关于证明

同样，大部分是 true，但证明意味着您自己正在编写完整的数学证明。只有当您与Coq 或 Isabelle 这样的证明助手一起工作时才会发生这种情况。大多数时候人们通过工具抽象进行形式验证：模型检查器、SMT 求解器、模拟、类型检查器等。

这似乎是一个小小的术语问题，但它对我们如何看待该领域产生了重大影响。这意味着你需要有很强的纯数学背景才能完成任何事情。虽然了解数学肯定会有所帮助，但您可以使用许多工具而无需自己编写完整的证明。

4. FM 需要一种特殊的语言

这是C 中经过验证的 LeftPad。Frama-C 将规范语言改造为 C，因此您可以在 C 代码上使用形式化方法。大多数企业语言都有可用的 FM 改造。然而，这些语言并不是为了让 FM 变得容易，这就是为什么人们用专门的 FM 语言做大量工作的原因。但是您仍然可以在遗留项目中使用 FM。

（通常面向开发人员的可供性使验证代码更加困难。动态调度、自由别名、用户输入等。还有像 Ada 这样的“混合”语言，其中语言的一个子集围绕验证而设计，其余围绕一般可用性.)

5. FM需要博士学位

您需要大量专业知识才能使用证明助手，您可以在其中手动编写大部分。你从证明助理那里得到的越多，你需要的学术背景就越少。我不是说容易，我只是说这是日常开发人员可以学会使用的东西（通过时间投入）。

证明助手主导了大众的想象有两个原因：

1. 他们待的时间最长。直到最近 15 年，您才可以在不使用证明助手的情况下验证大量代码。
2. 他们是最“强大”的。自动化工具不够智能，无法自行验证编译器或整个操作系统，因此，如果您想做任何雄心勃勃的事情，则需要使用证明助手。

6. FM 必须是端到端的

人们认为FM是唯一有用的，如果你可以验证所有属性的整个程序：一个终端对终端规范的全面核查。如果你想要绝对的保证，这是真的。您还可以进行部分验证，以更便宜的方式验证更少。你可以：

• 验证代码的某些属性。这在主流语言中已经很常见，诸如“这是类型安全的”或“这不会改变别名指针”之类的属性。使用 FM 只是将其扩展到任意属性。
• 验证一些代码的属性。您有一个经过形式验证的“核心”和经过非形式验证的周围代码。这是很多行业公司的做法。您也可以使用单独的库执行此操作，然后将这些库包含在更大的项目中。
• 验证代码模型的属性。这就是您在验证“设计规范”（如 TLA+）时所做的工作。不过，您仍然必须自己编写代码。

我已经看到所有这些在实践中运作良好。实际上取决于问题域和您认为重要的内容。

7. FM太贵了

公众的看法是，FM 仅在极其昂贵的关键任务系统上才值得。

我认为更准确的权衡是

学习 FM 的时间 + 应用 FM 的时间 - 应用 FM 节省的时间vs生产中错误的财务成本 + 调试时间

8. FM只适用于大公司

毫无疑问，我的读者都听得津津有味，所以我首先在一家拥有 10 名工程师的公司开始编写形式规范。在我的教学过程中，我听说有人在更小的公司成功应用了它，即使只有一两个工程师。我认为你更有可能在大公司看到 FM，因为他们有更多的项目“显然”从中受益，而且工程师越多，个人拥护该学科的机会就越大。

我确实相信与验证代码相比，验证系统对更广泛的公司有益，这就是为什么我专注于教授 TLA+ 和 Alloy 而不是 Coq 或 Dafny。但我一直在寻找有助于代码验证成为主流的新语言或技术改进，我相信我们将在未来几年开始看到可负担性的巨大进步。

9.如果需求发生变化，FM 将不起作用

“FM 会告诉你你做的东西是否正确，但不会告诉你你做的东西是否正确。” 这只是关于客户需求的一个基本事实的一个极端例子：如果它们发生变化，您将不得不放弃工作，无论是一些代码、完整的测试套件还是数学证明。只是单元测试比形式证明更便宜，所以你用 FM 赚了更多的钱。

问题是这通常作为软件的普遍事实而被提出，而这仅适用于一个子集。当您为外部客户编写软件时，需求更改最常发生，就像您在咨询中看到的那样。如果您正在制作内部软件或销售软件产品，那么您可以更好地控制需求变更。您也更有可能维护遗留软件和编写基础设施代码。如果您出于性能原因需要将夜间批处理作业移动到实时任务队列，那么您的老板不太可能说“没关系把它放在区块链上”。我的意思是他们可以，但发生的频率较低。项目时间线更长，因此 FM 更有价值。

10.FM 是正确的必要条件

让我们以另一方面的误解作为结束：没有形式方法，软件永远不会“好”的普遍观念。

无论如何，代码正确和被验证正确之间有很大的区别。您可以在不需要证明的情况下以非常高的置信度确定代码符合规范：类似于“99% 确定它 100% 正确”。您可以通过真正彻底的测试、真正彻底的代码审查或遵循严格的流程等来做到这一点。通常，这些比完整的端到端代码验证便宜。即使使用测试、CI/CD 和定期代码审查等“主流”技术，也能让您对自己的正确性充满信心。你并不需要任何的这种形式化方法。