[科普中国]-抽象释义

在计算机科学中，抽象释义是基于在有序集合特别是格上的单调函数，计算机程序的语义的可靠逼近理论。它可以被看作对计算机程序的部分执行，获取关于它的语义信息(比如，控制结构、信息流)而不进行所有计算。

它的主要具体应用是形式静态分析，关于计算机程序的可能执行的信息的自动提取；比如这种分析有两个主要用途:

在编译器内部，分析程序来确定特定优化或变换是否是可适用的；针对缺陷类的程序的调试甚至校验。

抽象释义是 Patrick Cousot 和 Radhia Cousot 所形式化的。

直觉我们现在展示一下抽象释义在现实世界中非计算例子的意味着什么。

让我们考虑在会议室中人们。如果我希望证明某个人不在场，一个具体的方式是查看所有参与者的名字和唯一于他们的某种标识符比如美国的社会保障编号的列表。因为没有两个人有相同的编号，有可能证明或反证一个参与者的出席，简单的通过在列表中查找他的名字或他的编号。

但是我们可以限制自己只登记他们的名字。如果一个人的名字在列表中没有找到，我们可以安全的结论说这个人不在场；但是如果有这个名字，我们不能明确的结论而不做进一步的质询，原因是有可能重名。我们要注意这个不精确的信息对多数用途是足够的，因为实践中重名是很少见的。但是在严格的情况下，我们不能确切的说某个人在屋子里；我们只能说他可能在这里。如果我们查找的这个人是罪犯，我们将发出“警报”；但是当然有可能发出“假警报”。类似的现象将出现在程序的分析中。

如果我们只感兴趣于某些特定信息，比如“有年龄n岁的人在屋子中吗？”，则必须保存所有人的名字和生日的列表是不必需的。我们可以安全和不损失精确的限制自身保存参与者的年龄的列表。如果这处理起来太多了，我们可以只保存极小年龄m和极大年龄M。如果问题是关于严格小于m或严格大于M的年龄，则我们可以安全的回应没有这个参与者在场。否则，我们只能说不知道。

在计算的情况下，具体的精确的信息在有限时间和内存内一般是不能计算的(参见Rice定理和停机问题)。抽象被用来把问题一直简化到有职能自动解答的问题。减少精度的一个关键要点是使问题易于处理而对回答你感兴趣的问题(比如“程序会崩溃吗?”)仍保持足够的精度。1

计算机程序的抽象释义给定一个编程或规定语言，抽象释义一般由抽象关系连接的一些语义所构成。语义是程序的可能行为的数学特征化。描述了非常接近程序的实际执行的最精确的语义被称为具体语义。例如，指令式编程语言的具体语义可能对每个程序关联上它可以生成的执行跟踪的集合 – 执行跟踪是程序执行的一序列的可能的连续状态；状态典型的构成自程序计数器和内存位置(全局、栈和堆)的值。更抽象的语义是导出的，比如你可以只考虑在执行中可触及的状态的集合(相当于考虑在有限跟踪中的最后状态)。

静态分析的目标是在某些点上导出可计算的语义释义。例如，可以选择表示操纵整数变量的程序的状态，通过忘记变量的实际值并只保持它们的符号(+, - 或 0)。对于某些基本运算比如乘法，这种抽象不丢失任何精度: 要得到乘积的符号，知道操作数的符号就足够了。对于某些其他运算，抽象可能丢失精度: 比如不可能知道操作数分别是正和负的求和的符号。

有时精度的丢失对使语义成为可决定性的是必需的(参见Rice定理,停机问题)。一般的说，在分析的精度和它的可决定性(可计算性)或可跟踪性(复杂性)之间要做出妥协。

在实践中定义的抽象适合于想要分析的程序性质和目标程序的集合二者。1

形式化设L是叫做具体集合的有序集合，并设L′是叫做抽象集合的另一个有序集合。通过定义映射一个的元素到另一个的元素的全函数，把这两个集合相互联系起来。

函数 α 叫做抽象函数，如果它映射在具体集合L中的元素x到抽象集合L′中的元素 α(x)。就是说，在L′中的元素 α(x) 是L中的元素x的抽象。

函数 γ 叫做具体化函数，如果它映射在抽象集合L′中的元素x′到具体集合L中的元素 γ(x′)。就是说，在L中的元素 γ(x′) 是L′中的元素的x′的具体化。

设L1,L2,L′1和L′2是有序集合。具体语义f是从L1到L2的单调函数。从L′1到L′2的函数f′被称为f的有效抽象，如果对于所有L′1中的x′有 (f∘γ)(x′) ≤ (γ∘f′)(x′)。

程序语义在循环或递归过程在场的情况下一般使用不动点来描述。我们设L是完全格并设f是从L到L的单调函数。则任何x′使得f′(x′) ≤x′是f的最小不动点的抽象，它依据Knaster-Tarski定理而存在。

困难现在是获得这样的x′。如果 L' 是有限高度的，或最多检验“升链条件”(所有上升序列最终都固定)，则这样的x′可获得为通过如下归纳法定义的上升序列x′n的固定极限:x′0=⊥ (L′的最小元素) 并且x′n+1=f′(x′n)。

在其他情况，仍有可能通过拓宽算子∇ 来的得到这种x′: 对于所有的x和y，x∇y应当大于等于x和y二者，并且对于所有序列y′n，定义自x′0=⊥ 并且x′n+1=x′n∇y′n的序列最终是固定的。我们接着选取y′n=f(x′n)。

在某些情况，有可能使用伽罗瓦连接(α, γ) 来定义抽象，这里的 α 是从L到L′而 γ 是从L′到L的单调函数。这假定了最好抽象的存在性，这不是必然的情况。例如，如果我们通过套入凸多面体抽象实数对 (x,y) 的集合，则对于x+y≤ 1 定义的圆盘没有最优抽象。2

本词条内容贡献者为:

王沛 - 副教授、副研究员 - 中国科学院工程热物理研究所