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

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

最直接的查明一个程序将会做什么的途径就是执行它，有时候这确实没问题——大量的软件测试就是通过基于已知的输入运行再根据期望的输出检查结果完成的——但有时候运行代码可能也不是一种可接受的方式，原因如下。

首先，任何有用的程序有可能会处理直到运行时才知道的一些信息：来自用户的交互式输入，作为参数传进来的文件，从网络读取的数据，诸如此类的东西。

还有一个问题,就是用足够强大的语言写成的程序可以永远运行而从来不会产生结果。这让通过运行程序来可靠地研究任意程序变得不可能，因为有时候不可能预先说出一个程序是否会无限运行。

最后，即使一个程序不管什么原因，它事先所有的输入数据都可用，而且总是能终止而不会永远循环，运行这个程序的代价也可能非常高或者很不方便。

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

抽象解释

抽象解释给了我们一种着手处理难处理问题的方法，这些难处理的问题或许过于庞大，过于复杂，或者有太多的未知东西难以直接处理。抽象解释的主要思想就是使用抽象，或者通过让它更小，更简单，或者通过去掉未知的东西，但这样做还能保留足够的细节，以便让它的解决方案与原始问题相关。

静态语义

到目前为止，我们已经看到了如何不实际执行计算就能发现它的近似信息。我们本可以通过实际执行计算来获得更多信息，但近似的信息比没有还是要强，而且对于某些程序（如路线规划） ，可能这就是我们所需要的全部了。

我们了解了编程语言的动态语义，一种定义代码运行时含义的方法。一种语言的静态语义告诉我们程序性质，无需执行就可以研究。静态语义的经典例子就是类型系统：它是一个能用来分析程序的规则集合，能检查其中是否含有某种 bug。

应用

我们对抽象解释的讨论非常不正式。正式来讲，抽象解释是一种数学化的技术，同样语言的不同语义通过函数连接到一起，这些函数把具体值的集合转换成抽象值的集合，反之亦然。这就允许抽象程序的结果和性质可以按照具体程序的方式来理解。

这项技术一个著名的工业级应用是 Astrée 静态分析器（http://www.astree.ens/fr/） ，它使用抽象解释自动证明一个 C 程序没有像被零除、数组越界和整数溢出这样的运行时错误。
Astrée 不仅已经用来验证为国际空间站运送补给的儒勒·凡尔纳（Jules Verne）ATV-001 任务的自动对接软件，还被用来验证空客 A340 和 A380 飞机的飞行控制软件。抽象解释通过提供安全的近似而不是有保证的答案来遵循 Rice 理论，因此 Astrée 有可能报告实际不存在的运行时错误（错误警告） ；实际上，它的抽象在验证 A340 软件时准确到足以避免任何错误的警告。