我作为实践者的程序分析观

# 从业者视角的程序分析 来源：https://sawyer.dev/posts/practitioner-program-analysis/ \>首页 (https://sawyer.dev/)\>博客文章 (https://sawyer.dev/posts) ## 我对程序分析的实践看法 大约十年前，我开始认真思考：怎样才能让写出“正确”程序这件事变得更容易。研究这个问题把我带进了形式化方法、类型系统等方向——这些技术能帮助确认一段代码是否遵守某些规则。但我仍然不确定，如何*真正*证明软件是正确的。不是“执行结果与规约一致”那种正确，而是“这段程序确实做了*所有人希望它做的事*”那种正确。 不幸的是，这引出了一个看似不可能完成的任务：当所有相关人员都清楚程序该做什么，并且能确认程序只做该做的事时，软件才算正确。某种意义上，这*确实*不可能。代码只是代码，而“程序”（大写 P）是我们脑海里的概念。要让所有人认同代码正确，就等于让所有人对同一个概念达成一致（我觉得这做不到；哲学可行性不在本文讨论范围）。于是我把说法改得学究一点：当所有人一致同意，现实运行的程序充分代表了他们脑海中的 Program，并且现实程序只做该做的事时，它才算正确。那么，我们怎么知道写出来的代码就是大家想象中的那个 Program 呢？ 对我帮助最大的概念是[语义鸿沟](https://en.wikipedia.org/wiki/Semantic_gap)。在我看来，它凸显了把想法形式化成代码时我们失去了什么。有些人读代码，发现它跟脑海里的 Program 一致，就能敲下“lgtm”。这是最理想的用代码缩小语义鸿沟的模式。但另一些人读同一段代码，却完全看不出它跟脑海里的 Program 有何关联。当所有缩小语义鸿沟的工具都已用尽，而项目又要继续推进，我们只好也默默敲下“lgtm”。显然，光靠读代码不足以传达代码背后的意图。与此同时，可执行代码又最有资格成为“真相源”。如果代码连程序员之间都无法有效沟通，我们该怎样帮大家理解程序？我认为答案就是程序分析。 我把程序分析看作一种手段：对自己写的程序问一句“我到底干了什么”，然后得到有意义的回答。方法很多，“跑一遍”最流行，但我更感兴趣的是*静态分析*。它吸引人的地方在于，理论上可以拿到一组已定义的组件，在不真正运行、不消耗运行资源的前提下，问整个系统能干什么。这段代码会不会访问某份数据？有没有不登录就能进到某网页的路？换句话说，程序里到处要做决策，我们想知道这些决策是否被谨慎地做过。 然而决策并不总在真空中做出，也不总由能读代码的人来做。要检查系统——对日常生活中扮演重要角色的程序，给出一致且准确的回答——是拥有正确软件的前提。即便身为作者，我们也只是摸象的盲人之一。需要他人的视角与理解，才能确认我们没做错。