证据应自行修复

弗兰克·鲍姆（L. Frank Baum）在1900年出版的《绿野仙踪》中讲述了一个会引起任何软件工程师共鸣的故事。一名名叫尼克·克珀（Nick Chopper）的wood夫遭受了一系列的工作场所事故。反过来，他的手臂，腿部，身体，甚至他的头部都被金属假肢代替。最终，剩下的是一个完全不同的锡制男人。

像鲍姆（Baum）的《锡曼》（Tin Man）一样，所有软件项目都经过修复和重新配置，并且一个项目可以按度数转换为完全不同于其起点的项目。正如软件工程师早就知道的那样，这种代码和规范的转变是常态。研究表明，维护消耗了大型项目1中的大部分资源，许多系统建立在以前项目的基础上。

近年来，许多公司已开始使用形式证明来为软件提供保证。例如，AWS现在正式验证其s2n库的重要部分，该库为Amazon.com，Alexa等提供了加密安全性。证明用于Facebook，Google，Intel，Apple和其他公司的保证。对于这些公司，证明工程就是软件工程。随着软件的发展，该软件的证明也必须以实物形式发展。

这些公司成功的关键方法是证明工具与持续集成（CI）开发环境之间的紧密结合。证明与代码之间的这种联系意味着可以在几秒钟内重新检查对代码的编辑，以便在软件更改时重新建立对软件的保证。但是，经验表明这种联系是脆弱的。如果代码更改很小，自动化工具通常可以重新建立证明。但是，如果将代码重组到一定程度之外，即使软件不包含任何缺陷，证明工具也通常无法重新建立正确性证明。取而代之的是，证明的内部支架必须由正式的方法专家手动重建。因此，与常规软件工程师一起工作的嵌入式证明专家将维护和维护证明。

这种方法无法扩展，因此，证据修复是可伸缩性问题。如果证据需要专家定期修理，则对证据的部署范围有固有的限制。形式方法专家供不应求，手动重建证据所需的时间和成本相当可观。在可预见的将来，构建正式的证明将继续需要人类的专业知识，但是我们应该将维护证明的努力与维护软件的努力相提并论。如果我们要达到一个证明是软件工程的常规组成部分的世界，那么适度的代码更改应会导致适度（自动）的证据修复。

我们有理由认为这样的证据修复是很容易的。与其尝试从无到有综合一个完整的证明（众所周知的难题，这是非常困难的），不如从一个相当相似的软件的正确证明开始。我们将尝试在已知邻域内进行证明重建。

本地维修搜索。证明中的许多属性仅适用于特定代码段，这意味着代码更改可能只会使一小部分证明无效。证明工具通常不考虑这种局部性，而是对所有代码执行可能的指数分析。同样，当证明失败时，当前的证明工具不能很好地在程序中定位失败源。在许多情况下，将有可能使证明工具适应本地搜索现有证明的修复。当证明需要维修时，该工具将识别受影响的代码和证明的最小片段，然后搜索本地修正以重新建立保证。

耐变化的证明。形式上的证明代表两种属性：断言正确行为所必需的基本属性，以及反映代码结构的偶然属性。当前最新的证明将这些问题混合在一起，并且面对代码的更改变得僵化。应设计校样以减少基本特​​性和偶然性之间的耦合。当证明表达了这样的区别时，在证明本身的结构中确定修复机会将更为可行。

在证明之间转移学习。证明与程序一样，证明也很多样化，但是维修通常遵循一小组模式。当前证明工具仅对当前代码进行操作，而与其他任何模式无关。大代码的新研究领域已经确定了通过观察代码使用模式和相应属性，将机器学习应用于代码更新的方法。在这种模式再次出现的地方，即使在完全不同的应用程序中，证明工具也将获得有关试图影响证明修复的技术的指导（类似于人类的洞察力）。从其他用途中学习会产生一个良性循环，成功的证据修复会为推动学习的示例增添色彩。

可以理解的维修。有些维修可以自动进行，但有些维修甚至需要更改本地代码，也需要人工输入。当前，证明工具需要正式的方法专业知识。我们认为，有可能创建一条途径，使直观地了解其代码意图的软件开发人员可以与证明修复工具进行交互。工具应以对软件开发人员有意义的方式提出可能的维修建议，包括对总体保证结果的变更后果的说明。这些工具可能会尽可能地证明无法修复证明，并建议可能的程序修复。

现在，越来越多的实际软件项目具有随附的证明。其中一些证明已经集成到软件工程管道中。这既是证明工程作为一个领域的风险也是机会。不管从证明中获得的保证收益如何，如果它们无法保持，它们将很快被搁置。我们必须迅速开发可以应对变化的技术，这在实际软件中是无处不在的。

尽管如此，仍有理由感到乐观。自动化证明修复的研究很少，并且（如上所述），有几种可能的成功途径。当前许多商业证明都是开源的，完整的变更日志存储在其存储库中。这代表了一组丰富的测试数据，通过这些数据我们可以完善我们的想法。现在该进行雄心勃勃的研究来解决这个问题的时候了，我们才刚刚开始。