从业者十年思考：程序分析如何助力实现正确软件？

程序分析如何助力实现正确软件从业者分享十年思考与见解大约十年前我开始认真思考如何让编写正确的程序变得更轻松。对这个问题的研究让我接触到了形式化方法和类型系统等主题这些都是有助于确保给定程序符合某些规则的技术。然而我仍然不确定如何证明软件 真正 是正确的。这里所说的正确并非指执行的指令能产生与规范一致的结果而是指这个程序实际上能满足相关人员的期望。不幸的是这引出了一个看似不可能完成的任务的简单描述当所有相关人员都清楚程序应该做什么并且能够确认程序只做它应该做的事情时软件才是正确的。从某种意义上说这确实是不可能的。一方面有实际的程序另一方面还有抽象的 程序概念。这里大写的 程序概念 是存在于我们头脑中的理念。从某种意义上讲认定一个程序是正确的就意味着大家的想法达成了一致我想我是假设这是不可能的关于这一点在哲学上是否可行不在本文讨论范围内。这就使得我之前的表述变得更加严谨当所有相关人员都认同实际运行的程序充分体现了他们头脑中的 程序概念并且该程序只做它应该做的事情时这个程序才是正确的。那么我们如何知道实际存在的程序就是我们所设想的 程序概念 呢在思考这个问题时我认为最有帮助的概念是[语义鸿沟](https://en.wikipedia.org/wiki/Semantic_gap)。在我看来语义鸿沟凸显了我们在将想法形式化为代码的过程中所失去的东西。有些人阅读代码后能看出它反映了他们头脑中的 程序概念然后会说 看起来不错lgtm。我认为这是利用代码缩小人与程序之间语义鸿沟的理想模式。但也有人读了同样的代码后却完全搞不清楚它与自己头脑中的 程序概念 有什么联系。当我们用尽了缩小语义鸿沟的工具又面临推进工作的压力时除了郑重地敲下 看起来不错lgtm还能做什么呢显然阅读代码不可能是传达代码背后想法意图的唯一方式。不过我认为可执行代码确实有理由成为事实的来源。但如果代码甚至在程序员之间都不能有效地传达信息我们该如何帮助人们理解程序呢我认为这正是程序分析发挥作用的地方。在我看来程序分析是一种让我审视自己编写的程序自问 我做了什么 并能得到有意义结果的方法。实现这一点有很多途径虽然 运行代码 是最常见的方式但我感兴趣的分析分支是 静态分析。它之所以吸引我是因为理想情况下我们可以针对一组指定的组件询问整个系统的功能而无需消耗运行代码所需的资源。例如这个程序是否会尝试访问特定数据不登录是否可以访问某个网页换句话说每个程序中都有一些决策需要做出我们希望确认这些决策是经过审慎考虑的。但决策并非总是孤立做出的而且做出决策的人也不一定都能通过阅读代码来验证其正确性。能够对系统进行检查为人们关于日常生活中所涉及程序的问题提供一致且准确的答案是实现正确软件的必要条件。即使作为程序的作者我们也只是摸到大象一部分的盲人。我们需要他人的视角和理解来确认我们做对了。