如何证明一个程序是正确的？

注：本篇推送的主题是结构化编程范式，阅读本文需要简单的数理逻辑和编程语言方面的背景知识。

自从1945年，Alan Turing在真实的计算机上编写了第一个真正的计算机程序起，编程领域已经发生了许多次革命性的变革。其中，广为人知的是编程语言的演变。今天的主题则是另一个可能更重要的变革，也就是编程范式（Programming Paradigms）领域的变革。编程范式是与编程语言相对不相关的编程的方式，它告诉你该使用哪种结构来编程，以及何时该使用它们。迄今为止，已有三种编程范式，分别是结构化编程（Structured Programming）、面向对象编程（Object-Oriented Programming）、以及函数式编程（Functional Programming）。

首先，从结构化编程讲起。简单来说，结构化编程语言就是支持顺序、选择和迭代这三种控制结构的编程语言。结构化编程语言的起源可以追溯到上世纪中叶Dijkstra对程序正确性的证明（对，就是发明Dijkstra算法的那个Dijkstra）。

程序正确性的数学证明

Edsger Wybe Dijkstra于1930年出生在鹿特丹。1952年到1955年，Dijkstra在上大学之余，还在阿姆斯特丹的数学中心接受了一份程序员的工作。事实上，他是荷兰的第一个程序员。

Dijkstra发现，任何复杂的程序都包含了太多的细节，让人的大脑无法在没有帮助的情况下进行管理。忽略一个小细节就会导致一些看似有用的程序以惊人的方式失败。

对这个问题，Dijkstra的解决方案是数学证明。他的设想是建立一个包含假设，定理，推论，和引理的欧几里德公理体系。程序员可以像数学家一样使用经过这个公里体系验证的结构，并将它们与代码结合起来，然后证明自己是正确的。

当然，在构建公理体系的过程中，Dijkstra却发现证明简单程序的正确性已经是一件很有挑战性的任务。在他的调查中，Dijkstra发现goto语句的某些用法可以防止程序模块被递归地分解成更小的单元，从而不能使用分治法来证明程序的正确性。然而，并非所有的goto的语句都有这个问题。Dijkstra意识到这些“好的”使用了goto对应的简单选择和迭代控制结构，例如if/then/else和do/while。只使用那些类型的控制结构的模块可以被递归地细分为可证明的单元。

1966年，Böhm和Jacopini在《Comm. ACM》上发表了一篇论文，证明所有的程序都可以由顺序、选择和迭代这三个结构组成，也就是说，goto语句在逻辑上是多余的。

1968年，Dijkstra在《Comm. ACM》上发表了一篇名为《Go To Statement Considered Harmful》的文章，文中概述了他对这三种控制结构的证明。

在顺序结构中，Dijkstra通过简单的枚举从序列的输入追溯到序列的输出，从而证明程序是正确的。

在选择结构中，Dijkstra通过枚举每条路径的正确性来证明选择结构的正确性。如果这每条路径都最终产生了适当的数学结果，那就证明了选择结构是正确的。

迭代的证明有一点不同。为了证明迭代是正确的，Dijkstra必须使用归纳法。他首先通过枚举证明了第一次迭代的正确性，再通过枚举证明了如果第N次迭代是正确的，那么第N + 1次迭代是正确的。他还通过枚举证明了迭代的开始和结束标准。

这样的证明是费力而复杂的，但它们是形式化的数学证明。继续发展下去，可以用这些数学证明构建出一个欧几里得体系结构。

于是一个值得注意的情况出现了：所有的程序都可以由三个数学上可证明正确的控制结构构造而成，而逻辑上多余的goto语句则会破坏这种控制结构。

证明程序正确性的科学方法

但是欧几里德式的公里结构没有建立起来，程序员们也从来没有看到过通过艰苦的过程来形式化证明每一个小函数正确的好处。Dijkstra的梦想破灭了。今天的程序员很少相信形式化证明是生产高质量软件的合适方法。

当然，形式化的数学证明并不是证明某些东西正确的唯一策略，另一个非常成功的策略是科学方法。

科学与数学本质上是不同的，因为科学理论和定律不能被证明是正确的。我无法证明牛顿第二定律或万有引力定律是正确的。我可以向你们展示这些定律，我可以做一些测量来证明精确到很多小数位之后这些定律依然是正确的，但我不能用数学证明来证明它们。不管我做了多少实验，或者我收集了多少经验证据，总有可能存在一些实验会证明牛顿第二定律或万有引力定律是不正确的。然而，我们每天都把自己的生活押在这些定律上。每当你坐上一辆车，你就会认为牛顿第二定律是对世界运转方式的可靠描述。你每走一步，你就会把你的健康和安全赌注压在万有引力定律上。

这就是科学方法的本质：它是可证伪的（falsifiable），但不可证实（provable）。

科学方法不能证明程序是正确的，只能证明程序是错误的。那些经过了许多次尝试也不能证明错误的程序，我们认为对我们来说是足够正确的。这种证明程序正确性科学方法在软件开发领域还有个更为熟知的名字——测试。

换句话说，一个程序可以通过测试被证明是不正确的，但是它不能被证明是正确的。而那些经过充分的测试的程序，可以被认为对我们来说是足够正确的。

这一事实有些令人震惊。尽管软件开发看似是一个操纵数学结构的过程，但是实际上软件开发更像一门科学。所谓的软件开发的科学方法，其实就是通过无法证明程序是错误的，来证明程序是正确的。

但是科学方法只能应用于可证实的程序。所以不管一个程序通过了多少个测试，如果它不受限制地使用goto对程序的控制进行转移，它就不能被认为是（足够）正确的，因为它是在科学上是不可证伪的。

编程语言的发展也证明了科学方法的有效性。随着计算机语言的不断发展，goto语句的声明一直在向底层移动，直到消失。大多数现代语言都没有goto语句——当然，LISP从来没有过。有些人可能会指出Java的命名中断或类似于goto的异常处理。事实上，这些结构并不是像Fortran或COBOL这样的旧语言的完全无限制的控制权转移。即使仍然支持goto关键字的语言，也经常将目标限制在当前函数的范围内。

结论

结构化编程的本质其实是对程序控制的直接转移施加约束（也就是对goto语句加以限制），以确保程序可被科学方法（也就是足够的测试）证明正确。这就是现代编程语言通常不支持无约束的goto语句的原因。

我们递归地将程序分解为一组小的可证伪的程序单元（函数），然后用尝试测试来证明那些小的可证伪的函数是不正确的。如果这些测试不能被证明不正确，那么我们认为这些函数对我们来说是正确的。

从最小的函数（function）到最大的组件（component），软件开发都是由可证伪性（falsifiability）驱动的。软件开发者努力定义易于证伪（可测试）的模块和组件。为了做到这一点，他们在一个更高的层面上采用了类似于结构化编程的限制性规则。

参考文献

[1] Dijkstra, Edsger W. "Letters to the editor: go to statement considered harmful." Communications of the ACM 11.3 (1968): 147-148.

[2] Martin, Robert C. Clean architecture: a craftsman's guide to software structure and design. Prentice Hall Press, 2017.

©一天木易 2018

封面图来自Luca Bravo，根据CC0协议使用