面向对象程序的容器数据结构操作的推理技术

理论计算机科学电子笔记131（2005）51-62www.elsevier.com/locate/entcs集值域马丁·里纳德2麻省理工学院计算机科学与人工智能实验室美国摘要当前面向对象语言的一个核心特性是能够动态实例化用户定义的容器数据结构，如列表、树和哈希表。这些数据结构的实现通常使用对动态分配对象的引用，这使得对结果程序的推理变得复杂。如果数据结构操作是根据与每个数据结构相关联的抽象对象集来指定的，那么推理就会简化。 例如，在这种方法中，插入到数据结构中变成简单地插入到对象的动态变化的集值字段中，而不是操纵附加到对象的动态链接结构。在本文中，我们将探索用于操作数据结构的程序的推理技术，这些数据结构使用与容器对象相关联的集值抽象字段来规范。我们基于1）一阶逻辑的可判定前缀词汇类，2）具有计数的双变量逻辑，以及3）多分类理论的Nelson-Oppen组合来比较特定语言的表达能力和复杂性。这样的规范逻辑可以用于验证具有提供的不变量的面向对象程序。此外，通过选择在这样的逻辑中可表达的属性的适当子集，这些逻辑的决策过程使得能够在抽象解释域中自动计算格操作，以及自动计算抽象程序语义。关键词：程序验证，数据结构，对象，决策过程，计数二元逻辑，经典决策问题，尼尔森-奥本技术，两级三段论1介绍现代面向对象编程语言的分析和验证提出了独特的挑战[29，18，24，11]。在本文中，我们研究了当前面向对象语言的一个中心特征：引入用户定义的1电子邮件：vkuncak@csail.mit.edu2电子邮件：rinard@csail.mit.edu1571-0661 © 2005由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2005.01.02252诉昆恰克湾Rinard/Electronic Notes in Theoretical Computer Science 131（2005）51抽象数据类型，并在程序执行期间创建这些数据类型的无限数量的实例。当每个数据类型实例本身使用多个动态分配的对象实现时，会出现特殊的困难，这些对象形成一个链接的数据结构。我们分析此类程序的方法是使用抽象集值场作为描述抽象数据类型操作的指定变量。我们将程序的分析分为：1）验证抽象数据类型的实现相对于集合规范的正确性，以及2）验证程序其余部分的正确性，其中链接数据结构被抽象集值字段替换。Hob项目。 Hob项目[17，32]背后的主要设计原则之一是，如果数据结构操作是根据与每个数据结构相关联的抽象对象集来指定的，那么对具有复杂数据结构的程序的推理就会变得更简单。例如，在这种方法中，插入到数据结构中变成简单地插入到动态改变的对象集合中，而不是操纵动态链接的数据结构。Hob将对具有这种数据结构的程序的验证分为两个任务：1）使用形状分析（或其他一些分析或验证技术，包括像交互式定理证明这样强大和重量级的技术）来验证数据结构实现是否符合抽象集变量的规定，以及2）在程序的其余部分中仅使用抽象集合变量来推理数据结构的行为。到目前为止，我们已经使用Hob来验证全局数据结构的实现，这些结构在编译时被实例化为有限数量的实例（可以存储和操作静态无限数量的对象）。对全局数据结构的关注使我们能够使用静态模块机制来封装对象场并防止表示暴露，以及使用布尔代数的可判定理论[13]来推理指定数据结构的抽象集的有限数量。这项研究的一个目标是扩展这种方法的动态实例化的数据结构以及。链接数据结构的动态实例化。 抽象数据类型的动态实例化是当前面向对象编程语言的主要特征之一。动态实例化通常通过将每个抽象数据类型实例与对象关联来实现，使用字段将底层链接数据结构附加到对象。这项研究探讨了一种方法来扩展Hob验证程序，使用链接的数据结构，可以动态实例化。在这种方法中，我们使用有限数量的集值对象字段来指定连接到对象的链接数据结构。使用这种技术抽象内容的结果是一个程序诉昆恰克湾Rinard/Electronic Notes in Theoretical Computer Science 131（2005）5153它操纵使用关系连接的对象。结果程序中的关系可以是一个函数（其给定对象的值是由对象值字段引用的对象），也可以是一个一般关系（其给定对象的值是存储在与该对象相关联的数据结构中的对象集）。Hob中数据结构的动态实例化的一般化需要扩展验证的两个阶段：1）验证链接的数据结构符合由对象字段的值给出的集合接口，2）验证使用具有集值字段的对象的结果程序。 为了解决第一个阶段，我们扩展了Hob中的现有技术，使用指定单个对象表示的技术[22，6，5，2，3];这些扩展是必要的，以确保在堆中存在其他实例的情况下，对一个实例的分析仍然有效本文的主题是第二个问题：验证用集值场操纵对象的程序像[26]一样，我们关注抽象数据类型的客户端的验证，但我们专注于用集值场表示的规范，并为我们类中的约束导出一个完整的决策我们的方法使用假设/保证推理和用户提供的注释，将类实现的分析与上下文的分析完全分离;其他方法试图自动推断上下文的近似和类实现的近似[18]，可能使用全局定点分析。集值场的决策过程。为了研究关于具有集值场的程序的推理的自动化，我们探索了这些场上的约束的决策过程。我们的约束可以表示与同一对象相关联的集合之间的关系、对象引用之间的别名以及与不同对象相关联的集合之间的关系。通过用这样的约束注释程序并使用验证条件生成器[32]，开发人员可以验证面向对象程序的一系列不变量通过选择一个适当的子集的属性express- ible使用这样的约束，这些约束的决策过程，使分析自动推导出的格操作的抽象解释域，并计算抽象程序语义（传递函数）。贡献和概述。为了激发本文中研究的约束，我们在第2节中给出了一个例子。我们在第3节中介绍了我们的正式设置。作为本文的主要结果，我们探讨了使用集值抽象字段的程序的推理技术我们比较了基于可判定前缀类的特定语言的表达能力和复杂性54诉昆恰克湾Rinard/Electronic Notes in Theoretical Computer Science 131（2005）51assumex/=nullx∈alloc;oldxc：= x. c、新y;其中，e [x/=nu ll很好。c=oldxc]（x. c/=100）{intn =nums（n）;//process（e）;insert（y，e）;}断言y. c=oldxc;Fig. 1.一个操纵集值场的示例程序片段。这里是Z。c表示与由ze：= removeFirst（x）：assertx.c/=n;havae;假设e∈ x。c、X. c：= x。c\{e}插入（y，e）：y. c= y。c{e}图二.图1中的过程调用规范一阶逻辑（第5节），计数的二元逻辑（第6节），以及多分类理论的尼尔森-奥本组合（第7节）。我们观察到，根据可确定的预紧类s[k，k，k]=和Nelson-Oppen组合，产生最优的NP算法来决定一个有趣的约束类另一方面，使用带计数的双变量逻辑允许更多表达性约束（例如字段永远不为空的约束），但通常需要NEXPTIME决策过程。我们在第8节中提出结论，并在整个论文中讨论相关工作。2例如图1给出了一个示例程序片段，其中包含一个前提条件（使用假设语句表示）、一个循环不变式（使用[... . 在while循环的条件前加上一个]括号）和一个后置条件（使用assert语句表示）。程序片段清空集合X. c并将其内容复制到集合y中。c（可以想象在每次循环迭代中对e的原始场进行一些处理，但这与我们的例子无关）。我们希望验证的属性是集合y的内容。c在程序片段的末尾等于集合x的原始内容。c，其存储在辅助集值局部变量oldxc中。该属性为true，因为过程调用removeFirst从x中删除了一个元素。c并在e中返回它，然后insert将相同的元素插入y。C.图2显示了过程调用的受保护命令规范，我们使用它来推理过程的效果;我们的系统单独验证过程符合它们的规范。给定图1中程序片段的前提条件、循环不变式和后置条件，我们可以生成验证条件，诉昆恰克湾Rinard/Electronic Notes in Theoretical Computer Science 131（2005）5155x/=yx/=nu lly/=nu llx。很好。c=oldxce∈x。cx/=y（x. c\{e}）c{e}）=oldxc图三. 图1中示例的循环保留验证条件O：：= VO|null|O.fOS：：=VS|S1和S2|S1和S2|S1\S2|{01， . .... . . 你 好 。 ，On} |O. fSf：：= Vf|fO [O1<$→O2] |fS [O→ S]A：：= O1 = O2|O∈S|S1 = S2|卡（S）≤k|f1 = f2F：：=A|F1和F2|F1和F2|€F见图4。 表达式和公式程序的后置条件成立图3显示了图1中程序的验证条件之一。请注意，生成的约束不仅需要推理单个集合的内容（如insert的语义），还需要推理对象(as在合取x/= y中）以及关于与不同对象相关联的集合之间的关系的推理（如在合取x中）。很好。c=oldxc）。在第3节中，我们定义了一类具有集值场的对象上的此类约束在本文的其余部分，我们研究了该类约束的有效性和可满足性问题。3规范语言图4显示了我们的规范语言的语法，用于用集值场来表达对象上的约束 我们的规范语言是类型化的（多分类的）;我们只关心类型良好的公式。非终端O表示可能为空的对象，S表示非空对象的集合，f表示场。域可以将对象映射到对象（然后它们被表示为fO），或者它们可以将对象映射到集合（然后它们被表示为fS）。我们使用公式（非终结符F）作为假设和断言语句、while循环的条件和if语句的一部分我们在赋值语句的右侧使用该语言的对象值和集值项（图4中的非终结符O和S）这种语言中构造的含义符号x.f表示对象x的场f的解引用，其可以被认为是函数应用，如果对象x为空，则信号是错误的。O[o1→o2]denotesanupdata的旋转一个对象值的域fO的更新操作，使得o1.fO=o2，并且同一个域对于所有其他对象的值都是相同的;如果我们把域f看作是由对象索引的对象的数组，那么这样的更新操作对应于数组更新。在我们的语言中，集合运算有标准的含义。 表达式中card（S）≤k，记法card（S）表示元素的个数（基数）56诉昆恰克湾Rinard/Electronic Notes in Theoretical Computer Science 131（2005）51，并且k表示非负整数常数。出于复杂性考虑，请注意我们用一元符号表示整数常数，因此常数k的长度为k，而不是logk。本文考虑的公式，其语法是由图4中的非终端F的有效性的决策程序。这些公式的有效性可以用来表示程序设计语言中验证条件的有效性。判定验证条件允许用循环不变式标注的面向对象程序的验证. 决策过程可以也可用于通过识别形成抽象域的有限公式集来合成循环不变量。如果S是有限谓词集，设D（S）表示S中所有公式的析取的集合，设B（S）表示S中公式的所有布尔组合的集合。如果S是图4的语言中的封闭公式的有限集合，则集合D（S）{true}和B（S）也是图4的语言中的公式，并且可以用作域。转移这 些 域 的 函 数 可 以 使 用 谓 词 抽 象 来 计 算 [1] 。 设 Q v1 ， ... ， vn （ S ）={\displaystylev1，.，vn. F|F∈ S}，设S是一组具有一元和二元函数符号的无数量因子公式. 则D（Q v1，.，vn（B（S）是可以用于符号形状分析的公式域[30]。类D（Q v1，...，vn（B（S）））以及B（Q v1，...，vn（B（S））可以使用[矩阵矩阵]=c las来决定第5节中使用的多个变量。4初步意见首先，我们对决定图4语言中公式的有效性进行几点观察。请注意，该语言在所有布尔运算下都是封闭的，因此我们只考虑满足性问题。我们的约束是无量化因子的，因此我们可以将满足性算法视为一个非确定性过程，该过程为无量化因子公式的原子选择一个令人满意的分配，并检查该令人满意的分配对应于一个令人满意的文字合取[8]。 通过这种方式，我们将约束的满足性降低为文字的合取的满足性。最后请注意，我们可以将每个字面量的合取转换为不包含嵌套项的等价合取。我们通过引入新的变量将公式转换为这种非嵌套形式;这些新的变量成为存在性量化的，因为我们正在考虑满足性。在最终的非嵌套形式中，每个原子式具有以下语法形式之一：V1=V2.fO，O OV S= V1<$V2，V S= V1<$V2，V S= V1\V2，V S={V1，...，V n}，V S= V O.f S，S S S S S O OV1=V2[V1<$→V2]，V1=V2[VO<$→VS]，V1=V2，VO∈VS，V1=V2，f fOOF FO O S S卡（VS）≤k，V1=V2. 在续集中，我们概述了可判定的连接词f f这些非嵌套公式及其否定式。 我们认为三个不同的诉昆恰克湾Rinard/Electronic Notes in Theoretical Computer Science 131（2005）5157方法. 我们最关注第一种方法（第5节）。5古典预科词汇课在本节中，我们概述了检查非嵌套文字的连接的满足性的第一种这种技术基于一阶逻辑中具有关系签名的泛公式类，没有非零元的函数对称我们将文字的合取转换为这类中的等价公式，同时引入有界数量的泛量化器（即，最多三个）。Theclass []=.Definenethelass[q]=作为所有形式为x1，.，xp. 第一，... 其中p≥0，F是一阶对数方程的无数量因子公式，方程y不含函数ymbol s. Let[]=bethe格公式q≥0[q]=。我们有以下几点：[258]Fact5.1F或任何固定edq，[k]的可满足性在NP中。Fact5.2[时间轴]=的可满足性以NEXPTIME表示。翻译的想法。将图4中的语言翻译为[类]=clas可以概括为以下内容：1）使用一元关系来表示集合，2）使用二元关系来表示对象值和集合值场，以及3）使用通用量化器来表示集合运算。为了使这种方法工作，我们需要正确地表示空引用，通过案例分析消除数组更新，并仔细地翻译基数约束以避免引入无限数量的量化器。为了确保对象值字段不会同时分配多个值，我们引入一个合取(1)x，y，z。 fO（x，y）<$fO（x，z）<$y = z我们只想考虑场是总体函数的模型，这些总体函数通常具有值nul。虽然不能确定它的不变量，但我们可以把公式变换成一种形式，使得一个不满足这个不变量的模型意味着存在一个满足这个不变量的模型（详见[16]）。积极字面量的翻译的主要规则如图5所示。要翻译一个否定的字面量，需要否定图5所示的底层原子公式的翻译，用存在性量化器替换泛量化器，然后删除存在性量化器，同时确保新引入的变量是新的。通过引入k个新的常数a1，...，a k，用VS ={a1，.，a k}，然后如图5所示转换结果。我们通过引入新的常数a1，.，来转换负基数约束<$（card（VS）≤k），它等价于card（VS）≥k + 1。，ak，ak+1，并替换约束58诉昆恰克湾Rinard/Electronic Notes in Theoretical Computer Science 131（2005）51F[[F]]V2=V1.fOO OfO（V1，O OVS=V1V2S S+x。V S（x） ⇐⇒V1(x)∨V2(x)SSVS=V1V2S S+x。V S（x） ⇐⇒V1(x)∧V2(x)SSVS=V1V2S S+x。V S（x） ⇐⇒V1(x)∧ ¬V2(x)SSVS={V1，.，Vn}OO+x。V S（x）x = V1. Vn=VnOOV S= V O.f S+x. V S（x）{\displaystyleV S（x）}V1=V2O OV1=V2O OVO∈ VSVS（VO）V1=V2你好V （x）第2条（x）款+1个S SSSV1=V2f f1996年，V（x，y）=V2（x，y）+1FFV = V [V ›→V]12 12个以上f f OOx，y。V（x，y）（（x = V1y = V2）1FOO（x/=V1<$V2（x，y）外来资产V1=V2[VO<$→VS] 1996年，V （x，y）（（x=VOVS（y））+1f fF（x/=VO<$VS（x，y）图五. 将正字面值转换为[字符串]= fragment其中1≤i≤k+1VS（ai）<$1≤i j≤k+1ai/=aj。复杂性接下来我们证明图4中公式的可满足性是NP完全的。我们仔细地构造了我们的翻译，以便它引入有限数量的量化器。事实上，每个合取最多引入三个泛量化器（（1）需要三个量化器）。通过移动这些用于更新位置的条件可以写成公式[等式3]=。因为生成的公式的大小是原始公式大小的多项式，生成它的时间是多项式，通过事实5.1我们得出结论，检查一个赋值给非嵌套原子公式的满足性非嵌套形式是一个多项式，其大小为文字的合取，指定了图4中公式F的原子公式的赋值，并且可以在NP中完成对原子公式的赋值。通过组合这两个非确定性的选择，我们得到了一个NP决策程序的表达式的满意度。NP难性是因为我们的语言包含了命题逻辑。 我们的结论是，诉昆恰克湾Rinard/Electronic Notes in Theoretical Computer Science 131（2005）51591图4中的公式是NP完全的。对相关工作的评论。基于量化预紧的一阶逻辑的片段在[4，9]中被分解，其中[递归函数]=classisdescribedasBernays-Schéonfinnkel-Ramseyclass。FinitemodelfindinggtooolssuchasAl-因此，loy [12]可以用来检查这些公式的满足性。解析技术[27]对于此类也是完整的，因为术语模型是有限的。6双变量逻辑在本节中，我们将展示带计数的双变量逻辑（记为C2）可用于决定图4中的约束，以及这些约束的一些有用扩展。我们考虑满足性问题，并使用包含任意数量的常数、一元关系符号和二元关系符号的语言。双变量逻辑逻辑C2是一阶逻辑：1）扩展为计数量化器<$k ≥kx.F（x），即对于某个常数k，至少有k个元素x满足公式F（x）; 2）限制为只允许公式中的两个变量名x，y。注意，变量x和y可以通过量化器嵌套重用，并且形式为k=kx的公式。F（x）和k ≤kx。 F（x）可表示为以 下 形式 的 公 式 的 布尔组合：n ≥kx。F（x）。文[10]证明了逻辑C2是可判定的，在[23，25]中确定了C2的C2没有计数L2的二元逻辑具有有限模型性质[19];这不是有计数的二元逻辑的情况[10]。在[14，15]中，确定了带有计数的双变量逻辑在对命令式程序中对象之间关系进行推理时的有用性。编码成带计数的双变量逻辑。 考虑将图4中的约束编码为带有计数的双变量逻辑的问题。事实证明，第5节中编码的大部分思想也适用于使用双变量逻辑的编码，因为我们在图5中最多只使用了两个泛量化器，并且存在量化的变量在语言中只是常量。为了避免使用三个变量来表示事实上，一些关系是函数s，我们用h_x代替（1）。≤1y。f（x，y）. 我们可以通过将卡（S）≤k替换为卡（S）≤kx.S（x）来直接表示基数约束。60诉昆恰克湾Rinard/Electronic Notes in Theoretical Computer Science 131（2005）517尼尔森-奥本组合我们接下来注意到，图4中公式的可满足性可以使用Nelson-Oppen决策过程的多排序版本来确定，该决策过程结合了三个单独的决策过程：1）关于表示为组件Nelson-Oppen过程的集合的推理理论，类似于[31]，但添加了有限基数（使用第5节的思想表示）; 2）多排序语言中的未解释函数符号[21]，其结果排序可以是集合排序的函数符号;以及3）阵列的扩展理论[20，28]。由于Nelson-Oppen决策过程中共享变量的等价类可以用NP算法来猜测，并且每个决策过程都是NP的，我们得出结论，我们的语言的Nelson-Oppen组合决策过程也是NP的虽然[31]已经观察到关于元素的推理可以与使用Nelson-Oppen过程的关于元素集合的推理相结合，但我们在这里观察到将所得过程与未解释的函数符号和数组相结合的有用性，获得用于推理对象的集值场的决策过程。8讨论和结论我们已经概述了解决集值场约束的三种技术：降阶为t阶逻辑，降阶为具有计数的双可变逻辑，以及使用Nelson-Oppen组合解决多排序问题。理 论 如 果 目 标 仅 是 决 定 图 4 中 的 语 言 ， 则 [ 编 辑 ]=clasanddNelson-Oppencombinatonyeldoptimalaldecisionprooce-dure。二变量逻辑有更复杂的决策过程，额外的表达能力，使表达的结构的形式mix。很好f（x，y）.suchcon构造了对象的所有状态非空属性，这些属性对于对象初始化的推理是很重要的。面向对象编程语言[7]此外，计数量化器可以自然地将数据库社区和面向对象建模社区中识别的高级应用程序约束表示为参考完整性和基数约束，以及角色约束[15]。注意，[f（x，y）f]=fragment比图4中的语言更接近x，允许对诸如fx，y. A（x）f（f（x，y）惠g（y，x））之类的属性的陈述。同时保留有界数量的量化器，因此是NP判定过程。基于将图4的语言分解为较小的纳尔逊-奥本理论的方法（如第7节所述）具有使用先前理解的和有效的决策程序的优点 此外，不需要特殊的编码，因为诉昆恰克湾Rinard/Electronic Notes in Theoretical Computer Science 131（2005）5161排序的使用自然地将约束分解为个体可判定理论的约束。我们的观察意味着，Nelson-Oppen组合中的每一个理论都可以用第5节的结果证明是可判定的。最后，我们可以结合第5节和第6节中介绍的技术使用纳尔逊-奥本组合的思想，因为纳尔逊-奥本方法允许公式的无量化器组合，这些公式本身不需要是无量化器的。例如，我们可以使用Nelson- Oppen技术来决定两变量逻辑在计算中，[计算公式]=用于计算和线性算法，其中包括三种方法的思想。致谢。我们感谢Darko Marinov对本文早期版本的有益评论，以及关于集合在符号执行中的使用的有益讨论。我们感谢Nguyen Huu Hai就本文件的早期版本所我们感谢AIOOL引用[1] T.鲍尔河Majumdar ，T. Millstein和S. K.拉贾马尼C程序的自动谓词抽象。Proc. ACMPLDI，2001年。[2] M. 巴尔内特河 D eL in e，M. Füahndr ich，K. R. M. L eino，andW. 是的。 面向对象程序的不变量的验证。Journal of Object Technology，3（6）：27[3] M. Barnett，K. R. M. Leino和W.舒尔特 Spec#编程系统：概述。 CASSIS 2004：安全、可靠和可互操作智能设备的构建和分析国际研讨会，2004年3月。[4] E. Büorger，E. Graédel，anddY. Gurev ich.Cl asicalDeci sinProbl em. Springer-Verlag，1997年。[5] C.博亚帕蒂河Lee和M. C.里纳德 一种防止数据竞争和死锁的类型系统。第17届ACM面向对象编程、系统、语言和应用年会，2002年。[6] D. G.克拉克，J.M.波特和J.诺布尔。 用于灵活别名保护的所有权类型。 在proc 1998年第13届ACM面向对象编程、系统、语言和应用年 会 。[7] M. Füahndr ichandK. R. M. L EIN O。在一种非结构化语言中，DECLARING和CHECKING是一种非结构化类型。在OOPSLA[8] C.弗拉纳根河Joshi，X. Ou和J. B.萨克斯使用懒惰证明解释的定理证明。在CAV，第355-367页[9] E. Gréadel. 设计了一个简单的结构化和可扩展的数据处理逻辑的片段。从一个简单的类到一个复杂的逻辑。InProceedingsofKalm′arWorkshoponLogicanddComputerScience， Szeged，2003.[10] E. Gréadel，M. 等等，还有E。 Rosen.两种不同的逻辑都可以实现。在Proceedings of12th IEEE Symposium on Logic in Computer Science LICS'97中[11] M. Hirzel，A. Diwan和M.动态类加载时的指针分析。 在ECOOP，2004年。62诉昆恰克湾Rinard/Electronic Notes in Theoretical Computer Science 131（2005）51[12] D. Jackson. Alloy：一种轻量级对象建模符号。 ACM TOSEM，11（2）：256-290，2002.[13] D.浩善 布尔代数的复杂性。 理论计算机科学，10：221[14] V. Kuncak和M.里纳德 角色逻辑。 技术报告925，MIT CSAIL，2003年。[15] V. Kuncak和M.里纳德角色逻辑中的广义记录与空间合取。2004年8月26-28日，在意大利维罗纳举行的第11届国际静态分析年会（SAS[16] V. Kuncak和M.里纳德关于集值场的决策过程。 技术报告，MIT CSAIL，2004年11月。[17] P. Lam，V. Kuncak和M.里纳德数据结构一致性的广义类型状态检查。2005年第六届验证、模型检查和抽象解释国际会议[18] F.洛格佐基于类的面向对象语言的独立组合分析。在Proceedings of the 10 th InternationalConference on Algesthetics Methodology And Software Technology（AMAST346. Springer-Verlag，2004年7月。[19] M. Mortimer. 一个普通的人和一个充满活力的人在一起。 Zeitschr. 我也是。 我知道一个G在数学课上跑。，21：135[20] G. Nelson和D. C.奥彭通过合作决策程序简化。ACM翻译计划。Lang.系统，1（2）：245[21] G. Nelson和D. C.奥彭 基于同余闭包的快速决策方法。 杂志of the ACM（JACM），27（2）：356 -364，1980.[22] J. Noble，J. Vitek和J. Potter。 灵活的别名保护。 在1998年第12届ECOOP会议上[23] L.帕乔尔斯基，W. Szwast和L.温柔一阶双变量逻辑计数的复杂性结果。SIAM J. on Computing，29（4）：1083[24] I.波莱湾L. Charlier和A.科特斯 静态分析的区分和共享域Java程序。在ECOOP，2001年。[25] I. 普 拉 特 - 哈 特 曼 具 有 （ 二 进 制 编 码 ） 计 数 量 化 器 的 双 变 量 片 段 的 复 杂 性 。 CoRR ，cs.LO/0411031，2004年。[26] G. Ramalingam，A. Warshavsky，J. Field，D. Goyal和M. 萨吉夫 为验证组件-客户机一致性而导出专门的程序分析。ACM SIGPLAN 2002年编程语言设计和实现会议集，第8394. ACM Press，2002.[27] A. Robinson和A.沃龙科夫，编辑。自动推理手册（第1卷）。 Elsevier和MIT出版社，2001年。[28] A.施通普角W. Barrett，D. L. Dill和J. R.莱维特数组扩张理论的一个判定过程。LICS，第29-37页，2001年[29] F.蒂普和J·帕尔斯伯格。可扩展的基于传播的调用图构造算法。 在proc 第15届ACM面向对象编程、系统、语言和应用年会，281-293页，2000年。[30] T. 是的。一个简单的故事。Master[31] C. G. 扎 尔巴 将 集合 与元 素 组合 。在 N.Dershowitz ，editor ，Verification ：Theory andPractice，volume2772 ofLecture Notes in Computer Science，pages 762-782. Springer，2004.[32] K. Zee，P. Lam，V. Kuncak，and M.里纳德结合定理证明和静态分析来保证数据结构的一致性。软件验证与确认国际研讨会，西雅图，2004年11月。