这里会有一个有趣的现象！因为基于数据流分析的方式，都是在抽象域上定义好格，然后算不动点。那么这个格决定了分析的一切属性，比如soundness。在具体应用的时候，soundness对于缺陷检测则很带来大量的误报。因此，很多时候，我们并不会用数据流分析的方式做缺陷检测，而是采用符号执行，或者简单粗暴的模式匹配。

    假设我们正在开发一种新的分析方法，并且我们已经选择了一个分析格和为各种编程语言构造生成分析约束的规则。为了使分析的准确性和精确性能够进行形式化推理，我们还提供了适当的收集语义（如第12.1节所述）以及定义分析格元素含义的抽象/具体化函数（如第12.2节所述）。此外，假设我们已经使用第12.3节中的方法证明了分析的准确性。现在我们可以问：相对于所选择的分析格，我们的分析约束是否尽可能精确（但仍然保持准确性）？

    如前面内容所述，

• 我们令 $\alpha: L_1 \rightarrow L_2$ 表示一个抽象函数，其中L1是收集语义的格，L2是分析的格
• $\alpha, \gamma$ 形成一个Galois连接，
• $cf: L_1 \rightarrow L_1, af: L_2 \rightarrow L_2$，分别表示语义约束和分析约束的函数

那么，我们定义af是cf的最优抽象，如果

$$ af = \alpha ~\circ~cf~\circ~\gamma $$

(也可以被写作：$af(b) = \alpha(cf(\gamma(b))) ~\text{for all}~b \in L_2$。)用符号分析作为一个例子，这个属性可以表示为如下形式：

对比soundness的概念，

我们来看为什么$\alpha ~\circ~cf~\circ~\gamma$是对于cf函数的sound抽象来说，是最精确的单调函数。假设函数$g: L_2 \rightarrow L_2$ 是cf函数的另一个sound抽象，并且也是单调函数，那么我们可以知道对于所有具体域里面的 $a \in L_1$，（演算再抽象 ≤ 抽象再演算）

$$ \alpha( cf(a)) \sqsubseteq g(\alpha(a)) $$

那么对于所有的抽象域里面的元素 $a' \in L_2$，因为$\alpha \circ \gamma$ 是减少的操作（也就是没有最开始的抽象大），并且g是单调的，那么

$$ \alpha( cf(\gamma(a'))) \sqsubseteq g(\alpha(\gamma(a'))) \sqsubseteq g(a') $$

因此

$$ \alpha ~\circ~cf~\circ~\gamma \sqsubseteq g $$

也就是说，$\alpha ~\circ~cf~\circ~\gamma$是最精确的抽象。

    请注意最优性条件告诉我们：对于给定的分析格元素 y，我们可以通过先具体化 y，然后应用语义函数 cf，最后进行抽象，来获得最佳可能的（即最精确但仍然保持准确性）cf 的抽象。不幸的是，这一观察并不自动给我们提供计算最优抽象的实际算法，但它使我们能够推理出关于我们手动指定的分析约束精确性的信息。