自动推理作为一个讨厌的孩子

这个博客是有关Galois，Supranational，以太坊基金会和协议实验室之间的联合项目的系列文章的第二部分，该项目验证了最先进的签名库。您可以在这里找到第一篇文章。这是我的恶作剧和对我们要实现的目标的概述。

它已经发生了。开发团队与证明工具进行了深入的对话，他们正在付出很多努力。关于这些对话进行方式的最好描述是“就像和孩子说话一样”。

在我太深入地解释工作上的困难之前，让我们先花时间描述一下我们到底要实现什么，以及什么是程序验证的证明工具（例如SAW工具）。像SAW这样的程序证明工具将带走一个程序，以及对该程序应执行的操作的描述，并告诉您两者是否一致。在此过程中，该工具可能会突出显示没有足够信息来成功完成此操作的地方，甚至是程序存在错误的地方。

基本上，使用程序证明工具就像和一个非常好奇且执着的孩子说话。实际上，让那两个孩子。每次您告诉他们一些事情时，他们都会听着，点点头，然后问：“为什么？”。然后，您回答问题一会儿，不久之后，您坐在杂货店停车场，两个戴着面具的英雄正凝视着您：

令人毛骨悚然，我知道。如果所有这些听起来令人沮丧，那么您是对的-可以！但是，就像向两个好奇的蜘蛛侠讲解《克隆传奇》一样，该工具最终对您的理解远胜于弥补。让我们举一个简单的例子，确切地证明证明者像孩子一样的能力，以及为什么最终，这种幼稚的好奇心实际上是一件很棒的事情。

SAW帮助我们证明程序是正确的。我们称编写程序正确性证明的过程为正式验证。

SAW要做的第一件事是为我们提供一种精确的语言来描述程序应该做什么。我们称其为规范。 SAW中的规范（以及其他验证工具的负载）采用以下形式：

如果您有一个称为M的对象和变量的集合（通常被描述为C中的内存布局）

看起来很简单吧？这正是我们所有人对所编写程序的看法。特别是，我们“跳过”了功能操作的细节，转而考虑了如何调用它们以及完成后会发生什么。它是抽象的。我真的很喜欢抽象。我也喜欢抽象。我想我对抽象有积极的感觉。

验证工具思考诸如M之类的内存布局和诸如P之类的参数的方式上有一个关键差异。当我们运行一个函数时，我们的内存布局看起来像这样（相对于1索引和在存储单元0上放置一个值之间的张力） ：

我们只是将变量卡在那里。就在内存中！每个变量代表任何数字。存储器单元x可能包含17、1729或1270亿个，并且此存储器布局表示所有这些可能性。这意味着我们可以使用SAW来理解数以百万计的不同可能的内存布局，并且全部使用相同的规范。

程序F只是正常功能。假设它是一个（伪代码）函数，可以递增数组中的每个值。

void inc_all（int [] r，size s）{for（int i = 0; i＆lt; size; i ++）{r [i] = r [i] + 1}}

是的，我编写了C伪代码。它使您对这些天的真实情况有了一些真正的了解。我确实省略了分号来向我的Haskell和Python伙伴表示敬意。

我们还需要参数来调用此函数。假设r从存储单元1开始，大小为5（因此结束于5）。功能完成后，我们期望什么？我们称该内存布局为M’

在那里，有了inc_all的完整规范（当以特定大小和特定的内存布局调用时）。如果我们知道原始内存布局中的x值，那么无论选择什么数字，我们都知道结果中的x值。

证明工具向证明工程师提出的第一个问题是您要我证明什么？这个问题的答案以规范和程序的形式出现。在此阶段发现错误并不罕见。只是试图解释程序应该做什么的行为很可能会发现程序中的某些错误（如果存在）。

一旦描述了该功能应该做什么，我们如何使用SAW来确定它是否确实起作用？这是真正的问题开始的地方，其中有很多！对于程序inc_all SAW将询问所有以下问题：

证明工具获得的M’是否与规范中为每个记忆值建议的M匹配？

2行程序有很多问题，但是每个问题都针对程序中可能出错的特定问题。事实证明，在没有分号的情况下，C可能会出错。毕竟，C是一门强大的语言，强大的能力伴随着巨大的责任。

好消息是，证明自动化使证明工具无需程序员的任何帮助即可回答许多（或全部）这些问题！实际上，这是SAW所做的大部分工作-提出问题，然后回答问题本身。不幸的是，蜘蛛侠不会这么做。

程序证明工具的最好之处在于，无论多么细致，它们都会始终询问每个问题，并且除非他们完全相信答案，否则它们不会证明程序是正确的。这种细致性是我们经常称为健全性的概念。如果您想让我发狂，请问我我对这句话的感觉如何。我什至不知道为什么要提出它。可能不是因为我希望您在Twitter上与我联系（我是@ n1nj4）。

在这种情况下，我们的证明自动化可以回答有关程序的所有这些问题，这意味着证明将成功。在其他情况下，代码或规范都不对，我们需要弄清楚怎么做。同样，许多错误被淘汰了，仅仅是因为我们的证明工程师知道该工具会询问很多代码问题。它不会留下任何草率或挥手的错误。证明工具会根据规范减少大多数代码的正确性或不正确性，并且在完全确信之前不会认为证明是完整的。

在这样的框架之上学习如何思考程序，从根本上改变了证明工程师思考程序的方式。实际上，我们的技术负责人Andrei Stefanecsu通常会先使用SAW分析新代码，而不是手动检查代码。这是因为SAW为他提供了一个有用的框架，可用于思考代码的重要属性而不是表面结构。

如果您花了很多时间进行编程，则可能已被程序推理工具转变了思维方式。从类型系统到功能的所有因素都会影响我们对程序的思考，甚至​​在不可用时，我们也会使用它们来指导我们的编程。问问从强类型语言过渡到动态类型语言的任何程序员，或者已回到使用C语言的Rust程序员。问问：像SAW之类的程序证明工具都是这种扩展。

特别是，程序证明工具的类似于孩子的方面会改变工程师对程序的思考方式。养成永远不放弃任何东西的心态，因为您知道该工具会召唤您，这将使您成为更好的程序员，就像孩子通过问您为什么需要8盒Cookie一样，使您成为更好的人到杂货店。

在我们如何指定程序和开发证明的细节中，所有这些都变得更加具体。在本系列的下一篇文章中，我将向您展示一些关于我们最严格的规范的示例，并将其详细分解。