在软件工程堆栈交易所，我看到了一个问题：“什么阻止了形式方法的广泛采用？” 该问题因偏见而被关闭，大多数答案是诸如“太贵了！！”之类的评论。或“网站不是飞机！” 在某种程度上，这是对的，但并不能解释太多。我写这篇文章是为了更全面地介绍形式方法（FM）的历史情况，为何不实际使用它们以及我们为纠正这种情况所做的工作。

在开始之前，您需要制定一些条件。实际上，没有太多的正式方法：只有几个小组。这意味着不同的组使用不同的术语。广义上讲，有两种形式化方法： 形式化规范研究精确，明确的规范的编写， 形式化验证研究证明方法。这包括代码和抽象系统。我们不仅对代码和系统使用不同的术语，而且我们经常使用不同的工具对其进行验证。更让人困惑的是，如果有人说他正在创建一个正式的规范，这通常意味着设计验证。如果有人说他正在进行形式验证，则通常指代代码验证。

为了清楚起见，我们将代码验证验证 （CV）和设计验证 （DV）划分为类似的内容，并将规范分为CS和DS。这样的术语在广泛的FM社区中并不常用。让我们从CS和CV开始，然后再转到DS和DV。

此外，仅检查规范子集的部分验证或完全验证是可能的。这可能是指控证据“系统永不崩溃且不接受错误的密码”或“如果您输错了三次密码而导致系统永不崩溃并锁定帐户”之间的区别。基本上，我们将假设我们正在进行全面检查。

您还应该阐明我们正在形式化的软件的类型。大多数人隐含地识别出高度可靠的程序，例如医疗设备和飞机。人们认为形式化方法已被广泛使用，但其余方法则不需要它们。这太乐观了 ：大多数高度可靠的软件都不使用正式方法。相反，我们将专注于“常规”软件。

最后，免责声明：我不是专业的历史学家，尽管我试图仔细地验证信息，但是文章中可能存在错误。此外，我专门研究正式的规范（DS和DV），因此在谈论代码验证时有更多的出错机会。如果您看到，写信给我，我会纠正的（还有一件事：我从TLA +和Alloy的研讨会上赚钱，因此我对这些语言非常有偏见;我力求尽可能客观，但您明白了：偏见就是偏见）。

正式编程

获取规格

在证明代码的正确性之前，您需要获得真理的标准。这意味着对代码应该执行的操作进行了一些规范。我们必须确定结果是否符合规范。仅说列表是“已排序”是不够的：我们不知道我们正在排序什么，我们使用什么标准，甚至是“排序”的含义。相反，我们可以说：“整数列表l对于任意两个索引i和j 以升序排列 ，如果i < j ，则l[i] <= l[j] 。”

代码规范分为三种主要类型：

首先是编写与代码无关的语句。我们编写排序函数，并在一个单独的文件中编写定理“这将返回排序列表”。这是最古老的规范形式，但是Isabelle和ACL2仍然可以这种方式工作（专门发明了ML来帮助编写此类规范）。
第二种以前置条件和后置条件，语句和不变式的形式在代码中实现规范。您可以在函数中添加一个后置条件，即“返回值是一个有序列表”。基于索赔的规范最初被正式化为Hoar的逻辑。它们最初是在1970年代初期以Euclid编程语言出现的（尚不清楚是谁首先开始使用它们的：Euclid或SPV ，但据我所知，Euclid是在之前被引入公众的）。这种样式也称为合同编程 -现代工业中最流行的验证形式（此处合同用作代码规范）。
最后，还有类型系统。通过Curry-Howard对应关系，任何数学定理或证明都可以编码为从属类型。我们将定义排序列表类型，并为函数声明类型[Int] -> Sorted [Int] 。

在“ 让我们证明左键盘”上，您可以看到它的外观。 HOL4和Isabelle是“独立定理”的规范的好例子，SPARK和Dafny是“嵌套语句”的规范，而Coq和Agda是“依赖类型”。

如果仔细观察，会将这三种形式的代码规范与自动验证的三个主要领域进行比较：测试，合同和类型。这不是巧合。正确性范围很广，形式验证是其极端情况之一。随着验证的严格性（和工作量）的减少，我们得到的检查变得更加简单和狭窄，无论是限制正在研究的状态空间，使用较弱的类型还是在运行时强制检查。然后，任何完整规范的方法都将变成部分规范的方法，反之亦然：许多人认为Cleanroom是一种形式验证的技术，其中代码审查远远超出了人员的能力。

哪些规格正确？

验证验证代码是否符合规范。问题出现了：我们如何知道我们有正确的规范？找到正确的规范是形式化方法中的最大问题之一。这也是对他们的主要反对意见之一。但是，这里的怀疑者并不意味着正式专家会想到什么。

当局外人问“您如何获得正确的规格？”时，他们通常会考虑验证，即不符合客户要求的规格。如果您正式证明您的代码对列表进行了排序，而客户实际上想要Uber来买汤（tm），那么您就花了很多时间。就像，只有快速迭代和较短的反馈循环才能确认您的要求。

的确，代码验证不会验证它。但是这种说法有两个问题。第一个是应用形式方法的阶段只是被推迟了，但是并没有完全消失。经过所有这些快速迭代之后，您可能已经对客户的需求有了一个想法。然后开始进行代码验证。其次，尽管我们不知道客户到底想要什么，但我们可以假设他绝对不想要什么。例如，使软件意外崩溃。他们不需要安全漏洞。每个人都对此表示赞同：最后，没有人说您需要在迭代过程中跳过单元测试。因此，至少要确保您的版本控制系统不会删除随机用户数据（注意：不要以为我很烦或类似的事情）。

找到正确的规范的问题更为根本： 我们通常不知道在那写什么 。我们以人类而非数学的角度考虑我们的要求。如果我说：“该程序应该将树木与鸟类区分开来”，那是什么意思呢？我可以通过显示一堆树木和鸟类的图片来向一个人解释，但这只是具体的例子，而不是对该概念的描述。实际上，为了将其转化为正式规范，有必要对人类概念进行形式化，这是一个严重的问题。

不要误会我的意思。可以在此处定义相关的规范，专家会一直这样做。但是编写适当的规范是需要开发的技能以及编程技能。这就是为什么通过将我们想要的东西清楚地映射为我们可以表达的东西来解释最近在代码验证方面取得的许多成功的原因。例如， CompCert是经过正式验证的C编译器，其规范为：“避免编译错误”。

但这与验证无关。有了规范后，您仍然需要证明代码与之匹配。

规格证明

有史以来第一个代码验证工具是Dijkstra风格的“思考为什么如此”的方法，该方法主要用于ALGOL。例如，我可以通过插入方法“证明”排序的正确性，如下所示：

基本选项 ：如果将一个元素添加到空列表中，它将是唯一元素，因此将对其进行排序。
如果我们有一个包含k个元素的排序列表并添加一个元素，那么我们插入该元素，以便它在所有较小的数字之后，在所有较大的数字之前。这意味着列表仍在排序。
通过归纳，插入排序将对整个列表进行排序。

显然，实际上，证明看起来会更加严格，但这是一个普遍的想法。 Dijkstra和其他人使用这种样式来证明许多算法的正确性，包括许多并发基础。这也是Knuth的单词所关联的样式：“当心代码中的错误；我只证明它是正确的，但没有启动它。” 您可以轻松破坏数学证明，以至没人注意到。根据一些估计，大约20％的已发表数学证据包含错误。彼得·古特曼（Peter Guttmann）着有一篇很好的文章，证明了一个荒谬程序的健康性，如果运行这些代码，大量“经过测试”的代码将立即掉落。

同时，我们研究了自动证明数学定理的方法。 证明定理的第一个程序于1967年发布。在1970年代初，此类程序开始用于测试Pascal代码，并在20年代中期出现了特殊的形式语言。程序员制定代码的某些属性，然后创建可验证的证据证明代码具有这些属性。证明定理的第一个程序只是帮助人们验证了证明，而更复杂的工具可以独立证明定理的一部分。

这导致以下问题。

证据很难获得

举证很难，而且是非常讨厌的工作。很难退出编程并进入马戏团。令人惊讶的是，正式的代码证明通常比大多数数学家编写的证明都要严格！数学是一项非常有创意的活动，其中定理的答案只有在您显示出该定理之后才有效。形式主义和计算机的创造力差强人意。

以我们应用归纳法的相同插入排序示例为例。任何数学家都将立即了解什么是归纳，它一般如何工作以及在这种情况下它如何工作。但是在证明定理的程序中，所有事情都必须严格地形式化。通过矛盾的证明，通过对立的证明等也是如此。此外，所有假设都必须形式化，即使那些大多数数学家不担心证明的假设也是如此。例如， a + (b + c) = (a + b) + c 。先验定理检查程序不知道这是真的。您要么必须证明（困难），要么根据加法的关联法则将其声明为真实（危险），或者从已经能够证明它的人那里购买定理库（昂贵）。早期的定理证明程序在内置证明策略和相关定理库的数量上竞争激烈。最先发布的SPADE程序之一就是将完整的算术库作为主要优点。

接下来，您需要获取证明本身。您可以将其委托给程序，也可以自己编写。通常，自动确定证据是不可决定的。对于命题逻辑或类型检查HM等极其狭窄的情况，它“仅”是NP完整的。实际上，我们自己编写了大部分证据，然后计算机会检查其正确性。这意味着您需要了解以下内容：

数学
计算机科学；
您工作的领域：编译器，硬件等；
您的计划和专业的细微差别；
程序的细微差别可以证明您使用的定理，而定理本身就是一个完整的专业。

更坏的，计算机专用的操纵杆插入了车轮。还记得我曾说过假设一个相加法则是危险的吗？某些语言不符合它。例如，在C ++ INT_MAX. ((-1) + INT_MAX) + 1 INT_MAX. ((-1) + INT_MAX) + 1是INT_MAX. -1 + (INT_MAX + 1) INT_MAX. -1 + (INT_MAX + 1) ，这是不可检测的。假设在C ++中有关联加法，则您的证明将不正确，并且代码将被破坏。您必须避免使用此语句，或者证明特定片段永远不会发生溢出。

您可以说不定加法是一个错误，但是您需要使用不相关整数的语言。但是大多数语言都有干扰证据的特定功能。采取以下代码：

 a = true; b = false; f(a); assert a;

总是这样吗？不是事实也许f会改变a 。也许它将改变并行流。也许b赋予了别名a ，所以对其进行更改也会改变a （注意：别名使撰写约翰C. Reynolds必须创建全新的分离逻辑来处理此问题的证据变得如此困难）。如果使用您的语言可能会发生这种情况，那么您应该明确证明在这里不会发生这种情况。干净的代码将在这里有所帮助，在另一种情况下，它可能会破坏证明，因为它迫使您使用递归和更高阶的函数。顺便说一句，它们都是编写好的功能程序的基础。什么对编程有益，对证明不利！（注意：在本教程中， Edmund Clark列出了一些难以验证的属性：“浮点数，字符串，用户定义的类型，过程，并发，通用模板，存储，库...”）。

正式验证者有一个两难选择：语言越富有表现力，证明某件事就越困难。但是，语言表达越少，用它编写的难度就越大。最早可用的正式语言是表达能力较强的语言的非常有限的子集：ACL2是Lisp的子集，Euclid是Pascal的子集，依此类推。到目前为止，我们所讨论的内容都没有真正证明真实的程序，这些只是尝试写证据。

证据很难。但是，变得越来越容易。该领域的研究人员添加了新的启发式方法，定理库，预先测试的组件等。技术进步也有帮助：计算机越快，搜索速度越快。

SMT革命

2000年代中期的创新之一是将SMT求解器包含在证明定理的程序中。广义上讲，SMT求解器可以将（一些）数学定理转化为约束合规性问题。这将创造性的任务变成了计算任务。您可能仍需要向定理中的步骤提供中间问题（引理），但这比证明自己的一切要好。第一批SMT求解器于2004年左右出现，最初是作为学术项目。几年后，微软研究院发布了现成的SMT解决方案Z3。 Z3的最大优点是，它变得比其他SMT更加方便使用，坦率地说，它几乎什么也没说。 Microsoft Research在内部使用它来帮助证明Windows内核的属性，因此它们不仅限于最小的UX。

SMT令FM界大吃一惊，因为它突然使许多简单的证据变得微不足道，并使其能够处理非常复杂的问题。因此，人们可以使用更具表现力的语言进行工作，因为现在开始解决了表现性陈述的问题。 IronFleet项目取得了令人难以置信的进步：使用最佳的SMT求解器和先进的验证语言，Microsoft在短短的3.7个人年就能编写5,000行行之有效的Dafny代码！这是一个令人难以置信的快速步伐： 每天多达四行 （请注意：先前的记录属于seL4 ，其开发人员每天都用C写两行）。

证据很难。

为什么需要这个？

现在该退后一步，问：“这有什么意义？” 我们试图证明某些程序符合某些规范。正确性是一个范围。验证包括两个部分：客观上“正确”程序的方式以及检查准确性的认真程度。显然，验证越多越好，但是验证值得时间和金钱。如果我们有几个限制（性能，上市时间，成本等），则完全验证不一定是最佳选择。随之而来的问题是，我们需要的最低支票是多少，花费多少。例如，在大多数情况下，对于您来说90％或95％或99％的正确性就足够了。也许您应该花时间改善界面，而不是检查剩余的1％？

然后是一个问题：“一张90/95/99％的支票比100％便宜吗？” 答案是肯定的。很高兴地说，我们经过测试和键入良好的代码基础基本上是正确的，除了在生产中进行了一些更正外，我们甚至每天编写四行以上的代码。实际上，可以通过稍微更全面的测试来防止分布式系统中的绝大多数故障。它只是测试的扩展，更不用说模糊测试，基于属性的测试或模型测试了。通过这些简单的技巧，您可以获得真正出色的结果，而无需获得充分的证明。

如果打字和测试没有提供足够的验证怎么办？从90％切换到99％比从99％切换到100％仍然容易得多。如前所述，Cleanroom是一种开发人员实践，包括全面的文档，全面的流程分析和大量的代码审查。没有证据，没有形式验证，甚至没有单元测试。但是组织得当的无尘室可以将缺陷的密度降低到生产中每1000行代码少于1个错误（请注意：来自“ 朝着零缺陷编程的Stavley研究”中的数字>，但始终持怀疑态度，并检查其来源）。对Cleanroom进行编程并不会减慢开发速度，并且运行速度肯定比每天4行快。 Cleanroom本身只是许多高度可靠的软件开发方法之一，介于正常开发和代码验证之间。您不需要完整的验证就可以编写优秀的软件甚至几乎是完美的软件。有时需要它，但是对于大多数行业来说，这是浪费金钱。

但是，这并不意味着正式的方法通常是不经济的。前面提到的许多高度可靠的方法都是基于您未正式证明的代码规范编写的。在验证方面，行业可以从两种常见的方式中受益。首先，设计验证而不是代码，我们将在后面讨论。其次，对代码进行部分验证，我们现在将考虑。

部分代码验证

对于日常任务，进行全面检查太昂贵了。那部分呢？毕竟，您可以从单个代码片段的某些属性证明中受益。与其证明我的函数总是对数字进行正确排序，我至少可以证明它不会永远循环并且永远不会超出范围。这也是非常有用的信息。因此，即使是最简单的C程序证据，也是消除大部分未定义行为的好方法。

问题是可访问性 。大多数语言都是为完全验证而设计的，或者根本不支持它。在第一种情况下，您会错过来自更具表现力的语言的许多出色功能，而在第二种情况下，您需要一种方法来证明一种对概念本身有害的语言。因此，大多数有关部分验证的研究都集中在几种优先级较高的语言上，例如C和Java。许多只使用有限的语言子集。例如，SPARK是Ada的有限子集，因此您可以编写重要的SPARK代码并与不太重要的Ada代码进行交互。但是这些语言中的大多数都是相当小众的。

通常，某些类型的验证会嵌入语言的基本结构中。生产中使用的分类系统是一个常见的变体：您可能不知道tail总是返回tail，但是您确切知道其类型是[a] -> [a]。还有一些示例，例如Rust具有可靠的内存安全性，Pony具有安全性例外证明。它们与SPARK和Frama-C略有不同，它们只能执行部分检查。而且它们通常是由程序设计语言的专家开发的，而不是由形式方法的专家开发的：这两个学科之间有很多共同点，但是它们并不完全相同。也许这就是为什么Rust和Haskell之类的语言真正适合实际使用的原因。

设计规格

到目前为止，我们仅讨论了代码验证。但是，形式化方法还有另一面，它更加抽象，可以验证设计本身，项目的体系结构。这种分析是如此深入，以至于它是正式规范的同义词：如果有人说他正在履行正式规范，则很可能意味着他定义并验证了设计。

正如我们已经说过的，要证明所有代码行都是非常非常困难的。但是生产中出现的许多问题不是由于代码，而是由于系统组件的交互。例如，如果我们忽略实现细节，则认为该系统能够识别鸟类是理所当然的，那么对于我们来说，分析树木和鸟类作为高级模块如何适合总体设计将变得更加容易。以这种规模，描述您无法实现的事情变得更加容易，例如运行时环境，人机交互或无情的时间流。在这种规模上，我们使用通用系统而非代码行来形式化我们的意图。这更接近于人类的水平，在人类的水平上项目和需求可能比在代码水平上更加模糊。

例如，让我们采用一个粗略规范的过程“如果调用它，它将进行系统调用以将数据保存到存储库并处理系统错误”。属性很难验证，但是很清楚如何做到这一点。数据是否正确序列化？是否由于输入错误而违反了我们的保证？我们是否正在处理系统调用失败的所有可能方式？现在，将高级日志记录系统与“所有消息均已记录”的规范进行比较，并回答以下问题：

是否记录了所有消息或进入系统的所有消息？消息只记录一次还是保证一次？
消息如何发送？现在该了吗？频道只传送一次吗？交货一切都还好吗？
? , ? «» , ?
, ? ?
? « » ?
GDPR?
.

没有正式的设计，就很难表达系统的真正必要要求。如果您无法表达它们，那么您将不知道设计是否真正满足要求或看起来像它们，但这可能会导致不可预测的后果。通过更正式地表达意图和设计，我们可以轻松地验证我们实际上正在开发所需的东西。

正如我们使用编程语言来表示代码一样，我们也使用规范语言来表示项目。规范语言通常面向设计规范而非代码规范，尽管两种情况都可以使用某些语言（注意：将设计规范与代码规范匹配的过程称为优化）将来，我将称呼规范语言设计语言（DL）以最大程度地减少混乱（再次，这不是通用术语；大多数人使用“规范语言”，但我想清楚地区分代码规范和设计规范）。

第一个完整的DL大概是1972年左右的VDM。从那时起，我们已经看到了各种各样的不同规范语言。DL空间比代码验证语言（CVL）更加多样化和分散。粗略地说，人们发明了DL作为达到目的的手段，并发明了CVL作为目标。由于它们受到特定问题区域的强烈影响，因此DL实现了各种想法和语义。这是一些第一个DL的非常非常简要的概述：

语言能力	造型区	均值
ž	业务需求	关系代数
Promela		CSP
SDL		-

由于DL通常是为解决特定问题而创建的，因此大多数DL至少具有两个或三个实际应用程序。通常，结果是非常积极的。从业人员说，DL提供了对问题的理解并使查找解决方案变得更加容易。长期以来，主要的支持者是Praxis（现为Altran），他应用了“按设计修复”（Z构造和SPARK代码的组合）来创建关键的安全系统。规格可以节省时间和金钱，因为在项目后期您不会发现设计错误。

帕梅拉·扎夫（Pamela Zave）对Alloy进行了试验，发现了Chord中的一个基本错误，Chord是主要的分布式哈希表之一。 AWS开始发现35步严重错误通过编写TLA +规范。以我的经验，当人们尝试编写规范时，他们很快会成为该行业的忠实拥护者。

但是形式方法的拥护者和外部人士完全不同地评估书写规范的价值。对于粉丝来说，最大的好处就是设计过程本身可以使您了解自己在写什么。当您需要正式表达系统在做什么时，许多隐式错误突然变得很明显。局外人根本无法理解这一点。如果要给某人尝试DL，则该人应该有一种方法可以验证设计是否确实具有他想要的属性。

幸运的是，这对于许多说明者也非常重要，因此设计验证是一个很大的研究领域。

模型检查

与代码一样，我们可以通过编写定理来验证设计。幸运的是，我们还有另外一个技巧：您可以使用模型检查器程序。无需收集证明设计正确的证据，我们只是简单地暴力破解可能状态的空间，然后查看其中是否存在错误的状态。如果我们什么都没找到，那么一切都很好（请注意：模型验证程序也用于验证代码，例如JMBC，但模型验证比代码验证更常用于设计验证中）。

模型验证具有许多优点。首先，无需编写证据，从而节省了大量时间和精力。其次，无需学习写证据，因此进入门槛要低得多。第三，如果设计被破坏，检查模型将给出一个明确的反例。这样可以更轻松地修复错误，尤其是如果花费35个步骤来重现该错误。尝试自己找到它。

有两个缺点。首先，这些工具没有那么强大。特别是，您可能会遇到无限（无边界）由具有无限多个不同状态的模型组成。例如，您定义一个消息队列处理程序：它通常与十个消息的列表一起使用。但是，如果您需要在任何列表中相信它，那么……有无数个状态，因此该模型具有无数个状态。对于这种情况，大多数模型验证工具都有不同的技巧，例如定义等价类或对称类，但是每种情况都是不同的。

另一个大的缺点- 在状态空间爆炸（状态空间爆炸）。假设您有三个过程，每个过程都包含四个连续的步骤，并且它们可以以任何方式替换这些步骤。如果它们不影响彼此的行为，那么事实证明(4*3)! / (4!)^3 = 34 650可能的处决（行为）。如果每个过程都具有五个初始状态之一，那么行为的总数将增加到4,300,000，并且检查模型应确保它们都表现良好。前提是它们不互相影响！如果他们开始这样做，状态空间将增长得更快。组合爆炸被认为是测试模型的主要问题，要解决这个问题，还有很多工作要做。

但与此同时，还有另一种应对状态空间爆炸的方法：向其投入更多设备。检查模型的最大问题是“仅”性能问题，我们很好地解决了性能问题。大多数（但不是全部）模型检查很容易并行化。优化模型并使用小参数对其进行测试后，您可以部署AWS集群并使用大参数运行它。

实际上，许多限定词使用模型验证，然后根据需要切换到程序以证明定理（注意：请记住，“许多限定词”大约是10个）。甚至更多的规范编译器开始测试模型，并且当模型达到其功能极限时，他们会切换到强度较低的验证形式。

设计规范问题

因此，设计验证比代码验证更简单，更快捷，并且已经展示出许多令人印象深刻的成功。那为什么人们不使用它呢？ DV的问题更加隐蔽。代码验证是一个技术问题，而设计验证是一个社会问题：人们只是看不到重点。

这主要是由于设计不是代码这一事实。在大多数DL中，没有自动的代码创建方法，也没有方法将现有的代码与设计进行对照（注意：从规范生成代码称为综合 ;有关方向，请参见Nadya Polikarpova的著作;证明代码符合规范（或规范对应）其他规格）称为澄清：双向都在进行积极的研究）。

程序员倾向于不信任不是代码或没有被迫与代码同步的软件工件。出于同样的原因，文档，注释，图表，Wiki和提交也经常被忽略。

程序员似乎根本不相信规范有任何用处。以我的经验，他们认为当前的工具（伪代码，图表，TDD）足以进行正确的设计。我不知道这种观点有多广泛，除了普遍的保守主义之外，我无法用其他任何解释。

但是，确切地说，每个这样的方法论社区都有这样的抱怨，我知道：TDD支持者抱怨程序员不想尝试TDD，Haskell粉丝抱怨程序员不考虑静态类型，等等。

我听到过这样的论点，即敏捷不接受预先设计的设计，因此没有人愿意制定正式的规范。也许吧但是我遇到的许多人都拒绝敏捷和FM。另一个论点是，历史上的形式方法不断地被重新评估，并且没有实现所承诺的。这也是可能的，但是大多数人甚至都没有听说过正式的方法，甚至还没有听说过他们的历史。

即使人们认识到了好处，也很难使他们担心自己还没有做什么。

总结

验证代码是一项艰巨的任务。尽管定理证明程序和SMT求解器变得越来越复杂，但越来越多的人参与其中。但是，在可预见的将来，可能仍然会有很多专家。

设计验证要简单得多，但是其使用需要克服文化障碍。我认为情况可以改变。二十年前，自动化测试和代码审查是一个颇具异国情调和利基的话题，但最终成为主流。合同编程再次是利基市场，并且仍然如此。

我希望本文能更好地解释为什么很少使用形式化方法。至少与通常的论点“网络不是平面”相比，这是一个更好的解释。如果发现任何明显的错误，请随时尖叫。

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