Question

本章已经概括了抽象解释的基本思想：使用代价低的近似来了解代价高的计算，并展示了一个简单类型系统作为例子说明近似对分析程序是很有用的。

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

这项技术一个著名的工业级应用是 Astrée 静态分析器（http://www.astree.ens/fr/），它使用抽象解释自动证明一个 C 程序没有像被零除、数组越界和整数溢出这样的运行时错误。

Astrée 不仅已经用来验证为国际空间站运送补给的儒勒·凡尔纳（Jules Verne）ATV-001任务的自动对接软件，还被用来验证空客 A340 和 A380 飞机的飞行控制软件。抽象解释通过提供安全的近似而不是有保证的答案来遵循 Rice 理论，因此 Astrée 有可能报告实际不存在的运行时错误（错误警告）；实际上，它的抽象在验证 A340 软件时准确到足以避 免任何错误的警告。

用 Simple 语言写的程序只能操纵基本的值（数字和布尔值），因此本章的类型都很基本。现实中的编程语言会处理很多种值，因此真实的静态类型系统要更复杂。例如，像 ML 和Haskell 这样的静态类型函数式编程语言中函数也是值（就像 Ruby 的 proc），因此它们的类型系统支持函数类型。意思就像“带有两个数字参数并返回一个布尔值的函数”，可以让类型检查器校验到一个函数调用中用到的参数与函数定义的参数匹配。

类型系统还可以携带其他信息：Java 有一个类型与影响系统（type and effect system）不只跟踪方法参数和返回值的类型，还会跟踪能由方法体抛出的受检异常（checked exception，抛出一个异常是一个影响），用来保证所有可能的异常要么被处理掉要么被传播出去。