本章的内容是为了提供一种形式化的方法，也就是数学方法来论证分析的属性。个人觉得如果不是从事学术研究，能看懂就很好！
在前面的章节中，我们只是非正式地使用了分析的"soundness"一词：如果一个分析是sound的，那么它对于给定程序推断出的属性在所有实际执行中都成立。抽象解释的理论为分析的soundness提供了坚实的数学基础，通过将分析的规约与编程语言的形式语义相关联。抽象解释的另一个用途是了解分析设计或分析设计的一部分相对于分析结果的选择的格是否尽可能精确，以及可能出现不精确的地方。抽象解释的基本思想是由Cousot和Cousot在1970年代引入的[CC76，CC77，CC79b]。