本文简要介绍我学到的一个技巧，它能帮助我更快、更准确地编写代码。虽然称之为“技巧”，但实际上，随着我职业生涯的深入，我已经不知不觉地开始运用它了。

当你处理一些棘手的问题时，不妨在脑海中勾勒出代码能够实现预期功能的证明。这听起来很简单，但做起来却并不容易：要在不中断思路的情况下“实时”做到这一点，需要大量的练习。但一旦你熟练掌握了这项技巧，你会发现很多时候你的代码只需一次或两次就能成功运行。这感觉有点像魔法。

有很多方法可以实现这一点，我不想规定得太死板。我只列举一些我经常即兴思考的问题的例子，以便你了解大致情况。

单调性

在验证代码的正确性时，需要注意哪些部分是单调的。

你可能在数学中接触过单调函数。通俗地说，它们是不会“倒退”的函数——也就是说，递增的单调函数只能递增或保持不变，而递减的单调函数只能递减或保持不变（它们也分别被称为非递减函数和非递增函数）。

单调代码的概念比单调函数的概念稍微模糊一些，但它同样表达了只能沿一个方向进行的过程。例如，检查点机制就是单调性的一个很好的例子。假设你有一个脚本需要按顺序执行多个任务，你可以在磁盘上保留一些状态信息，记录目前为止已经完成的任务数量。如果出现错误导致脚本崩溃，它可以检查磁盘上的状态信息来确定执行到哪一步了，然后从尚未执行过的最早状态重新开始。

检查点机制意味着脚本中的“当前步骤”指针只能向前移动，因为脚本无法回溯并重新运行已经执行过的步骤。从这个意义上讲，脚本的执行是单调递增的，显然，如果脚本最终成功完成，那么每个步骤都恰好执行了一次。

保留这种活动日志的想法很简单，但它却经常出现在一些意想不到的地方，例如日志文件系统和数据库预写式日志。另一个更复杂的数据库示例是 LSM 树。LSM 树在某些数据库中用于在内存和磁盘上存储行，而且大多数情况下，它们都是纯粹的累加式结构。简单来说，LSM 树会记录所有插入、删除和更新操作，并在读取行时扫描日志以重建该行的相应值。过时的操作会定期被丢弃，以节省空间，这个过程称为压缩。LSM 树占用的空间只会增长（压缩期间除外，压缩期间它只会缩小）。

您可以将其与 B 树进行比较，B 树是一种更传统的数据库结构，它会就地删除和更新行。 B 树通常需要做更多的工作来回收删除操作后释放的空间，重组数据结构以便在更新操作增加一行数据时留出空间，确保有足够的缓冲区等等。如果你愿意，可以多了解一些关于 B 树和 LSM 树的知识，看看哪一个更容易理解。

值得注意的是单调性，因为它通常可以用来排除一大类可能的结果。另一个类似的概念是不可变性（在很多方面，它与单调性类似）——当你创建一个不可变对象时，该对象就不能被修改。值只能在对象创建时赋值一次；你不能“撤销”或“撤回”这些赋值操作。这使得你可以完全忽略所有对象可能在你不知不觉中发生变化的情况。

前置条件和后置条件

前置条件和后置条件是用来指定函数行为约束的一种方式。函数的前置条件是指函数执行前假定为真的条件。这些条件可以是函数输入的条件，也可以是关于程序状态或环境的更一般性的声明。函数的后置条件是指函数执行后假定为真的条件。与前置条件一样，这些声明几乎可以包含任何内容。如果函数执行前所有前置条件都为真，而执行后所有后置条件都不为真，那么至少根据指定的约束条件，该函数的实现是不正确的。

这些概念很简单（甚至显而易见），本身并不是真正的证明技巧，但仅仅是用形式化的术语来跟踪它们是什么，就能帮助你进行推理。

（有时你可能会发现你的函数没有明确定义的前置条件和后置条件，了解这一点也很有用！）

明确后置条件尤其有助于构思单元测试。此外，添加断言来确保前置条件和后置条件为真，否则程序崩溃，也有助于防御性地进行测试。这样可以更容易地推断代码在未崩溃的情况下会如何运行——这听起来或许只是一种中性的权衡，但通常来说，代码尽早崩溃比运行异常要安全得多。

不变量

一段代码的不变式是指无论发生什么，在代码运行之前、运行期间和运行之后都必须始终为真的条件。与前置条件和后置条件一样，不变式几乎可以包含任何内容。

用不变量来思考一致性会很有帮助——在这种情况下，不变量就是“这个数据结构是一致的/有效的”，你需要证明代码在任何情况下都保持这个不变量不变。一个简单的方法是将代码分解成原子性的“步骤”，并证明每个步骤本身都保持着这个不变量不变。这样你就可以得出结论：无论执行哪些步骤或执行顺序如何，这个不变量都成立。

会计等式是历史最悠久、最著名的不变量之一，也是复式记账法的基础。会计等式简而言之就是：公司账簿上借方总额必须等于贷方总额。很容易证明，只要复式记账法操作正确，就能保持这一不变量：对于每一笔交易，贷方账户的增加（或减少）必须等于借方账户的增加（或减少）。显而易见，如果交易前借贷方平衡，那么交易后也仍然平衡。因此，这一不变量始终成立。

另一种维护特定类型不变性的方法是使用监听器或生命周期方法来确保不变性在某些关键点保持为真。这种技术常用于需要保持多个状态同步的情况——例如，C++ 使用构造函数和析构函数来确保对象所需的任何内存仅在对象实际存在时才被分配。useEffect对 React 组件也做了类似的事情。

（由于不变量必须适用于所有可能的情况，因此在进行引入的新执行路径相对较少的更改时，通常更容易进行推理。）

隔离

我一直坚信，软件开发的很多“技巧”都（或者说应该是）围绕着如何在不破坏系统稳定性的前提下修改或增强现有系统展开。在修改代码库时，了解如何证明你原本**不想改变的行为实际上没有改变，这一点至关重要。

我经常使用一种技巧来验证这一点；我不确定它是否有专门的名称，或许与其说是一种技巧，不如说是一种思维模式。我能想到的最佳描述是：每一次改动都有一个“影响范围”——对代码某一部分的改动可能需要对另一部分进行修改，以确保整个系统的一致性和正确性。而这第二次改动又可能需要对第三部分进行修改，以此类推。要确定一项改动会影响哪些行为，不会影响哪些行为，就需要识别出一些结构性的“防火墙”，这些防火墙可以阻止改动传播到某个特定点之外。这有点像是封装的概念上的对应概念。

这个想法比较抽象，所以这里举个电影《玩命直播》（Nerve）的例子：

Nerve 是一个查询引擎，它允许用户像使用单个大型 API 一样查询多个数据源。Nerve 查询管道由查询规划器和**查询执行器组成。查询规划器负责计算执行查询的具体步骤，而查询执行器则负责执行该规划。Nerve 中的查询可以包含实体字段和虚拟字段。虚拟字段本质上是派生字段——换句话说，实体字段直接从源 API 获取，而虚拟字段则是在运行时根据其他虚拟字段或实体字段计算得出的。

实体字段的处理相当简单——只需发出相应的请求，并根据需要从响应中提取数据即可。虚拟字段则稍微复杂一些，因为有时虚拟字段依赖于其他字段。我们需要确保在计算虚拟字段之前，所有先决条件都已满足。要求用户自行将这些先决条件添加到查询中，未免过于繁琐。因此，我们应该提供一种机制，在计算虚拟字段之前自动提取其依赖项。但是，这种机制应该放在哪里呢？

一个简单的办法是修改查询规划器和查询执行器，让它们理解“物料字段”的概念，并将这些字段作为依赖项提取，而不是作为查询中指定的字段。这些“依赖字段”应该保留下来，以便我们用它们来计算虚拟字段，但它们不应该包含在最终的查询结果中。我们还需要考虑其他一些设计因素——例如，我们可能需要找到方法，在提取“普通”物料字段时，也能在相同的请求中提取这些依赖字段等等。

这本质上是对查询管道的扩展：可能有点复杂，但肯定可行。不过，我们可以用个小技巧来规避这个问题，那就是先过度拉取数据，然后再进行事后清理。

在第二种方法中，我们完全不引入任何新概念。相反，在查询规划阶段，我们计算每个虚拟字段的依赖关系，并将它们添加到查询中，然后将其交给查询执行器。查询执行器并不知道它接收到的查询并非用户编写的查询；它只是像往常一样运行查询，首先提取所有物料字段，然后计算任何相关的虚拟字段（而且它永远不需要提取虚拟字段的依赖关系，因为它们总是神奇地存在！）。

查询执行完毕后，我们会得到包含比用户请求字段多得多的查询结果。因此，最后我们会添加一个清理步骤，移除所有用户查询中未包含的字段。

该方案的主要优势在于，变更完全局限于查询管道的开头和结尾的两小层——中间部分（查询引擎的“核心”）完全无需改动。特别是，查询规划器和查询执行器之间的边界就像一道“防火墙”，阻止变更扩散。这使得我们能够轻松证明，在执行无需引入任何依赖项的查询时（因为在这种情况下，我们只运行未修改过的代码！），我们的变更不会导致回归问题。

有时这种方法是合适的，有时则不合适，但在其他条件相同的情况下，尽可能多地保留代码不变，就能减少认知负担。

（你可能在开闭原则的语境中听说过这个想法。这个原则涵盖了许多面向对象编程的细节，但在这里并不相关；重要的是它背后的理念，即：“当需求发生变化时，你应该通过添加新代码来扩展[你的程序]的行为，而不是修改已经可以正常运行的旧代码。”）

就职

许多有趣的程序都涉及递归函数或递归数据结构（从某种理论意义上讲，递归是计算本身的核心）。根据你所在领域的不同，你可能会经常遇到递归，也可能只是偶尔遇到，但无论哪种情况，了解如何理解递归都会让你的工作轻松许多。

递归数据结构是指包含自身副本的结构（不一定是完全相同的副本，而是同一“类型”结构的一个实例）。这个副本可以包含另一个副本，依此类推；这个过程要么无限进行下去，要么在达到“基本情况”时终止。例如，分形就是递归的。

在计算机科学中，递归数据结构的经典例子是树。树是一个节点，它有一定数量的子节点；每个子节点本身也是一棵树。没有子节点的树称为叶子节点，这是基本情况。

列表也可以用递归的方式表示，尽管你通常不会这样想。每个递归列表都包含一个头（head），它是列表的“第一个”或最左边的元素，以及一个尾（tail），其中包含列表的剩余元素。尾本身也是一个列表，而基本情况列表是空列表。（类似地，你可以把自然数看作是递归的——除了0（基本情况）之外，每个自然数都是1加上另一个更小的自然数。）

递归函数是指调用自身的函数。递归函数通常用于处理递归数据结构，因为它们可以对自身的递归副本进行调用（例如，处理树的函数可以对所有子树调用自身）。

还有一种专门用于处理递归结构的证明技巧，称为归纳法。“经典”的归纳法用于证明某个命题P（n）对于任何自然数，这个结论都成立。n证明这一点需要两个步骤：

  • 证明P（0）属实。

  • 证明这一点P（n）暗示P（n+1）。

这第二步被称为归纳步骤，其假设是：P（n）成立的结论被称为归纳假设。归纳步骤是归纳法真正力量所在之处——P一旦掌握了归纳假设，证明起来通常就容易得多。归纳法的目的是写出一个“逐步”证明，而不是试图一次性证明所有数字。

编写递归函数时，尝试使用归纳法证明其正确性。以下是一个简单的示例，大致改编自 Nerve 代码库：

简单来说，Nerve 中有一个特殊情况需要我们向用户可视化抽象语法树 (AST)。完整的 AST 非常复杂，因此在显示之前，我们需要移除用户可能不关心的节点。移除节点后，该节点的父节点应该“继承其所有子节点”（技术上讲，我们需要收缩被移除节点与其父节点之间的边）。

关于术语的简要说明：严格来说，“收缩”一词仅适用于边，但我将稍微变通一下，也讨论节点和树的收缩。当我说“收缩一个节点”时，我指的是“收缩该节点与其父节点之间的边”。当我说“收缩一棵树”时，我指的是“收缩树中的某条边”。

以下是我们在 Nerve 中使用的函数（并非确切的函数，但可以让你了解其原理）：

function simplifyTree(root: Node): Node {
  let newChildren = [] as Array<Node>;
  
  for (const child of root.children) {
    const simplifiedChild = simplifyGraph(child);
  
    if (shouldContract(simplifiedChild)) {
      for (const grandChild of simplifiedChild.children) {
        newChildren.push(grandChild);    
      }
    } else {
      newChildren.push(simplifiedChild);
    }
  }
​
  root.children = newChildren;
​
  return root;
}

我们希望函数尽可能简化提供的抽象语法树（AST）。换句话说，后置条件是：返回的图simplifyGraph应该是“完全收缩的”——也就是说，不应该还能再收缩任何边。

以下是证明该条件确实成立的归纳证明：

  • 我们先来看基本情况。根据定义，根节点不能被收缩，因为它没有父节点可以将其收缩。因此，基本情况——一个单独的叶节点——已经满足了后置条件。如果我们传入simplifyGraph一个叶节点，它会原样返回，所以我们可以得出结论，它在基本情况下工作正常。

  • 是时候展现神奇之处了：归纳步骤。我们需要证明，如果simplifyGraph对于一棵树的每个子树，结论都是正确的。T是正确的T此外，至关重要的是，我们现在可以使用归纳假设，这意味着我们可以假设每个子树（即以 为根的每个树simplifiedChild）都不能进一步收缩。

    我们唯一需要考虑的新的潜在收缩发生在simplifiedChild和之间root。如果我们确定simplifiedChild需要收缩，我们就将其移除，并将其所有子节点嫁接到 上root。对每个 执行此操作后simplifiedChild，我们就可以确定以 为根的树root不能进一步收缩，因为如果它可以收缩，那就意味着至少有一个子树可以被收缩，这与归纳假设相矛盾。证毕！

如果你能凭直觉进行这种归纳推理，你可能会发现处理递归函数更容易。

（如果你愿意，可以尝试用整体推理的方式，而不是归纳法，来验证这种simplifyGraph方法是否适用于所有可能的输入。哪种方法对你来说更自然？）

以证据亲和力作为质量指标

我目前的观点大致是“你应该尝试在脑海中为你的代码编写一些简单的证明”。但实际上这篇文章还有一个不为人知的平行版本，那就是“你应该尝试用一种易于编写简单证明的方式来编写你的代码”。

同样，这篇文章的每个部分都有其对应的对偶形式：

  • 寻找单调性和不可变性。→ 编写单调且使用不可变数据结构的代码。

  • 记住你的前置条件和后置条件。→从前置条件和后置条件入手，围绕它们编写代码。代码结构要清晰易懂，便于理解和验证。

  • 你可以通过证明每个执行单元都满足某个不变式来证明该函数保持了该不变式。→ 你应该将代码细分为能够保持该不变式的最小单元。

  • 注意组件边界如何起到“防火墙”的作用，阻止变更传播。→ 尽可能多地构建这些“防火墙”，并在编写新功能时充分利用它们。

  • 使用归纳法逐步证明递归函数的相关结论，而不是一次性全部证明。假设归纳假设已经证明，并利用这一点。→ 逐步编写递归函数。假设递归调用已经实现，并编写构建函数的那部分。n+1案例来自n然后，单独实现基本情况。

其理念在于，你可以通过代码的易读性来判断代码的质量。如果你能轻松地证明代码的正确性，那么它很可能设计得相当不错。反之，如果代码总是让你感到沮丧或难以理解，你就应该考虑清理或重构代码，使其更加简洁明了。

我原本想把这种特性称为“可证明性”，但这个术语已经存在，而且含义不同，所以我就把它称为“证明亲和性”。

如上文所述，可以（至少在主观上）设计出最大程度的证明亲和性。

当然，证明亲和性并非软件质量的唯一维度（你还希望代码正确、运行速度快、易于使用），但我认为它非常重要；毕竟，为了构建、扩展、改进或测试代码，你必须理解它的功能、局限性以及潜在功能。这听起来或许有些夸张，但我认为，从某种重要意义上讲，证明亲和性是优秀编程的催化剂！

如何才能在这方面做得更好

正如我开头提到的，我刚才谈到的这种微观推理，只有当你能够不假思索地运用它时，才能真正发挥作用。这有点像打字；只有当你几乎完全凭本能就能打字时，掌握盲打技巧才能比一指禅节省时间。在这两种情况下，培养直觉都需要……练习！我认为没有捷径可走；你只能投入时间。

我认为最好的方法是多写（数学）证明。写程序证明当然会有帮助，但我认为，构建证明——无论主题是什么——本身就是磨练逻辑思维的绝佳途径，这种思维方式在处理复杂系统时会非常有用（但你必须自己写，而不仅仅是阅读。一定要做练习！）。就我个人而言，我很久以前就开始出于兴趣学习数学，我发现写证明确实有助于提高我在各种情况下的思维清晰度。

如果你不知道从哪里开始，我一直在学习斯坦福大学在 EdX 上的本科算法课程，这是一门有趣且注重证明的课程，而且（在我看来）教授很棒！

另一个不错的训练平台是 LeetCode——虽然我不太愿意这么说。和很多人一样，我认为 LeetCode 的面试题存在一些严重的缺陷，但它对于自主练习还是很有用的，因为很多题目的难度都恰到好处，足以锻炼你的证明能力。你不必给自己计时（我通常也不计时）。此外，尽量避免那些有“技巧”的题目；相反，要寻找那些至少部分挑战在于如何正确地构建和实现所有步骤的题目。专注于尽可能用最少的尝试次数成功提交（如果遇到一些小问题，比如语法错误，也没关系）。

祝您编码/验证愉快！