抽象化

    为了阐明具体信息和抽象信息之间的联系，让我们以符号分析为例，考虑三种不同的抽象函数。这些函数会展示语义格中的每个元素如何通过分析格中的元素最精确地描述。这些函数将具体值的集合、具体状态的集合和具体状态的n元组映射到它们可能的最精确的抽象对应结果上：

• $\mathcal{P(\mathbb{Z})}$：是一个整数的幂集合，排序是基于子集关系

• Sign：是4.1节中的符号格

  

• $ConcreteStates = Vars \rightarrow \mathbb{Z}$：是一个映射，输入是程序变量，输出是整数的值

• $State = Vars \rightarrow Sign$：是一个映射，输入是程序变量，输出是符号格里面的元素

• n：CFG的节点的个数

这三个函数目的是为了精确的描述之前我们非正式的描述内容：(可以认为这三个函数是不同维度的抽象与具体的关系)

• 函数$\alpha_a$（目标是一个具体的整数值，如何映射到我们期望的抽象结果上）：对于任何的整数集合D，我们知道$D \in \mathcal{P(\mathbb{Z})}$，那么$\alpha_a(D)$定义如下：如果D是空集合那么就是bottom，D只有正数、负数、零对应+-0，其他情况就是top。

  

• 函数$\alpha_b$（目标是给定一个CFG节点，如何将节点之前的具体状态，映射到我们期望的抽象状态上）：对于R作为具体状态的子集合，也就是具体状态幂集合的元素，那么$\alpha_b(R)$的定义如下：其结果是一个映射$\sigma$，输入是对一个变量X（Vars的元素），输出是在具体状态里面这个变量的值，经过函数$\alpha_a$的结果。简单来说，这个$\alpha_b$的目的就是用来计算，从一个具体CFG节点v里面的具体状态，每个变量的符号。

  

• 函数$\alpha_c$（目标是对于一个程序，所有的节点的映射关系）：将一个节点，扩展到整个程序

  

    抽象函数是单调的是一种自然条件。直观地说，较大的具体值或状态集合不应该由较小的抽象元素在格序中表示。
  

具体化

    同样地，我们可以定义具体化函数（也是单调的），以具体值、状态和状态的n元组来表达分析格元素的含义：

• $\gamma_a$：输入是一个抽象符号格的元素，给出对应的整数的集合

  

• $\gamma_b$：输入是一个抽象状态，也就是Vars→Sign的映射，求解所有满足的具体状态的集合，满足的条件是，具体状态里面的变量X的值，属于这个抽象状态里面这个变量对应抽象格元素所对应的整数集合。简单说，也就是如果我们已知了一个变量X的符号，那么我们就知道了这个变量对应的具体的值的范围，那么我们就能够找到所有满足这个范围的具体状态的集合。

• $\gamma_c$：描述的是整个函数的情况。