如何验证程序的正确性

[pythonee]

突然想到一个问题：

我们在 leetcode 上提交的代码，有个“程序“来验证我们提交的代码的正确性，可哪个程序去验证这个“程序”的正确性呢？

[Buges]

自然是测试数据集。看标题还以为你说的是形式化验证。

[keith1126]

https://coq.inria.fr/

https://vst.cs.princeton.edu/

当然，我知道大多数情况下说的「验证」，无非是看看输入输出是否符合预期，而非上面两个形式化验证……

[pythonee]

@Buges 我感觉应该不是测试数据集

[anonymous256]

你这个问题，也是过去历代计算机科学家想要攻克的问题。你可以读一读 Dijkstra 1972 年的图灵演讲。
英文版： https://www.cs.utexas.edu/~EWD/transcriptions/EWD03xx/EWD340.html
中译版： https://www.ituring.com.cn/article/71467

他提到了：
“论据三是建立在程序正确性问题的建设性方法上的。今天，一项普通的技术就是写一个程序，然后去测试。 尽管，程序测试是一种非常有效的方法去暴露 bugs ，但对证明不存在 bugs 几乎是完全没用的。显著提高程序可信度唯一有效的方法是给出一个令人信服的关于正确性的证据。但是我们不应该首先写出程序，然后去证明它的正确性，因为要求证明只会增加苦逼程序员的负担。相反，程序员应该让正确性证明和程序相互验证，发展。论据三本质上是从以下的观察得来的。如果一个人问自己一个令人信服的证据应该具备什么，他了解后，写了一个很好的满足了证明要求的程序，然后这些关于正确性的担心变成一种有效的启发式的指导。当我们把自己限制在智能可控程序时，按照定义，只有这种方法是可行，但这种方法也提供许多有效的方法，让我们从中挑选一个满意的。”

他的思想是测试驱动开发（ TDD ）：先写好验证的测试，把所有可能的情况考虑到，再写程序。你只需要说明你写用于测试的程序是有效的（基于合理正确的思维逻辑），只要能测试通过，那么你写的被测试的程序必然是正确的。

但这个毫无疑问会增加程序员的工作量和负担。对足够优秀的程序员来说，我觉得一定是不必要的负担。

我通常只对不稳定的函数和接口添加测试。有些函数的参数来源于不可控的外部数据源，比如要读取一个文本，读取到的数据各种可能性都有，这个时候就要添加测试程序，只是用来验证和保证被测试程序的正确性。

[maplerecall]

不用想太多，简单的说所有程序追究到最后都是人工测试。

否则你将不得不面对类似"测试测试程序的测试程序应该怎么测试"这种无限套娃的问题。

[MegrezZhu]

去找那个在咖啡店点炒饭的测试人员

[muzuiget]

可以搜一下“刘未鹏 永恒的金色对角线”这篇科普文章。

[CrazyRundong]

形式化验证（即答），直接从理论上证明程序的正确性

[Coelacanth]

看一下北大熊英飞开的这门课，课件写得很不错：
https://xiongyingfei.github.io/SA/2019/main.htm

第一节的 Intro：
https://xiongyingfei.github.io/SA/2019/01_intro.pdf

[aguesuka]

https://www.google.com/search?q=%E7%A8%8B%E5%BA%8F%E5%8D%B3%E8%AF%81%E6%98%8E

[xarthur]

好家伙，楼主框的一声就丢出个大问题。
如果限定于 Leetcode 就是测试数据集，如果要是讨论程序证明就复杂了……

[mapoor]

个人猜测 leetcode 平台分为两步检验用户的代码，语法检查和运行时检查。
* 运行时检查： 如大家所言，就是测试用例，用以判断运行结果是否正确。
* 语法检查：不同的语言使用不同的 Compiler ，用以检查用户代码的语法正确性。这个 compiler 就是您所谓的那个“程序”。

那么是什么东西来验证这个 Compiler 呢？ 先将这个问题具体化下，gcc 这个编译器是如何保证自己正确的。
看下 gcc 的源码 https://github.com/gcc-mirror/gcc 其也是用 c 语言写的，
这里就要提到 c 语言标准，由 ANSI 和 ISO 两大组织制定，如：C89 标准。
使用旧版本的 c 语言去实现新的标准，再使用旧版本的 gcc 来编译出新版本的 gcc 。

那么第一个版本的 gcc 是怎么来的呢？
https://gcc.gnu.org/wiki/History
总而言之，先有标准，再实现标准。 （欢迎指正）

[aguesuka]

leetcode 就是大量的测试用例. 不过这个答案 OP 可能不想听.

可以参考 https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching/INF551/course.pdf

But how can we achieve this goal of applying techniques of proofs to programs?
It turns out that we do not even need to come up with some new ideas thanks to
the so-called proof-as-program correspondence discovered in the 1960s by Curry
and Howard: a program is secretly the same as a proof! More precisely, in a
typed functional programming language, the type of a program can be read as
a formula, and the program itself contains exactly the information required to
prove this formula. This is the one thing to remember from this course:
PROGRAM = PROOF

简译:
怎么校验程序.
感谢 Curry 和 Howard 在 1960s 发明的证明(名词)作为程序的对应关系, (我们不用充钱买 IDEA 了(划掉)):
程序和证明(名词)其实是一样的!
准确地说, 一个有类型的函数式编程语言, 程序的类型可以看成是公式, 而程序的存在就是这个公式所需的证明(动词).
只需记住一点就是:
程序=证明(名词)


对了, 这本书的导论的第一节的标题就是 Proving instead of testing(证明而不是测试)