抽象解释
在计算机科学中，抽象的解释是基于有序集（尤其是晶格）的单调功能的计算机程序语义的声音近似理论。它可以看作是计算机程序的部分执行，该程序在没有执行所有计算的情况下获得了有关其语义的信息（例如，控制流，数据流）。
它的主要具体应用是正式的静态分析，即有关计算机程序可能执行的信息的自动提取；这样的分析有两个主要用途：
1970年代后期，法国计算机科学家帕特里克·科索特（Patrick Cousot）和拉迪亚·科索特（ Radhia Cousot）正式化了抽象的解释。
直觉
本节说明了通过现实世界中非计算示例的抽象解释。
考虑会议室里的人。假设房间中每个人的唯一标识符，例如美国的社会安全号码。为了证明某人不存在，所有人要做的就是查看其社会保险号是否不在列表中。由于两个不同的人不能拥有相同的数字，因此只需查找他或她的号码，就可以证明或反驳参与者的存在。
但是，可能只有与会者的名字被注册。如果在列表中找不到一个人的名字，我们可以安全地得出结论，那个人不在。但是，如果是的话，由于可能会有异义词的可能性（例如，两个叫约翰·史密斯的人），我们将绝对得出结论。请注意，此不精确的信息对于大多数目的仍然足够，因为在实践中拼音很少。但是，总的来说，我们不能确定房间里有人在场。我们只能说他或她可能在这里。如果我们要查找的人是罪犯，我们将发出警报。但是当然有可能发出错误警报。在计划分析中将发生类似的现象。
如果我们只对某些特定信息感兴趣，例如“房间里有一个年龄n的人？”，请保留所有姓名和分娩日期的清单。我们可能会安全，而不会丧失精确度，将自己限制为保持参与者年龄的清单。如果这已经太多了，我们可能只保留最年轻的M和最大的人的年龄。如果问题严格低于M或严格高于M的年龄，那么我们可以安全地回答没有此类参与者在场。否则，我们可能只能说我们不知道。
在计算的情况下，混凝土，精确的信息通常在有限的时间和内存中不可计算（请参见Rice的定理和停止问题）。抽象用于允许对问题的广义答案（例如，当我们（抽象解释的算法）无法确定地计算出精确的答案时，将“也许”回答是/否问题，意思是“是或否”）；这简化了问题，使它们可以自动解决方案。一个至关重要的要求是增加足够的模糊性，以使问题可以管理，同时仍然保留足够的精确度来回答重要问题（例如，“可能会崩溃？”）。
计算机程序的抽象解释
给定编程或规范语言，抽象解释包括给出通过抽象关系链接的几种语义。语义是该程序可能行为的数学表征。最精确的语义非常紧密地描述了程序的实际执行，称为具体语义。例如，命令式编程语言的具体语义可以与每个程序相关联。执行跟踪集 - 执行跟踪是该程序执行的一系列可能连续的状态；状态通常由程序计数器和内存位置（全球，堆栈和堆）的值组成。然后得出更多抽象的语义。例如，可以仅考虑执行中的一组可及的状态（这等于考虑有限迹线中的最后状态）。
静态分析的目的是在某个时候得出可计算的语义解释。例如，人们可以选择通过忘记变量的实际值而仅保留其符号（+， - 或0）来代表程序操纵整数变量的状态。对于某些基本操作，例如乘法，这样的抽像不会失去任何精确度：要获得产品的迹象，就足以知道操作数的符号。对于其他某些操作，抽象可能会失去精度：例如，不可能知道其操作数分别为正和负面的总和的迹象。
有时，必须丧失精确度以使语义能够确定（请参见Rice的定理和停止问题）。通常，在分析的精度及其可定性（可计算性）或障碍性（计算成本）之间存在妥协。
实际上，定义的抽像是针对一个人想要分析的程序属性和目标程序集的量身定制的。对计算机程序进行抽象解释的第一个大规模自动分析是由事故发生的，这导致了1996年Ariane 5火箭的第一次飞行。
形式化
令L为有序集，称为混凝土集，让L '为另一个有序集，称为抽象集。这两组通过定义将元素从一个到另一个映射的总函数相互关联。
如果函数α将其映射到混凝土集中的元素x中l '中的元素α（ x ），则称为抽象函数。也就是说， l '中的元素α（ x ）是x中x的抽象。
如果函数γ将元素x'映射到抽象集l '中的元素x '中，则称为混凝土函数，将其映射到混凝土集合中的元素γ（ x '）中。也就是说， L中的元素γ（ X '）是L '中X '的混凝土。
令L 1 ， L 2 ， L' 1和L' 2订购。混凝土语义F是从L 1到L 2的单调函数。如果对于L' 1中的所有X '，（ f∘γ ）（ x '）≤（ γf '）（ x '），则认为从l' 1到l' 2的函数f '被认为是F的有效抽象。 ）。
通常在存在循环或递归程序的情况下使用固定点来描述程序语义。让我们假设L是一个完整的晶格，让F是从L到L到L的单调函数。然后，任何X '这样， F （ x '） ≤x '是根据用于纳斯特– tarski定理的F （x'）≤x'的最小固定点的抽象。
现在的困难是获得这样的X '。如果L '的高度为有限的高度，或者至少验证上升链条件（所有上升序列最终都是固定的），则可以作为通过感应定义的上升序列x'N的固定限制获得的X ' ，如下所示： x'0 =⊥（ L '的最小元素）和x'n +1 = f ' （ x'n ）。
在其他情况下，仍然可以通过扩大的操作员获得这样的X '：对于所有x和y ，x y y， x y y应该比x和y都大或相等，对于任何序列y'n ，序列由x' 0 =⊥和x'n +1 = x'n y'n定义。最终是静止的。然后，我们可以服用y'n = f ' （ x'n ）。
在某些情况下，可以使用GALOIS连接（α，γ）定义抽象，其中α是从L到L '，γ是从L '到L。这假定存在最佳抽象，这不一定是这种情况。例如，如果我们通过封闭凸多面体来抽象实数的夫妇（ x ， y ），则没有x 2 + y2≤1定义的光盘的最佳抽象。
抽象域的示例
数值抽象域
一个人可以分配给给定程序点的每个变量x，一个间隔[ l x ， h x ]。如果对于所有x ， v （ x ），将值v （ x ）分配给变量x的状态将是这些间隔的具体化。从变量x和y的间隔[ l x ， h x ]和[ l y ， h y ]中，一个人可以轻松获得x + y （[ l x + l y ， h x + h y ]）的间隔，而对于x -y （[[ l x -h y ， h x -l y ]）;请注意，这些是精确的抽象，因为例如x + y的可能结果集，正是间隔（[ l x + l y ， h x + h y ]）。可以得出更复杂的公式，用于乘法，除法等，从而得出所谓的间隔算术。
现在让我们考虑以下非常简单的程序：
y = x; z = x - y;
 |
 |
对于合理的算术类型， Z的结果应为零。但是，如果我们从[0，1]中的x开始进行间隔算术，则在[-1，+1]中获得z 。虽然每个采用的每个操作都被完全抽象了，但它们的组成却不是。
问题很明显：我们没有跟踪X和Y之间的平等关系；实际上，这个间隔的域未考虑变量之间的任何关系，因此是一个非关系域。非关系域倾向于快速，易于实施，但不精确。
关系数值抽象域的一些示例是：
及其组合（例如减少产品，参见右图）。
当人们选择一个抽象领域时，通常必须在保持细粒度的关系和高计算成本之间取得平衡。
机器词抽象域
虽然诸如Python或Haskell之类的高级语言使用默认情况下使用无界整数，但较低级别的编程语言（例如C或Assembly语言）通常会在有限尺寸的机器单词上操作，这些单词更适合使用整数模型（其中N是N是n是n机词的位宽度）。有几个抽象域适用于此类变量的各种分析。
比特菲尔德域分别用机器单词对待每个位，即宽度n的单词被视为n个抽象值的数组。抽象值是从集合中获取的，抽象和具体函数由以下方式给出：，，，。这些抽象值的位操作与某些三值逻辑中的相应逻辑操作相同：
|
|
| ||||||||||||||||||||||||||||||||||||||||||||||||||
其他域包括签名的间隔域和未签名的间隔域。所有这三个域都支持向前和向后抽象运算符，以进行常见操作，例如加法，偏移，XOR和乘法。这些域可以使用还原产品组合。