抽象解释及其在程序分析中的应用

网址：http://www.elsevier.nl/locate/entcs/volume59.html15页隶属方程逻辑Bernd Fischer和Grigore Ro su高级计算机科学研究所自动化软件工程组NASA艾姆斯研究中心美国加利福尼亚州莫伊特菲尔德，邮编：94035，地址：fisch，grosuptolemy.arc.nasa.gov摘要我们提出了一个逻辑框架，在这个框架中，抽象的解释可以被自然地具体化，然后被验证。我们的方法是基于成员资格方程逻辑扩展方程逻辑的成员公理，断言一个术语有一定的排序。我们把抽象的解释表示为一个隶属方程逻辑规范，通常表示为一个具有成员公理的重载有序签名。事实证明，对于任何项，它在这个指定上的最小排序对应于它最具体的抽象值。Maude实现了隶属关系等式逻辑，并提供了计算项ef的最小排序的机制。最近。我们首先展示了如何使用Maude免费获得抽象解释的原型。“在Maude的元逻辑设施的基础上，我们进一步开发了一个工具，可以自动检查一组用户定义的属性的抽象解释。这可以用来选择适当的抽象解释，描述抽象过程中特定的信息损失，以及比较不同的抽象。1引言抽象解释[5]已经成为各种程序分析技术的统一框架。它也越来越多地应用于计算机科学的其他领域，例如，[2][3][4][5][6][7][8][9][10]它的吸引力恰恰在于它所涉及的抽象，它简化了计算和搜索，从而使我们能够有效地找到问题的近似但正确的解决方案，否则这些解决方案可能会太难。然而，在实践中，往往微不足道不同的抽象或不同的权衡之间的有效性和近似，往往可以验证和评估，只有与一个原型实现的抽象解释。一c 2001年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。2对抽象的更详细的评估，例如，以正确性或完整性证明的形式，甚至需要对形式验证的支持在本文中，我们将解决这些验证和验证问题。我们展示了抽象解释是如何在代数方程逻辑（MEL）[11，1]中被指定和解释的，MEL是一种表达逻辑，它概括了代数规范技术中使用的各种形式的方程逻辑。通过这种重新解释，我们可以使用Maude系统[4，3]作为执行抽象规范的环境，或者换句话说，我们免费获得了一个原型环境。“我们进一步开发了一种工具，它使用Maude的元逻辑功能来验证抽象解释对也被指定为MEL句子的属性。更准确地说，我们提供了一个Maude模块，允许我们编写命令，Maude> reduce验证抽象上的属性。其中，ABSTRACTION是抽象解释的规范，PROPERTIES是另一个MEL规范。verifyon返回一个警告列表，显示抽象解释违反的PROPERTIES中的所有句子，以及（抽象）反例。在这个阶段，我们可以看到这样一个工具的三个应用，这取决于规范PROPERTIES实际代表的内容：如果PROPERTIES是一组抽象解释为了在特定上下文中使用而应该具有的期望属性，那么我们可以使用我们的工具从库中检索满足它们的抽象解释;如果PROPERTIES是具体领域的公理化表示，那么我们可以使用该工具来查看抽象丢失了多少信息和什么样的信息，然后决定它是否可用于特定任务;如果PROPERTIES是同一个具体域的另一个抽象解释，那么空的警告列表意味着ABSTRACTION是第二个抽象。我们方法的基本思想相对简单。如果我们把抽象的解释看作一个格，那么一个排序与格中的每个节点相关联，一个子排序与每个边相关联。定义抽象操作的表被一系列重载运算符替换，而表无法捕获的特性则通过MEL语句声明。排序底部阴性阳性真实值。子分类底部<阴性阳性<真实值。op_+_：阴性->阴性。op_+_：位置位置->位置op_*_：阴性阳性->阴性。op_*_：阴性->阳性op_/_：Real Real -> Real。op_/_：实零->底部。mbX/X：位置1。是通常的符号抽象的一个片段1.一个前的抽象价值1 这里使用的精确形式将在后面解释。3具体域中的表达式对应于其在指定签名上的最小排序; Maude提供了一种有效的自动最小排序计算。我们的方法抽象的解释MEL是更面向逻辑比通常的面向格的方法。我们主张一个松散的语义规范对应的抽象解释。那么，预期的抽象解释只是规范的一个模型，即除了子分类声明所要求的包含载体的结果之外，为每个载体添加一个新元素的模型。另一种模型是将具体域构造成子集的模型 相同类型的元素”。因此，该模型类似于通常在面向格的方法中用作具体域抽象解释的最终目标是简化对具体领域的推理。因此，我们倾向于根据需要向规范中添加尽可能多的作为具体域的有效属性的句子，而不是精确地添加那些使预期的抽象解释成为初始模型的句子。我们的方法不需要结构上的具体域和抽象域不需要是一个完整的格或下半格。相反，相关联的规范被期望是正则的[1]，以便Maude正确地计算项的最小排序。有趣的是，排序上的偏序是一个格，这一事实在实践中对正则性来说是足够的。我们在这里的工作代表了对MEL中的抽象解释进行全面重新解释的第一步。 我们的方法目前仅限于nite数量的排序，或抽象类型，我们还不能处理xpoint运算符。这些限制将受到进一步调查。 本文的重点是在工具方面，而不是在理论方面。本文的其余部分组织如下。在下一节中，我们简要地介绍了成员方程逻辑和莫德系统的基本概念和符号，只要它们是我们的目的所需要的。然后，我们在第3节中展示了抽象解释如何被视为隶属代数。第4节显示了如何将MEL规范与抽象解释相关联，以及如何在该规范级别自动计算抽象类型。第五节最后讨论了如何在本文提出的框架中验证抽象解释。2隶属方程逻辑与Maude成员关系方程逻辑[11，1]扩展了多排序方程逻辑[8]，其中成员关系断言t：s声明项t属于排序s。 它包含了各种各样的规范形式主义，包括序排序[7，9]和部分方程逻辑。尽管它的通用性，它仍然享有良好的性质方程逻辑：它是简单的，有效地实现，4S承认健全和完整的演绎以及自由的模式。在本节中，我们非正式地介绍了成员等式逻辑和一些使用的我们假设基本熟悉多分类等式逻辑。在隶属方程逻辑中，排序被分组在种类中，操作被定义在种类上。一个签名由一个集合S的种类，一个集合K的种类，一个映射S！K和K？k-指标集=fw; kj（w; k）2K？公斤的操作。一个-代数是一个-代数A加上一个子集AsAk对于每个k2 K和每个s21（k）.对于任意K-指标的变量集X，T（X）是通常的（Ki）-项代数。MEL语句通过所有的隶属断言推广了方程逻辑的条件方程（8X）t=t0ifC.它们是形式为（8X）t：s的普遍量化Horn子句，如果C。在这两种情况下，条件C都是一个集合fu1 =v;：; u=v; t：s;：; t：sg和t;t0; t;：t; u; v;：; u; v是这样的术语1nn11mm1m11nn在T（X）中。 如果n = m = 0，那么这个句子被称为无条件的或原子的。在这一段中，我们只讨论原子句子的满足;一般情况很容易理解。对于-代数A和赋值a：X！我们用的是？：T（X）！A表示A到（K;）-代数的一个态射的唯一扩张. 是否有A满足（8X）t=t0（或（8X）t：s）当且仅当对于每个赋值A我们也有A？（t）=a？（t0）（或a？（t）2A）。一个MEL规范或理论是一对（;），其中是一组-句子，它定义了一类-代数（满足它的代数），记为Alg（;）。MEL的证明理论是从标准的证明理论的平等理性逻辑它的显著特点是除了标准的词项等价性外，还允许对词项的成员资格进行分类推断。 给定一个指定（;），有两个推理规则可以帮助实现这一点。 一是肯定前件推理规则的一个修改，一旦它的条件被证明，就从（条件）句子中推导出成员资格。 第二个规则是外延性规则，它断言相等的项具有相同的排序。成员：`（8X）t=t0`（8X）t：s（8X）t0：sMaude [4，3]是OBJ家族[10]中的一个高性能重写系统，它支持成员关系方程逻辑和重写逻辑。它的当前版本在标准硬件上每秒可处理多达300万次重写本文用Maude符号表示隶属方程逻辑中的抽象解释，并对其进行验证。下面介绍一些符号约定。等式和条件等式分别通过关键字eq和ceq声明;成员资格和条件成员资格断言通过mb和cmb声明。可以使用mix-x表示法声明操作。它们也可以被重载;但是，这只是适当的条件成员关系断言的语法糖例如，* ：如果X：Pos和Y：Neg，则Pos Neg -> Neg可以被cmb X * Y：Neg替换，其中 * 由适当的种类定义。 var X：S形式的声明用于引入变量;它们的作用域是有界的5（1;+1）？一号？，0？+1？由fmod引入的封闭模块.端类型不需要显式声明。它们被自动计算为子排序声明所定义的偏序的连通分量。允许顺序排序和运算符重载的规范形式主义的一个典型问题是，某些项可能同时具有不同的正确排序。项的可能种类可以使用MEL的完整演绎系统来推导，即，sort（t）是集合fs 2S j（8X）t：sg.一个specication（;）被称为正则的当且仅当对于每个项t，sort（t）要么是空的，要么有一个最小元素w.r.t. subsort关系关于正则性的详细讨论可以在[1]中找到，以及可判定性结果和暗示正则性的各种句法标准。Maude实现了其中的一些标准。因此，我们可以假设每个有效的规格是正规的，我们可以计算任何项的最小排序。3作为-代数的为了说明我们的方法，我们描述了一个广义的符号/范围抽象的实数，其中的正数和负数被分成大和小。 这种解释是我们在统计数据分析领域的程序合成系统中实现的更复杂解释的简化版本[6]。 在这个域中，概率（即， 区间[0; 1]），因此实数"\0”和“\1”是特别感兴趣的。为了正确地处理除以零，我们需要对实数做一个我们可以把除法看作是部分函数而不改变实数集，也可以看作是全函数，在这种情况下，我们需要在实数中添加一个新元素来表示不必要性。为简单起见，我们选择第二个假设;请注意，MEL也支持XML，因此我们的选择并不反映框架的限制让？是表示“under ned”的特殊符号;我们使用相同的符号？ 对于集合f？g，让我R？ 表示实数n的集合加上？. 抽象域则由IR？ 其中c，h是通过包含部分排序的。实数的每个区间也包含？，反映了一个表达式的结果可以是该区间内的一个数或该区间下的一个数的这个域通常可以用下面的格表示：（1;0]？、、、、[0;+1）？（1;1]？、、、【1;0】？Ccc【0;+1】？、、【+1;+1）？、、Ccc、、、、、、、、、？6X=Y（1;1）（1;0][0;1）（1;1）[1;0][0;+1][+1;1）10+1个？（1;1） （1;1）（1;1）（1;1）（1;1） （1;1） （1;1）（1;1）（1;1）？（1;1）？（1;0） （1;1）[0;1）[0;1） （1;1）（1;0）（1;1） （1;1）[0;1）[1;0] （1;1）[0;1）【0;+1】 （1;1）（1;0）[0;1）（1;0）（1;0）[0;1）[0;1）？[0;1）（1;0）[0;1）[0;1）（1;0]（1;0）（1;0）[0;1）[0;1）【+1;1）（1;1）（1;0）[0;1）（1;0]（1;0）[0;1）（1;0）（1;1）【+1;1）[0;1）什么？（1;0）什么？（1;0）什么？[0;1）什么？（+1;1）什么？（1;1]？【0; +1】？[1; 0]【0;+1】0[1; 0]？【+1;1）（1;1）00000[1; 0]【0;+1】[0;1）[1; 0]0【0;+1？+1个01？？？10+1个？？？+1个 （1;1）（1;0）（1;1）【+1;1）？？？？？？？？？我们现在可以提供操作的抽象版本。典型的、简明的方法是用表格，例如下面的第2部分表格：然而，众所周知，表通常不足以完全描述抽象操作的预期行为。例如，不可能指定X=X的抽象值为+1？. 因此，抽象变得不像人们希望的那样精确。我们将在下一节中展示MEL如何允许我们使用成员关系断言来指定此类属性。在MEL的上下文中，将晶格和这些表与作为适当签名上的-代数的抽象解释相关联。这种一般的代数观点使我们可以自由地把抽象解释看作是（;）- speci cation的“一个特定模型”。由于一个规范可以有许多不同的模型，这也允许我们将不同的抽象相互联系起来。在本节的其余部分，我们将集中展示抽象解释如何被视为- 代数 在接下来的部分中，我们将展示MEL规范如何可以自然地与一个预期的抽象解释相关联，以及我们如何在该规范的级别而不是在抽象模型的级别上证明属性。格实际上给了实数的最初具体域一些结构。现在，通过为网格中的每个节点提供排序并使用子排序关系来反映网格结构，将MEL签名与上述网格相关联是很自然的。在Maude中，这表示为：sort实数-=^阴性-=^阴性-l-=^Neg-s-=^负一--位置-=^Pos-l-=^Pos-s-=^一号位置--零-=^屁股了. --（1;+1）？（1;0]？（1;1]？【1;0】？一号？[0;+1）？【+1;+1）？【0;+1】？+1？0吗？？2由于某些地理原因，我们省略了？- 下标在这里。7？子分类为阴性阳性<实型。子分类Neg-oneReal。op-_：Real-> Real。现在，扩展实部数IR？ 可以看作是一个-代数A如下。 对于每一种s，我们定义NE作为其载体A s的适当子集的IR？. 例如，我们定 义为Ak=AReal=IR？，APos=IR+=fx2IRjx0或x =？g等等，直到我们得到ABottom = f？G. A的操作是在IR上的常用算术运算. 请注意，大多数运营商在夜间设置。然而，A并不是我们能构造的唯一有趣的-代数我们也可以使用区间本身，而不是使用各个区间内的实数集作为载体因此，我们得到ABottom = B Bottom =f 。 g 和 APos-one=BPos-one=f+1; ？ g 但 BPos-s=f[0;+1];0;+1;？g和BPos-s=f[+1;+1];+1;？G，等等。因此，B的载波Bk是nite。|事实上，它由与晶格完全相同的11个元素组成。B的运算是通过运算符表来定义的，例如除法表。上面两个-代数A和B的主要区别显然是B是nite.因此，它在实践中很容易处理，但它丢失了关于实数的具体域的信息，因此实数的许多A只是构造了具体的域，但仍然承担了直接分析实数的所有负担理想情况下，我们希望保留两个代数，而不是像实践中经常发生的那样，只丢弃A而保留B。接下来我们将展示MEL是一个框架，在此框架下，我们可以编写一个（nite）规范，该规范接受A和B作为模型。这个规范可以被看作是具体域的一个抽象，它可以根据需要包含域的许多属性4翻译抽象的解释我们在上一节的例子中展示了我们的技术。在Maude中，我们从一个模块ABSTRACTION-REAL开始，通过排序和子排序将抽象域定义为偏序：fmod ABSTRACTION-REAL是sort实数负位置负-l位置负-l位置负-s位置负-s位置负-1 0位置负-1底部。子排序Neg-one使用成员关系断言定义的Real：保护真正的罪犯op|_|：MachineReal ->Real。瓦尔河：MachineReal。MB|：零。| : Zero.MB|一号岗位。|:Pos-one . MB|-1个|：负一。CMB|：如果R = -1，则为负-1。|: Neg-l if R <= -1.CMB|R|：如果R >=-1且R< = 0，则为Neg-s。CMB|R|：Pos-s，如果R >= 0且R< =1。CMB|R|：Pos-l，如果R >= 1。注意|0 |0的抽象可以有三种：Zero、Neg-s和Pos-s。但是，Maude会自动计算每个术语的最小排序，|0|排序为零。下一步是抽象定义在具体域上的运算，在我们的例子中是加、乘、反、减和除。我们通过使用运算符重载来做到这一点，这基本上代表了一种优雅的方式来编码经常用于定义抽象解释的表：op _+_ ：底部真实->底部。op _*_ ：底部真实->底部。op _+_ ：实际底部->底部。op _*_ ：实际底部->底部。op _+_ ：负一零->负一。op _*_ ：负一位置负一op _+_ ：零负一负一op _*_ ：Pos-one Neg-one -> Neg-one.op _+_ ：零->零。op _*_ ：真零->零。op _+_ ：负一位一零op _*_ ：零实数->零。op _+_ ：正一负一零op _*_ ：一号位置一号位置一号位置op _+_ ：Pos-1Zero-> Pos-1。op _*_ ：负一负一正一op _+_ ：零位置1->位置1。op _*_ ：阴性-l阳性-l->阴性-l。op _+_ ：阴性-l阴性->阴性-l。op _*_ ：Pos-lNeg-l-> Neg-l。op _+_ ：阴性阴性-l->阴性-l。op _*_ ：Neg-s Pos-s -> Neg-s。op _+_ ：阴性零->阴性。op _*_ ：Pos-s Neg-s -> Neg-s。op _+_ ：零负->负。op _*_ ：Pos-s Pos-s -> Pos-s。op _+_ ：Pos-s Zero -> Pos-s。op _*_ ：Neg-s Neg-s -> Pos-s。op _+_ ：零Pos-s -> Pos-s。op _*_ ：阴性-l阴性-l->阳性-l。op _+_ ：Pos-l Pos-l。op _*_ ：Pos-l Pos-l -> Pos-l。op _+_ ：Pos-l -> Pos-l。op _*_ ：阴性阳性->阴性op _+_ ：阴性阴性->阴性。op _*_ ：阳性阴性->阴性op _+_ ：阴性-l阳性-s->阴性op _*_ ：位置位置->位置op _+_ ：Pos-s Neg-l -> Neg.op _*_ ：阴性阴性->阳性op _+_ ：位置位置->位置op _*_ ：真实真实->真实。op _+_ ：Pos-l Neg-s -> Pos.op _+_ ：阴性-阳性-l->阳性op _+_ ：真实真实->真实。在这种情况下，我们能够完全通过运算符重载来定义加法和乘法的预期抽象（即，表格形式）。然而，在实践中，表格通常不足以正确地定义运算符的抽象版本。运算符的某些重要的域特定属性不能仅通过其参数的抽象类型来指定。例如，没有办法声明X/X的抽象类型是Pos-one9只不过是分析除法（的抽象）的arity（或table）。幸运的是，成员关系等式逻辑允许我们声明成员关系为- sertions，然后可以用来推断抽象项的最小类型：op -_：Bottom -> Bottom。op -_：Pos-one -> Neg-one。op -_：Zero ->Zero。op -_：Neg-one -> Pos-one。op -_：Pos-l -> Neg-l。op-_：Pos-s-> Neg-s。op-_：Neg-s-> Pos-s。op -_：Neg-l -> Pos-l。op -_：阳性->阴性op-_：阴性->阳性op-_：Real -> Real。变量X Y：真实。mb X +（-X）：零。op _-_：Real Real ->Real。等式X-Y= X +（-Y）。op_/_：BottomReal->Bottom 。 op _/_ ： 实 零 -> 底部。op _/_ ： Neg-one Pos-one-> Neg-one 。 op _/_ ： Pos-one Neg-one ->Neg-one。op _/_：零实数->零。op_/_ ： Pos-onePos-one->Pos-one 。 op _/_ ： Neg-one Neg-one ->Pos-one。op _/_：Neg-l Pos-s -> Neg-l。op _/_：Pos-l Neg-s -> Neg-l。op _/_：Neg-s Pos-l -> Neg-s。op _/_：Pos-s Neg-l -> Neg-s。op _/_：Pos-s Pos-l -> Pos-s。op _/_ ： Neg-s Neg-l -> Pos-s.op _/_：Neg-l Neg-s -> Pos-l。op _/_：Pos-l Pos-s -> Pos-l。op_/_：阴性阳性->阴性op_/_：阳性阴性->阴性op _/_：阴性->阳性op_/_：Pos Pos-> Pos.op_/_：Real Real-> Real。mb X/X：位置1。mb（-X）/X：负一。endfm注意，我们可以使用等式\eqX-Y= X +（- Y）。“以符合其具体定义的方式消除抽象减法，从而减少规格的大小。这里值得一提的是，Maude提供了内部算法来确保签名的规则性，并且在测试上面的重载签名时，它多次警告我们签名不规则。经过仔细检查，我们发现我们的“表”是不一致的，在这个意义上，某些具体的表达式不可能有一个最精确的抽象值。例如，我们忘记添加 *的第三个声明;然后Maude发出警告说正则性检查失败：确实，负1和正1的乘积可以在集合fNeg-s，Neg-l，Neg，Realg中有任何排序，但这个集合没有最小元素。因此，定期检查有助于我们涵盖所有情况。 我们强烈地认为，在有序重载签名的正则性与抽象解释的大多数具体抽象值的存在性之间存在着深刻的关系，其中抽象值形成格，并且这种关系值得研究。上面的模块现在可以用作抽象表达式的决策过程。以下是几个例子，说明它是如何工作的：红色|1 - 1页|.红色|二、二|.红色|1|- -一种|1|.红色|2|- -一种|2|.红色|1|+的|-1个|.红色|2|+的|-2个|.红色（|-1个|+的|1|）+|1|.红色|-1个|+（|1|+的|1|）10的。11红色|-2个|/（|3|//下一页|3|）的。红色（|-2个 |** |3|）/|3|.前五个表达式都被正确地抽象为零;也就是说，它们都简化为排序为零的项，但是出于不同的原因：前两个简化为| 0 |其排序为零，接下来的两个rst使用等式eq X-Y = X +（-Y）来消除减法，然后使用成员关系断言mb X +（-X）：零，最后一个rst计算|1|和|-1个|然后使用声明操作+ ：Pos-one Neg-one -> Zero。的以下是其他ve约简的Maude输出：resultReal：|2|+的|-2个|结果Pos-one：（|-1个|+的|1|）+|1|结果阳性：|-1个|+（|1|+的|1|）结果阴性-1：|-2个|/（|3|//下一页|3|）result Neg：（|-2 个|* * |3|）/|3|以上的简化反映了抽象解释会丢失信息的直觉。例如，由于2和-2的最具体的抽象值分别是Pos-l和Neg-l，因此我们不能对|2|+的|-2个|，所以返回的类型是Real。接下来的两个约简表明，加法的抽象不再是关联的，这是我们在数据分析综合系统中遇到的一个意想不到的问题。最后，最后两个约简表明，具体域的其他预期方程性质在抽象层次上也不成立，在这种情况下，方程eqX/（Y/Z）=（X * Z）/Y。5抽象解释由于通过抽象具体领域，实际上会丢失信息，因此一个自然而重要的问题是“丢失了多少信息？”“. 这是这是一个既要提出又要回答的复杂问题，而且可能有新的理论结果在背后; 2我们决定采取务实的态度，开发一个环境，在这个环境中，人们可以测试一个抽象的解释，作为一个Maude模，用于各种方程或不期望满足的性质。例如，假设考虑以下性质（也写为Maude模）：fmod PROPERTIES是排序Pos Neg Real。子排序Pos Neg真实。ops（_+_）（_-_）（_*_）（_/_）：Real Real->Real。vars X Y Z：Real.等式X + Y = Y +X。*>true等式X * Y = Y *X。*>true等式X +（Y + Z）=（X + Y）+Z。*>错误等式X *（Y * Z）=（X * Y）* Z。*>真等式X *（Y + Z）=（X * Y）+（X * Z）。*> falseeq-（-X）= X。*>true等式X *（-Y）=-（X * Y）。*>true等式（-X）/Y =-（X/Y）。*>true等式（X/Y）/Z = X/（Y * Z）。*>true12等式X/（Y/Z）=（X * Z）/Y。*>假等式（X +Y）/Z=（X/Z）+（Y/Z）。*>错误等式X * X = X * X * X *X。*>truemb X * X：位置*>truemb（（X * X）+（Y * Y））+（X * Y）：位置 *> falsemb（X-Y）*（Y-X）：Neg.*>错误endfm为了写出抽象解释的所需性质，我们只需要知道我们想要引用的排序和操作。请注意，只有最后三个属性才需要排序Pos和Neg，因此如果对成员资格属性不感兴趣，可以删除它们。在我们前面的抽象解释中，Real的主排序有10个子排序，这是抽象的一部分，而不是它所期望的属性w.r.t.。 具体领域。由于人们可能想测试相同的属性对许多不同的抽象解释相同的域，并选择一个最好的TS一个人的目的，一个应该是指尽可能少的排序专用于只有一个抽象时，写属性。现在可以使用简单的命令根据上一节中红色验证ABSTRACTION-REAL上的属性。在第一次加载后，定义操作verifyon及其语义的模块，其实现在附录中简要介绍。上面模块中的ftrue，falseg注释总结了此命令的执行。事实上，对于上面的每一个属性，Maude检测到了所有的反例，即，X，Y，Z的可能抽象值），这违反了它;总共有780个反例，Maude在1.5GHz的Linux机器上花了大约30秒才找到所有反例。例如，当X：Neg-one，Y：Pos-one，Z：Pos-one时，加法的结合性不成立，当X：Pos-one，Y：Poss，Z：Zero时，最后一个成员关系断言不成立。有趣的是，请注意最后一个方程对所给出的抽象解释成立，即使它对实数的具体域不成立我们从这个系统的实验中学到的教训是，由于抽象而导致的信息丢失不仅反映在具体域的丢失属性上，而且反映在抽象所具有的在具体域中不成立的属性上。需要Maude的Meta级别来实现上述环境，即操作verify on的功能。在Meta级别上，模块只是FModule的排序项，因此验证on具有元FModule FModule ->，其中是警告列表。在我们当前的实现中，我们遍历第一个模块，对于每个等式或成员资格断言，我们取第二个模块并为变量生成所有可能的抽象排序，然后计算所涉及的项的最少排序（如果语句是等式，则为两个项，如果语句是成员资格，则为一个项）。如果语句是一个等式，则当且仅当两项13具有不同的最小排序，并且如果语句是成员资格断言，则当且仅当计算出的最小排序不小于或等于成员资格语句中指定的排序时，输出警告。有兴趣的读者可以查阅附录以了解更多的实施细节该工具仍处于实验阶段。我们的主要目标之一是保持它的简单和灵活性，以便轻松地将其应用于具体用途。我们目前可以预见该工具的三种应用，这取决于规范属性是什么：抽象解释检索。如果它是在需要抽象解释的具体情况下手动或自动生成的所需属性的集合，则可以使用我们的工具从库中自动检索满足要求的那些抽象解释;与具体领域的比较。如果它是具体领域的公理化表示，如自然数的Peano规范，那么人们可以使用该工具来理解或测试某个抽象解释丢失了多少信息和什么样的信息，然后决定它对于特定任务是否可以接受;抽象的解释。如果它是同一个具体域的另一个抽象解释，那么一个空的警告列表意味着ABSTRACTION是第二个抽象。6结论和今后的工作我们提出了一种新的方法来表示和验证抽象的解释。我们用一个有限隶属方程逻辑规范抽象了一个具体的域，在松散语义下，它也接受一般抽象解释作为模型，其抽象值形成一个格，其抽象运算由一个表给出。这个灵活的框架允许人们添加所需的具体域的属性，这些属性不能通过等式和成员断言被表捕获。然后，我们展示了如何使用Maude，一个实现隶属关系方程逻辑的高效重写引擎，来执行这样的规范，从而计算表达式的最具体的抽象类型（或最少的排序）。 基于元能力 的Maude，我们进一步实现了一个工具，通过该工具可以实际验证抽象解释，作为MEL规范，针对方程或成员属性。这样的工具可以用来从库中检索适当的抽象解释，描述由于抽象而导致的信息丢失，以及显示抽象解释的结果我们使用这种方法的编程合成工具，生成数据分析C程序从随机speci阳离子，为了象征性地证明算法模式的条件之前，他们被应用。然而，还有很多有趣的研究要做，以证明我们14为更广泛的实际情况提供方法。例如，我们不知道在这个阶段如何表示在nite抽象的解释，如任意整数区间。格的排序表示应该放弃吗？或者应该扩展成员资格等式逻辑以允许各种自由生成代数？在这种情况下，规律性意味着什么？我们没有研究的抽象解释的另一个重要方面是定点的计算。MEL签名的规则性与x点之间是否存在任何关系？致谢：我们感谢Jos e Meseguer和Steven Eker的鼓励和富有成效的讨论。 我们还要感谢Steven Eker为我们提供了Maude 2.0的alpha版本，它使用成员断言来计算最小的术语，因此我们可以测试我们的程序和声明。引用[1] Adel Bouhoula，Jean-Pierre Jouannaud，and Jos e Meseguer.隶属方程逻辑中的规范与证明。理论计算机科学，236：35{ 132，2000。[2] Edmund M.Clarke，Orna Grumberg，and David E.久了模型检查和抽象 。 ACM Trans. Programming Languages and Systems ， 16 （ 5 ） ：1512{ 1542，September 1994.[3] Manuel Clavel，F.放大图片创作者：John W. Mart-Oliet，Jos e Meseguer，and J. F.克萨达Maude系统在P. Narendran和M. Rusinowitch，编辑，Proc. 10th Intl.重写技术和应用，Lect.Notes Comp.Sci.第240页，意大利特伦托，1999年7月。斯普林格。系统描述。[4] Manuel Clavel，FranciscoJ. Duran，Steven Eker，Patrick Lincoln，NarcisoMart-Oliet，Jose Meseguer，and Jose F.克萨达Maude ：Speci cation andProgramming in Rewriting Logic，March 1999. Maude系统文档，请访问http://maude.csl.sri.com/papers。[5] Patrick M. 库索和Radhia Cousot摘要释义：通过构造或逼近不动点进行程序静态分析的统一格模型。第四届ACM Symp.《程序设计语言原理》，第238页，加利福尼亚州洛杉矶，1977年1月。Press.[6] Bernd Fischer，Johann Schumann，and Thomas Pressburger.从统计模型生 成 Walid Taha ， 编 辑 ， Proc. Intl. Semantics Applications ， andImplementation of Program Generation，Volume 1924 of Lect. Notes Comp. Sci.第212页，加拿大蒙特利尔，2000年9月。斯普林格。[7] 约瑟夫·戈根。有序代数技术报告14，UCLA计算机科学系，1978年。计算级数的语义学与理论。15[8] 约瑟夫·戈根和乔斯·梅塞格尔。多类等式逻辑的完备性。Houston Journal ofMathematics，11（3）：307{334，1985.[9] 约瑟夫·戈根和乔斯·梅塞格尔。有序代数I：多重继承、重载、异常和部分操作的等式推导。理论 计算机科学，105（2）：217{273，1992.[10] Joseph Goguen，Timothy Winkler，Jos e Meseguer，Kokichi Futatsugi，and Jean-Pierre Jouannaud.在Joseph Goguen和Grant Malcolm的编辑中，使用OBJ的软件工程：行动中的代数规范。Kluwer，2000年。[11] 乔斯·梅瑟格尔隶属代数作为方程说明的逻辑框架。在Proceedings，WADT'97 ， Lecture Notes in Computer Science 的 第 1376 卷 ， 第 18 页{61.Springer，1998年。[12] David A.伪装。抽象的定理证明。艺术Intell ，16（1）：47{ 108，1981.[13] Willem Visser，S.帕克和约翰·佩尼克斯使用谓词抽象来减少面向对象程序的模型检查。第三届ACM SIGSOFT正式研讨会论文集方法以软件实践，2000年8月。出现。一一些实现细节在本附录中，我们给出了一些关于如何实现操作verify on：FModuleFModule-> Bool的细节，该操作针对用户定义的属性（均表示为Maude模块）验证抽象解释。感兴趣的读者可以在www.example.com上下载本文中讨论的所有Maude源代码http://ase.arc.nasa.gov/grosu/download/absint-code.html。我们首先在Maude的Meta层上实现了一些辅助操作。下面的代码是不可执行的;由于空间限制，我们用三个点代替了简单的代码：fmodMETA-AUXILIARY包括META-LEVEL。...对VarDeclTuple进行排序。op|_|：VarDeclSet -> VarDeclTuple。...op getVarTuples：FModule VarDeclSet -> VarDeclTupleList。var M：FModule.var Var：VarDecl. var Vars：VarDeclSet。eqgetVarTuples（M，none）=|没有一|.eq getVarTuples（M，Var Vars）= mergeVarDeclSet（getVarsFromVar（M，Var），getVarTuples（M，Vars））。opmergeVarDeclSet：VarDeclSet VarDeclTupleList->VarDeclTupleList。op mergeVarDecl：VarDecl VarDeclTup