Question

编程就是用语法与机器交流思想。在写程序的时候，我们知道在程序执行的时候我们想要机器做什么，而了解编程语言的语义让我们相信机器将理解程序每个细节的含义。

但复杂的计算机程序远非单个语句和表达式的累加那么简单。一旦把许多小零件组合到一起构成更大的整体，能检查整个程序是否实际做了我们想要它做的事会很有用。例如，我们可能想要知道它总是返回确定的结果，或者运行这个程序能对文件系统或者网络有既定的副作用，或者只是不含有明显的一遇见非期望输入就会导致崩溃的 bug。

实际上，我们可能想要程序拥有各种各样的属性，而如果能只是检查一个特定程序的语法来看它是否有那些属性，将是相当方便的事情。但从 Rice 定理可知，通过看源代码预测一个程序的行为不可能总是给出正确答案。当然，最直接的查明一个程序将会做什么的途径就是执行它，有时候这确实没问题——大量的软件测试就是通过基于已知的输入运行再根据期望的输出检查结果完成的——但有时候运行代码可能也不是一种可接受的方式，原因如下。

首先，任何有用的程序有可能会处理直到运行时才知道的一些信息：来自用户的交互式输入，作为参数传进来的文件，从网络读取的数据，诸如此类的东西。我们当然可以用一些假的输入运行程序以便感知它能做什么，但那只会告诉我们针对这些输入的程序行为，而真正的输入不一样时会发生什么呢？用输入的所有组合运行程序经常是不实际或者不可能的，而用特定集合的输入运行程序虽然可行，却不一定能告诉我们有关其行为的多少信息。

还有一个问题，我们在 8.1.4 节已经探索过了，就是用足够强大 1 的语言写成的程序可以永远运行而从来不会产生结果。这让通过运行程序来可靠地研究任意程序变得不可能，因为有时候不可能预先说出一个程序是否会无限运行（参见 8.3 节），因此任何尝试运行程序的自动监测器都面临永远得不到答案的风险。

1“ 足够强大”这里意思是“通用的”，参见 8.1.4 节。

最后，即使一个程序不管什么原因，它事先所有的输入数据都可用，而且总是能终止而不会永远循环，运行这个程序的代价也可能非常高或者很不方便。可能会花很长时间才会结束，或者有不可逆转的副作用——发送邮件、汇钱、发射导弹——对于测试的目的，这些都是不应该发生的。

所有这些原因让能够不实际执行程序就能发现它的问题变得很有用。做到这一点的一种方式是使用抽象解释，这是一种分析技术。使用这种技术时，我们执行这个程序的简化版本，然后使用执行结果推导出原始程序的性质来。