之前定义的各种就是为了在本章节介绍soundness
在本章节，我们会形式化的定义，当我们声明一个分析具有soundness属性是什么含义。我们令 $\\alpha: L_1 \\rightarrow L_2$ 表示一个抽象函数，其中L1是收集语义的格，L2是分析的格。举一个例子，在12.2节中针对于符号分析的函数 $\\alpha_c: (\\mathcal{P}(ConcreteStates))^n \\rightarrow States^n$，就是这样的一个函数。一个分析针具有sound的属性，是对于一个给定的程序的语义和抽象函数，具有如下属性：
$$ \alpha(\{\![P]\!\}) \sqsubseteq [\![P]\!] $$
换句话说，Soundness（精确性）意味着分析结果对程序语义的抽象进行了过度逼近。对于符号分析，这个性质可以通过以下方式进行说明：【注意：这个图是格，所以顺序是格的偏序关系，在格的顶端表示范围越大！也就越不精确，是过度近似】
对于12.1节的符号分析的例子：
var a,b,c;
a = 42;
b = 87;
if (input) {
c = a + b; // 87+42=129
} else {
c = a - b; // 42-87=-45
}
// c = 129, -45; a = 42; b = 87
可以得到，对于这三个程序节点，都满足抽象函数对于具体状态进行抽象之后得到的抽象结果，在抽象结果这个领域，都是偏序关系“小于或者等于”分析所得到抽象结果，
如果我们使用具体化函数而不是抽象化函数来指定两个域之间的关系，我们可以对精确性进行双重定义，即分析结果的具体化过度逼近了程序的语义：
$$ \{\![P]\!\} \sqsubseteq \gamma([\![P]\!]) $$
对于符号分析来说，具体化函数的定义是 $\gamma_c: States^n \rightarrow (\mathcal{P}(ConcreteStates))^n$，这个属性也就是说：（比如说，分析得到的是T，而具体收集语义只会是+，那么就是sound）
通常来说，当我们提到soundness的时候，我们不是针对特定的程序。我们认为一个分析的sound属性，是针对于所有程序而言。