人们为什么不使用正式方法？ - 2019年

我在软件工程栈交换中看到了这个问题：防止广泛采用正式方法的障碍是什么？这个问题被关押为基于意见，大部分答案都是“太贵!!!”的东西。或“网站不是飞机!!!”这些都是真的，但不要非常解释。我写了这一点，提供了一个较大的形式方法的历史图片，为什么他们实际上是如此未使用，以及我们正在做的事情让他们使用。

在我们开始之前，我们需要放下一些条款。真的不是一个正式的方法社区，这是一个在草原上觅食的几个小乐队。这意味着不同的群体以不同方式使用术语。非常广泛地，FM有两个域：正式规格是研究我们如何编写精确，明确的规格，正式验证是研究如何证明事物是正确的。但“事情”包括代码和抽象系统。我们不仅使用单独的手段来指定这两种东西，我们经常使用不同的手段来验证它们。为了使事情更加令人困惑，如果有人说过正式的规范，他们通常意味着他们都指定和验证系统，如果有人说他们进行正式验证，他们通常意味着它们都意味着它们都指定和验证代码。

出于清晰目的，我将验证验证到代码验证（CV）和设计验证（DV），并将规范与CS和DS类似。这些不是更广泛的FM世界中使用的术语。我们首先谈论CS和CV，然后继续到DS和DV。

此外，我们可以进行部分验证，我们只验证规范的子集，或完全验证，我们验证整个规范。这可能是证明“它永远不会崩溃或接受错误的密码”或“如果您给出错误的密码三次，它永远不会崩溃或承认错误的密码并锁定帐户。”大多数此历史将假设我们正在进行全面验证。

我们还应该澄清我们正式的软件类型。大多数人将软件局面地分为高保证软件，例如医疗设备和飞机，以及其他一切。人们假设正式的方法广​​泛用于前者和后者不必要。这是，如果有的话，太乐观：大多数人在高保证软件中不使用正式方法。我们将重点关注“常规”软件。

最后，一位免责声明：我不是历史学家，而我试图做尽职调查，那么这里可能会有错误。此外，我专注于形式规范（DS和DV），因此我对代码验证的任何事情都有可能犯错误。如果你看到错了，请给我发电子邮件，我会修复它。 2

在我们证明我们的代码是正确的之前，我们需要知道什么是“正确”。这意味着具有某种形式的规范或规范，用于代码应该做什么，我们可以明确地说明特定输出是否遵循规范。只是说一个列表是“排序”尚不清楚：我们不知道我们正在排序是什么，我们正在使用什么标准，甚至是我们的意思是“排序”。相反，我们可能会说“如果对于任何两个索引I和j，则按升序排序，如果我＆l lt; j，然后l [i]＆lt; l [j]“。

第一个是作为独立于代码的语句编写它们。我们会写下我们的排序功能，并在单独的文件中写定理“这返回排序列表”。这是最古老的规范形式，仍然是Isabelle和ACL2做事的方式。 3.

第二个嵌入代码中的规格，以前/后置条件，断言和不变性的形式。我们可能会在“返回值是一个排序列表”的函数上添加一个后期位置。基于断言的规格最初是正式的，因为HOARE逻辑，并于20世纪70年代初期首次融入了一个欧几里德的编程语言。 4这种风格也被合同称为设计，是最受欢迎的工业验证形式。 5.

最后，我们有型系统。通过Curry-Howard对应，任何数学定理或证据都可以被编码为依赖类型。我们会定义“排序列表”的类型，并声明我们的函数具有类型签名[int] - ＆gt;排序[int]。

您可以看到所有这些样子的示例，让我们证明leftpad。 HOL4和Isabelle是“独立定理”规范，火花和大夫的良好示例，Spark和Dafny具有“嵌入式断言”规格，CoQ和Agda具有“依赖式”规格。 6.

如果您眯着眼睛，它看起来像这三种形式的代码规范映射到自动正确性的三个主域名检查：测试，合同和类型。这不是巧合。正确性是频谱，正式验证是该频谱的一个极端。当我们减少我们验证的严格（和努力）时，我们会获得更简单和更窄的检查，无论是否使用较弱的类型限制探索的状态空间，或向运行时推动验证。然后，任何总规格的方法都成为部分规范的手段，反之亦然：许多人认为洁净室是一种正式的验证技术，主要通过推动代码检查远远超出人类可能的代码。

验证证明代码与其规范匹配。这提出了一个问题：我们如何知道我们有正确的规格？找到合适的规范是正式方法中最大的挑战之一。它也是最升级的反对意见之一，但怀疑论者的意思是它与倡导者的想法的方式完全相同。

当户外人说“你如何有正确的规格？”他们通常在考虑验证：显示一个规格实际上是客户想要的。如果您正式证明您的代码排序列表，但客户实际上希望优步进行汤™，您只浪费了一堆时间。只有通过快速迭代和短的反馈周期，人们争辩，您是否可以验证您的要求。

确实，验证代码无法验证代码。但是这个参数有两个问题。首先是它只是延迟了FM的价值，而不是完全消除它。一旦您完成了快速迭代，您可能会想到您的客户想要的内容。然后你开始验证代码。第二，虽然我们不知道究竟是什么客户想要的，但有些事情我们可以假设他们不想要。他们不希望软件随机崩溃。他们不想要安全漏洞。每个人都认识到这一点：毕竟，没有人说你应该在你迭代时跳过单位测试。因此，至少证明您的版本控制系统不会随机删除用户预订的章节。 7.

找到正确的规格的问题更为根本：我们经常不知道我们想要的规格是什么。我们考虑了人类的要求，而不是数学术语。如果我说“这应该区分公园的鸟类”，我在说什么？我可以通过给予一堆公园和鸟类的照片来解释一个人，但这只是具体的例子，而不是捕捉从鸟类区分公园的想法。为了实际翻译成正式规格要求我们能够将人类概念形式形式化，这是一个严重的挑战。

不要让我错了，有可能弄清楚这里的适当规格，专家一直这样做。但是写作适当的规范是您需要开发的技能，就像您需要开发编码技能一样。这就是为什么许多代码验证的最近成功的成功都是我们想要的明显地图的事情以及我们可以表达我们想要的东西。例如，Compcert是一个正式验证的C编译器。这个规范有“这绝不会误解”。

这一切都不是实际的验证部分。有一个规格，您仍然需要证明代码匹配规范。

我们看到的最早的代码验证方式是Dijkstra风格的“非常努力地思考为什么这是真实的”方法，这基本上是allol旨在帮助做的。例如，我可能会“证明”插入排序通过争论

基本情况：如果我们有一个空列表并将一个元素添加到它，那将是唯一的元素，因此它将被排序。

如果我们有一个带有k个元素的排序列表并添加一个元素，我们将插入元素，以便在所有较小的数字之后和所有更大的数字之后。这意味着列表仍然排序。

显然，它看起来比这更严格，但这是一般的想法。 Dijkstra等人使用这种风格来证明一堆算法是正确的，包括许多并发原语。这也是一种风格，它引起了Knuth Quote“请注意上面的代码中的错误;我只证明它是正确的，没有尝试过。“在没有人通知的方式搞定数学证明是非常容易的，并且我读到了20％的发布的数学证明的估计，它们有错误。 Peter Guttmann有一个很好的论文，就如何获得了多法代码，如果运行，那么大量的“经过验证的”代码会立即崩溃。

同时我们正在探索如何自动证明数学定理，这是1967年出来的第一个此类定期先驱。帕斯卡社区的研究人员正在使用定理普通的普通验证计划于20世纪70年代初期，然后通过中期编程专用验证语言进行编程。十年。人们将写一些代码的属性，然后写一个可选择的证明代码具有这些属性。早些时候定理普查只是帮助人类检查并验证证明，而更复杂的人可以自己证明定理的部分。

证据很难。令人讨厌的努力。 “退出编程并加入马戏团”。令人惊讶的是，正式的代码证明往往比大多数数学家写的证据更严格！数学是一个非常有创造性的活动，具有明确的答案，如果您展示您的工作，才能有效。创造力，形式主义和计算机是一个不好的组合。

采取上述诱导。任何数学家都可以看出它，立即知道它是什么，它是如何工作的，以及它在这种情况下如何有效。这些都是我们需要严格地形式化的东西。与矛盾的证明相同，通过互相验证等，我们还需要正规化每一个假设，甚至是大多数数学家不烦恼的东西。例如，添加是关联：A +（B + C）=（A + B）+ C.定理箴言并不是先验的真实。您要么必须证明它（硬），声明这是一个假设箴言可以作为真实（危险），或者从已经证明它（昂贵）的人那里购买定理图书馆。早期审查助理竞争内置策略策略和捆绑定理图书馆。首次广泛的校验验证员之一，Spade，将其完整的算术库作为一个关键销售点宣传。

接下来，你必须实际上得到证据。您可以让谚语尝试自己找到它，或自己写它。在一般情况下，自动推断出证明是不可识别的。对于极度限制的情况，如命题逻辑或HM Type-Checki，它是“只有”NP-Complete。在大多数情况下，我们都陷入了自己的大部分证据，并让计算机验证它是正确的。这意味着您需要一个强大的背景：

您正在使用的定理谚语的复杂性，这是一个专业

让事情变得更糟，电脑物业将大量的扳手扔进证明。还记得我如何说假设加法是关联是危险的？某些语言并不关联。 C ++具有INT_MAX。 （（-1）+ int_max）+ 1是INT_MAX。 -1 +（int_max + 1）未定义。如果您假设C ++中的关联添加，您的证明将是错误的，并且您的代码将被打破。您要么必须避免使这种断言，或证明为您的特定代码段，您永远不会造成溢出。

现在，您可以说未定义的添加是一个错误，而且您应该使用带有未绑定整数的语言。但大多数语言具有妨碍证明的积极功能。采取以下代码段：

这总是真的吗？依靠。也许f修改a。也许另一个线程并发修改a。也许b别传到a，因此修改它也修改了一个。 8如果您的语言中的任何一种，则必须明确证明他们不会发生在这里。在这种情况下，纯度有助于在其他情况下丢失证明，因为它迫使您使用递归和更高阶函数来完成完成的东西。顺便提及，这两者都是编写良好功能计划的基础。对于证明，编码有什么好处！ 9.

正式的验证者有困境：这种语言更加表达，它越难以证明它。但语言表现较少，越难以写入它。第一个生产验证语言是更具表现性语言的子集：ACL2是LISP的一个子集，Euclid是帕斯卡的一部分等。到目前为止，我们已经讨论过的东西，实际上是以证明真实世界的计划，这就是只是桌面赌注首先开始写作证明。

证据很难。然而，他们一直越来越好。校正助理研究人员继续添加新的启发式，定理库，预取量组件等硬件改进，以及更快的计算机意味着更快的搜索。

这些日子最多的人口证明自动化是SMT。 10非常广泛地说，SMT求解器可以将（一些）定理转向约束满足问题。这将创造性问题变成计算一个。您仍然需要将其中间问题（LEMMAS）作为定理中的步骤提供，但这比证明每个该死的事物更好。斯坦福德于1998年发布了第一个“现代”SMT Solver，Stanford有效性检查员。他们建立在2002年发布的CVC，这涉及轻微的生产使用。 11.

当Microsoft Research发布Z3时，场景发生在2006年左右。 Z3的大优势是比其他SMT更有用户友好，诚实并不是很多。 MSR在内部使用它来帮助证明Windows内核的属性，这意味着它们在UX中投入了更多比较最小的。 Z3可以说是全面的默认选择进行通用自动化证明。 CV中的许多工具现在依赖于SMT，并且默认情况下，大多数Z3都有Z3。

无障碍的SMT解决是裤子到正式验证社区的踢脚，因为它使得很多简单的证据琐碎和令人讨厌的证据。反过来，这意味着人们可以以更快递的语言开始证明东西，因为他们现在有能力解决表达式陈述的挑战。 Ironfleet项目中可以看到以下令人难以置信的进展：通过使用先进的SMT求解器和尖端验证语言，微软只能在3.7人中编写5,000行验证的DAFNY代码！这是一天四整行的炽热速度。 12.

现在将是一个好时刻退后一步并问“什么是点？”我们试图证明一些程序符合某些规范。正确性是一个频谱。验证问题有两部分问题：如何客观地“正确”您的程序是，以及您严格验证了正确性。显然，更多的验证优于验证的更低，但验证成本时间和金钱。如果我们有多种约束来优化（性能，时间，成本等），则最优惠不一定是“完全证明正确”。那么问题变成了“我们需要的最小验证是什么”和“到达那里的成本是多少。”在大多数情况下，您可以逃避，如90％或95％或99％正确。你可能会更好地花时间让UX更好地获得最后1％的正确性。

问题，那么：“是90/95/99％正确比100％正确便宜？”答案是非常的。我们都很乐意地说，我们经过良好测试和良好类型的代码库大多是正确的Modulo在Prod中的一些修复，我们甚至一天写了四行的代码。事实上，通过略微全面的测试可以防止绝大多数分布式系统中断。这只是更全面的单元测试，无论如说都没有模糊，基于物业的测试或模型测试。您可以非常遥远，并且在不需要进行全面证明的情况下更简单的技巧。

如果类型的遗嘱没有让你验证怎么办？比99％到100％的90％〜99％更容易得多。如前所述，洁净室是涉及全面文档，仔细流量分析和广泛的代码审查的开发人员实践。没有证据，没有正式验证，甚至没有任何单位测试。但正常完成，洁净室在生产中将缺陷密度降低至少于1个错误/ kloc。 13个使用它的团队具有比不使用它的团队相同或更短的交货时间 - 一天肯定超过4行。洁净室本身只是坐在主流软件实践和代码验证之间的许多高保证技术之一。您不需要完整的代码验证来编写良好的软件甚至写入近乎完美的软件。有必要的情况，但对于大多数行业而言，这是浪费金钱。

但是，这并不意味着整体的正式方法是不经济的。许多上述高保证技术依赖于写作代码规范，您不正式证明。至于验证，有两种常见的方式在行业中受益。首先是验证设计而不是代码，我们将在下一节中介绍。第二个是部分代码验证，我们现在将覆盖。

在日常编程中进行全面验证真的太贵了。部分验证怎么样？我仍然可以从证明我的代码的某些部分的一些属性。而不是证明我的排序函数总是排序，而是至少证明它不会永远循环，而且从未写出过界。你仍然可以得到很多好处。例如，甚至写作关于C程序的基本证明是减少大量未定义行为的重要方法。

这里的限制是可用性的。大多数语言都设计用于完全验证或无验证。在前一个案例中，你以更具表现力的语言缺少了很多好的功能，在后一种情况下，你需要一种方法来证明在概念上的语言中的东西。因此，大多数关于部分验证的研究侧重于几种高优先级语言，如C和Java。您还看到很多人使用受限制的语言子集。例如，Spark是ADA的受限子集，因此您可以在Spark中编写关键的内容，并将其与较少关键的ADA代码互操作。但是大多数语言都是漂亮的利基。

更常见的是，人们将特定类型的验证纳入语言的核心结构。生产类型系统是一种常见形式：你可能不知道尾巴总是返回尾巴，但至少你知道它有[a] - ＆gt; [一种]。您还有像Rust这样的案例，证明了内存安全和小马，证明了异常安全。这些与Spark和Frama-C略有不同，因为您只能进行部分验证，而不是一些部分和一些完整的验证。他们还倾向于通过编程语言专家通过正式的方法专家，两条学科有很多重叠但不相同。这可能是为什么Rust和Haskell这样的语言实际上是可用的。

到目前为止，我们只讨论了代码验证。 不过，正式方法还有另一面，这是一步一步抽象，并验证设计本身。 这足以让它与正式规范的代名词：如果有人说他们做正式规范，他们可能意味着他们指定和验证设计。 正如我们所谈论的，证明每一行代码是真实的 ......