你这个问题,也是过去历代计算机科学家想要攻克的问题。你可以读一读 Dijkstra 1972 年的图灵演讲。
英文版:
https://www.cs.utexas.edu/~EWD/transcriptions/EWD03xx/EWD340.html中译版:
https://www.ituring.com.cn/article/71467他提到了:
“论据三是建立在程序正确性问题的建设性方法上的。今天,一项普通的技术就是写一个程序,然后去测试。 尽管,程序测试是一种非常有效的方法去暴露 bugs ,但对证明不存在 bugs 几乎是完全没用的。显著提高程序可信度唯一有效的方法是给出一个令人信服的关于正确性的证据。但是我们不应该首先写出程序,然后去证明它的正确性,因为要求证明只会增加苦逼程序员的负担。相反,程序员应该让正确性证明和程序相互验证,发展。论据三本质上是从以下的观察得来的。如果一个人问自己一个令人信服的证据应该具备什么,他了解后,写了一个很好的满足了证明要求的程序,然后这些关于正确性的担心变成一种有效的启发式的指导。当我们把自己限制在智能可控程序时,按照定义,只有这种方法是可行,但这种方法也提供许多有效的方法,让我们从中挑选一个满意的。”
他的思想是测试驱动开发( TDD ):先写好验证的测试,把所有可能的情况考虑到,再写程序。你只需要说明你写用于测试的程序是有效的(基于合理正确的思维逻辑),只要能测试通过,那么你写的被测试的程序必然是正确的。
但这个毫无疑问会增加程序员的工作量和负担。对足够优秀的程序员来说,我觉得一定是不必要的负担。
我通常只对不稳定的函数和接口添加测试。有些函数的参数来源于不可控的外部数据源,比如要读取一个文本,读取到的数据各种可能性都有,这个时候就要添加测试程序,只是用来验证和保证被测试程序的正确性。