++）中的不变量通常用于描述对象状态的一部分，并在对象的生命周期内保持不变

理论计算机科学电子笔记131（2005）63-74www.elsevier.com/locate/entcs推断对象不变量扩展抽象张宝裕美国加州大学伯克利分校K.鲁斯坦·M Leino2美国华盛顿州雷德蒙德市微软研究院摘要面向对象语言（如Java或C#）的程序状态由过程的局部变量和存储在全局堆中的变量组成。 存储在堆中的变量是对象的域（即，类实例的字段）。本文提出了一种技术，用于推断这种面向对象的程序的属性。该技术将工作分为两个相互作用的部分：一个是对数据流敏感的分析，它跟踪在每个特定程序点看到的局部和全局状态;另一个是对数据流不敏感的分析，它跟踪一个类的所有“有效”实例中共同的属性，独立于程序计数器。分析是合理的，并在存在许多对象引用（别名）的情况下工作。为了精确，分析使用了最近的对象不变量方法，该方法在假设每个对象的不变量时显式持有（有效对象）或被允许违反。保留字：对象不变量，抽象解释，面向对象程序，推理1介绍证明计算机程序的正确性需要有关程序的知识，这些知识在程序文本中不容易获得。例如，要证明循环的正确性，可能需要知道一个条件，例如0≤x，是循环不变式。或者，为了证明类在1电子邮件：bec@cs.berkeley.edu2电子邮件：leino@microsoft.com1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.01.02364B.- Y.E. Chang等人理论计算机科学电子笔记131（2005）63classA{整数x;classB{整数x;classC{整数x;public void run（）publicvoid run（）public voidrun（）{this.x：=8;this.x：=8;this.x：=8;}}}publicvoid run（）{方法M（Bb）{方法M（C c）{this.x：= this.x+1;this.x：=b.x+1;c.x：= 7;}}}}}}Fig. 1. 演示需要考虑对象引用的简单程序示例。在面向对象程序中，可能需要知道条件0≤this.f对于类的所有实例（对象）都是不变的。这样的条件称为对象不变量。由于我们不能总是依赖于程序文本，包括所需的不变量的声明，我们认为在本文中的技术抽象解释[7]自动地从面向对象程序的文本中推断出这样的不变量。对象引用让我们用一些例子来说明我们的程序分析需要处理什么考虑图1中的类Java类。对于类A，条件this.x8在从构造函数退出以及进入和退出方法M时成立，因此，我们希望从我们的分析中获得this.x8是A的对象不变式。由于像x8这样的条件可以使用多面体域[8]来推断，因此推断对象不变量this.x8的稻草人建议是将字段选择表达式this.x视为表示一个变量，本质上每次将分析集中在一个（任意）对象上。然后，对身体进行抽象解释构造函数和方法（例如，，在Logozzo [14]的类设置中）来推断条件this.x8，由此可以得出结论（A·a.x8）。 但这个稻草人有问题。B类说明了需要了解除此之外的对象的属性。由于它关注的是关于这个.x可以说些什么，所以稻草人在方法中没有给出关于b.x的B.M，因此，我们不能得出结论的事实（b：B·b.x8）。也许更关键的是，C类证明了稻草人是不可靠的。方法C.M更新了一个对象的x场，所以稻草人可能不会认为这个更新对C对象的对象不变量有任何影响然后，分析会错误地推断出x=8，这将暗示谬误（c：C·c.x=8）。我们从类B和C得出结论，我们的分析必须知道对象引用。为了处理对象引用，我们在以前的工作[6]中建立了堆结构的抽象解释在这个框架中，我们将源语言中的字段读取表达式o.x视为索引到显式B.- Y.E. Chang等人理论计算机科学电子笔记131（2005）6365heap（由变量H表示），位于位置0，x 0，其中0是对象引用（即，，对象标识，指针或地址），x是一个唯一值的常数，命名为字段x，写作sel（H，o，x）（参见[10、12、18]）。为了处理字段更新，我们的框架还使用了堆继承pred- icate Hashio。xHJ，它断言堆H和HJ对于所有位置存储相同的值，除了可能对于位置x0，x 0。从由抽象域元素L表示的初始状态开始，对字段更新语句o.x：=e执行前向分析相当于应用以下抽象域操作，其中HJ是新变量：L：=约束（L，sel（HJ，o，x）=e）;L：=约束（L，H）xHJ）;L：=Eliminate（L，H）;L：=H（L，HJ，H）;这些操作在update语句之后为堆引入一个名称HJ，并使用sel和堆继承谓词来约束HJ然后，旧堆H被投影出来，名称heapHJ被重命名为H。我们的抽象解释框架的大部分详细工作与我们目前的论文无关。然而，一个重要的特征是框架由各种“现成的”抽象域（即，将变量的关系作为独立坐标进行推理的方法）。例如，用多面体域参数化框架[8]，我们得到了一个分析，可以推理到堆和线性算术的引用因此，框架的这种实例化能够推断语句o.x：= 5 ;p.y：=o.x+ 12导致如下状态，其中o.x= 5×p.y = 17保持。还值得指出的是，我们的框架正确地处理了不同变量引用同一对象时出现的别名问题。在我们刚刚给出的例子中，别名不是问题（也就是说，如果o和p指向同一个对象，这例如... ;o.x：= 5 ;p.x：=o.x+ 12，分析（正确地）推断o.x= 5只有在存在暗示o和p不引用同一对象的信息时才在最终状态下成立。对象不变量请注意，即使没有别名问题，上面的B类和C类也会出现问题。这些例子表明，我们的分析必须以某种方式同时跟踪多个对象的状态（比如B.M中的.x，b.x，C.M中的c.x）。这种情况可能看起来相当严峻，因为不同对象的数量没有限制，所有这些66B.- Y.E. Chang等人理论计算机科学电子笔记131（2005）63物体可以同时处于不同的状态。作为一种解决方案，我们抽象出一个特定的对象子集，并集体跟踪它们的状态。我们说每个对象都处于两种状态之一：它要么是有效的，这意味着它的对象不变量可以被依赖，要么是可变的，这意味着它的对象不变量可能暂时被违反。它是我们的分析集中跟踪的有效对象的集合。有效对象是处于“稳定状态”的类实例我们对我们分析的面向对象代码做以下假设：• 对象o通过执行特殊语句包o从可变转变为有效• 对象o通过执行特殊语句unpacko从有效转变为可变• 字段更新o.x：=e仅在对象o是可变的时发生这些假设在Boogie方法中引入，用于对象不变式[1，13，3]，该方法用于面向对象的Spec#编程语言[2]。请注意，pack和unpack语句不需要由程序员直接提供;它们可以由源语言中 的 规 则 或语 言 的 某些程式化使用中 的 规 则 （例如，，打开包装方法入口和方法出口打包Boogie方法论也处理类继承。它通过为对象的每个类框架提供可变/有效状态位来实现。 类框架是特定类的声明字段的集合。例如，如果B是A的子类，那么B对象可以对A有效，对B可变。 这允许每个子类声明自己的对象不变量。 我们考虑因此，将O打包为T，并从T解包O，这改变了类帧T的对象O如果x是在类T中声明的场，那么我们假设场更新o.x：=e仅在o对于T是可变的时发生。我们的技术我们在本文中提出的推断对象不变量的技术执行两个一起工作的分析。一种分析是局部分析，它对程序的每一个点都是逐行敏感的，并推断出程序的属性这种分析或多或少地确定了局部变量的属性和从局部变量可到达的堆位置。另一种分析，即全局分析，对每个类T不敏感地进行，并推断出所有有效的B.- Y.E. Chang等人理论计算机科学电子笔记131（2005）6367T对象--即类T的对象不变量。当局部分析遇到某个类型T的有效对象时，全局分析对当局部分析到达一个程序点时，一个给定对象的不变量应该保持不变，它所拥有的关于该对象的信息被全局分析用于下一个近似。2推断对象不变量在本节中，我们将描述我们的技术，以推断对象不变量使用 上一节讨论的基于抽象解释的框架回想一下，框架是由各种传统的抽象域参数化的，这些域决定了我们推断的关于对象的不变量的种类。为了简化讨论，我们考虑一个这样的抽象域，我们称之为策略抽象域。换句话说，我们描述了一种灵活的机制，通过这种机制可以推断出对象不变量，并将决定推断出的不变量类型（以及分析的精确程度）的策略选择交给用户。设P表示给定的策略域。如前所述，我们可以透明地扩展策略域，以使用我们以前的工作[6]中描述的框架来推断堆结构的属性。我们用C（P，S）表示这个扩展给出的抽象域，其中S表示处理堆更新的堆继承谓词的抽象域的存在。局部小波敏感分析的抽象状态正是C（P，S）的一个元素。与此同时，全局对堆栈不敏感的分析跟踪每个类T的对象不变量，这只是对可由C（P）表示的类T的有效对象的字段的约束，策略域扩展到堆位置上的原因。因此，全局分析的抽象状态是从类到C（P）的元素的映射，我们用I表示。(The堆继承域S不需要表示对象不变量，因为它只需要推理堆的更新，而对象不变量全局应用于所有堆。更确切地说，“我”的一个要素的具体化是具有以下形式的普遍量化的命题的合取：（约翰· （注：T· 有效期（t） 与同品种器械C（P）（C）其中C是C（P）的一个元素，它的自由变量只有t和H。此外，ToPredicateC（P）（C）中的sel表达式对于T的任何场x或其超类都应该是sel（H，t，x）的形式。(In文献[7]，68B.- Y.E. Chang等人理论计算机科学电子笔记131（2005）63具体域通常被描述为程序状态的集合，而不是状态谓词，ToPredicate被写为γ。）我们现在通过定义以下语句s的抽象转换判断来描述抽象解释：s：I;CI →IJ;Cj其中I和IJ是I的元素，C和CJ是C（P，S）的元素。为了便于记法，我们在每个程序点上写上组合的抽象状态I;CI，但是，虽然在标准的ab-解释中每个程序点有一个C，但只有一个全局I。通常情况下，C在每个程序点初始都是底部（C（P，S）），除了在某些初始状态它是顶部（TC（P，S））。类似地，全局I最初也是底部的（即，，每个类T被映射到C（P））。抽象状态的全局和局部组件在unpack和pack语句中精确地交互 在每个语句包o为T时，程序断言类T的对象不变量对对象o保持不变，因此我们将关于o的场推断的任何性质合并到局部分析中。 粗略地说，我们需要从C中获得涉及在T或T的任何超类中声明的o的场的约束（即，，表达式对于类T的场x，形式为sel（H，o，x））。然后，在局部不变量中将o重命名为t，并用它削弱当前的全局I。正如我们在下面的例子中所展示的，这种削弱必须使用加宽运算符来执行，以确保分析的终止，而不仅仅是连接。(As通常[7]，我们可以使用一些连续的粗加宽算子序列，其中前几个可能是连接操作。 更确切地说，包装的处理如下：P=C↑sel（H，o，ΔT）将o包装为T：I;C→I[T<$→I（T）o[t/o]P];C其中H是当前堆的堆变量。我们写o表示加宽运算符，写[y/x]e表示表达式e中避免捕获的变量x重命名为y。此外，我们将C↑e写为可能从C中删除约束的操作，只保留那些没有自由变量的约束，而不是那些出现在匹配e的子表达式中的约束（其中如上所述，该操作获得仅涉及o的场的约束。 例如，如果x，y，z表示在类T中声明的字段，C表示sel（H，o，x）≤5sel（H，o，y）≤sel（H，p，z），则C↑sel（H，o，T）返回的值表示sel（H，o，x）≤5。33↑操作的实现使用了这样一个事实，即我们的框架映射了所有的subex-B.- Y.E. Chang等人理论计算机科学电子笔记131（2005）6369我们可以观察到C是C（P，S）的一个元素，而I（T）是C（P）的一个元素，所以上面的规则不是很好的形式。为了在两种分析之间进行交流，话语的语言是一阶逻辑的语言--我们首先从C中具体化和提取感兴趣的谓词，然后在抽 象 域C （P ） 中 抽象 ， 然 后 再扩 大 。 我们 可 以 把 C↑e 看 作 一个 特 殊 的ToPredicateC（P，S）滤波器。在局部分析过程中，我们可能需要实例化一个对象不变量，以获得特定点的特定属性。对象不变式方法确保对字段的更改由unpack语句保护，从而指示何时可能临时违反对象不变式。我们在unpack语句中实例化对象不变量，因为它标记了代码sec-这削弱了对象不变量。更准确地说，收益如下：从T解包o：I;C→I;CH[o/t]I（T）与pack类似，实际的交互是通过将I（T）转换为predicate（具体化），然后在与C相遇（H）之前在抽象域C（P，S）中进行抽象。所有其他的程序语句都只选择局部抽象状态C，并且基本上按照标准的抽象解释进行（除了推理扩展到堆结构[6]）。请注意，这种分离只是因为第1节中描述的对象不变方法而获得的。特别地，字段更新对全局抽象状态I没有影响，因为方法规定只有可变的（即，，未打包的）对象可以被修改-回想一下，I中携带的对象不变量仅适用于有效（即，打包的）对象。例如图2给出了对图1中的类B的一个稍微修改过的版本的示例分析，其中包含显式的unpack和pack语句。我们假设多面体域[8]用作策略域。每个程序点的抽象状态都是右对齐的，并被装箱。对于这个例子，我们假设我们有一个前提条件，即d是有效的，它可能是用户指定的，由源语言中的规则或语言的某些程式化使用所暗示的，通过单独的分析获得的，或者与此分析同时获得在任何一种情况下，我们在方法M的初始状态下都有sel（H，d，y）=通过对D和B不变量的当前对象的实例化，1个Rssel（H，d，x）= 8。 M中的unpack语句实例化当前对象我们可以使用符号值[6]，但我们在这里缺乏讨论这些细节的空间。70B.- Y.E. Chang等人理论计算机科学电子笔记131（2005）63classD extendsB{整数y;public voidrun（）{this.y：= 1;把它包装成D;}}classB{整数x;publicvoid run（）this.x：=8;把这个包装成B;}方法M（D d）{∗把这个从B解包;∗this.x：=d.x+d.y;把这个包装成B;}}图二. 实例分析。B的不变量。fieldupdate语句不检查全局状态，并在本地状态上照常进行然后，在M中的pack语句中，我们从局部状态得到sel（H，this，x）=9。这个状态被扩展到B的当前对象不变式，以获得B的新对象不变式的sel（H，t，x）8。由于这种加宽导致了B的对象不变量的当前近似的减弱，因此分析需要重新访问先前近似在图2中，即在那些标记有“”的点处，用较弱的对象不变量继续分析，然后到达一个固定点。图2中的示例演示了为什么对象不变量的弱化必须使用加宽运算符，就像在标准抽象解释中使用循环构造一样。在这个例子中，使用连接来削弱对象不变量将产生抽象域元素的无限上升链9sel（H，t，x）810sel（H，t，x）811sel（H，t，x）8 ......这是什么？D<$→sel（H，t，y）= 1，B <$→sel（H，t，x）= 8 ;sel（H，this，x）=9D<$→sel（H，t，y）= 1，B <$→sel（H，t，x）8 ;sel（H，this，x）=9D<$→sel（H，t，y）= 1，B <$→sel（H，t，x）= 8 ;sel（H，d，y）=1<$D<$→sel（H，t，y）= 1，B <$→sel（H，t，x）= 8 ;sel（H，d，y）= 1 <$sel（H，d，x）=8<$sel（H，this，x）=8 <$D<$→sel（H，t，y）= 1，B→D<$→sel（H，t，y）= 1，B <$→sel（H，t，x）= 8 ;sel（H，this，x）=8→sel（H，t，y）= 1 ;sel（H，this，y）=1D<$→sel（H，t，y）= 1，B<$→ n; T <$D ›→D <$→B.- Y.E. Chang等人理论计算机科学电子笔记131（2005）6371我们注意到，解包和打包的类参数不需要像这个例子中那样是周围的类例如，指定一个超类将实例化和更新超类的对象不变式引用多个对象的对象不变量的 技术 用于推断，到目前为止，我们所描述的对象不变量并不考虑对象不变，classSet{intcard;int[ ]arr;invariantthis.card=this. xl.Length;.. .涉及多能级场的这往往是相当重要的，坦特。例如，我们可以实现一个Set类，其中数组作为后备存储，其中对象不变式是集合的基数等于数组的长度（见插图）。如果没有额外的支持，很难正确地推断出这样一个不变量，因为存在别名问题--Set对象o的域的别名可以修改对象o指向的数组，而不需要- out通过o。arr.幸运的是，对象不变量方法[1]也可以帮助我们解决这个问题：所有权模型被强加，只有当对象不变量被声明为由Set“拥有”时（即，”（《说文》）。这种所有权模式的细节并不相关在这里;必要的是，该方法向我们保证，“易”是指“易”，“易”是指“易”，“易”指“易”。未打包）。这允许我们实例化任何拥有的字段的对象不变式（例如，当对象o被解包并包含有关所拥有字段的字段的任何信息（例如，当O被打包时（对于O的所有域是可传递的）。在第2节所描述的分析的上下文中，提取涉及场的约束的· ↑ ·操作被扩展为也获得拥有场的场（并且是传递的）。然后，pack规则中的行上方的条件采用如下形式（此处显示为没有传递性）：P=C↑ {sel（H，o，T），sel（H，（sel（H，o，repT）），）}其中，RepT匹配T中声明的任何Rep字段或T的超类，并且任何领域都3相关工作推断面向对象程序的属性提出了几个挑战。一个挑战是对象可能有别名，也就是说，不同的变量可能引用同一个对象。存在各种指针分析来解决这些问题（例如，参见[20，9]）。然后，这些指针分析可以用作72B.- Y.E. Chang等人理论计算机科学电子笔记131（2005）63用于生成抽象位置的基础，在该基础上可以应用传统的抽象解释[4，21]。另一个挑战是确定对象堆中指针的结构，这是一种名为形状分析的技术，也被用作抽象解释的基础。另一个挑战是分析对象字段的属性[6]，或者考虑类中方法的组合[14]。我们在本文中所面临的挑战是推断对象的场之间的关系，特别是推断对于类的所有实例我们的技术使用了一个低敏感的分析和一个低不敏感的分析的组合。Venet和Brat也使用了这些分析的组合[21]，尽管他们的对时间不敏感的分析被用来细化从初始点到分析获得的抽象位置集。通过C（·，S）框架，将类比推理引入到我们的时间敏感性分析中。Logozzo [15]还考虑了在存在别名和其他对象的上下文中对面向对象语言的分析。在他最近的博士论文中，Lahiri [11]考虑了推断量化，其主体是谓词P（k）的布尔组合，其中k是量化变量，P来自一些固定的谓词符号集。他的技术还执行了一个连接操作，通过以一种对时间敏感的方式推断出的新事实来削弱量化器的主体。4结论总结我们的贡献，我们已经提出了一种技术，推断面向对象的程序中的对象不变量。针对主流的面向对象语言，该技术处理对象之间的别名，并在存在多个可能处于不同状态的对象的情况下工作。我们的技术，nique分裂成两个协作部分的工作：一个对数据流敏感的分析，推断每个程序点的不变量和一个对数据流不敏感的分析，推断一个类的所有有效对象的不变量。 基于我们在结合抽象域和处理堆结构[6]方面的艰苦工作，我们的技术可以通过任意抽象域来参数化，这些抽象域确定推断出什么样的不变量。为了以结构化的方式确定对象何时处于据我们所知，我们的技术是第一个在存在多个对象的情况下，推断出适用于一个类的所有对象的对象不变量。该技术本身是第一个将工作划分为对气流敏感部分和对气流不敏感部分的组合的技术之一一个可能令人惊讶的B.- Y.E. Chang等人理论计算机科学电子笔记131（2005）6373我们工作的一个方面是我们不应用全局别名分析。 相反地， 我们使用本地可用的信息来解决别名问题。这使得我们的技术更加模块化，我们希望它在程序员能够编写方法前提条件的环境中工作得很好（如Eif- fel [16]，Java withJML [5]和Spec# [2]）。我们工作的最后一个贡献是将方法和分析结合起来，这为两者增添了力量。该方法给出了分析指导的形式是什么，被推断，并在哪里推断它，和分析，使方法更容易使用，补充任何显式的不变量的程序员可能已经宣布。事实上，我们解释说，由于方法论的原因，我们可以得到相当精确的不变量，即使使用廉价的保守的过程内分析，其中调用被建模为基本上扰乱整个堆，因为我们可以假设在调用之后，任何对象的对象不变量都没有传递给可变表中的被调用者（即，未打包的）状态保持。我们正在Spec# [2]程序验证器中实现我们的技术，并期待获得一些经验。引用[1] Bar n ettt，M. 、R. DeLine，M. Füahndr ich，K. R. M. 我不和W。 S chulte，Vericationofoject-oriented programs with invariants，Journal of Object Technology 3（2004），pp. 27比56[2] Barnett，M.，K. R. M. Leino和W. Schulte，The Spec# programming system：Anoverview，in：CASSIS 2004，LNCS3362（2005），pp. 49比69[3] 巴内特，M。和D. A. Naumann，Friends need a bit more：Maintaining invariants over sharedstate，in：Mathematics of Program Construction 2004，LNCS3125（2004），pp.54-84.[4] B.B. ，P. 科乌索河。 别这样，J。 弗累特湖 Mauborgne，A. 我的天啊。MonniauxandX. Rival，大型安全关键软件的静态分析器，PLDI 2003（2003），pp. 196- 207.[5] 伯蒂湖，Y. Cheon，D.R. Cok，M.D. 恩斯特，J。R. Kiniry，G.T. Leavens，K.R. M. Leino和E. Poll，An overview of JML tools and applications，International Journal on Software Toolsfor Technology Transfer（2005）.[6] 张，B.- Y. E.和K. R. M. Leino，Abstract interpretation with alien expressions and heapstructures，in：VMCAI 2005，LNCS3385（2005），pp. 147比163[7] Cousot，P. and R. Cousot，Abstract interpretation：A unified lattice model for static analysisof programs by construction or approximation of fixpoints（抽象解释：通过定点构造或近似对），第四届POPL，1977年，pp.238-252。[8] Cousot，P. and N. Halbwachs，自动发现程序变量之间的线性约束，在：第五POPL，1978年，pp. 84比96[9] 达斯，M.，基于统一的指针分析与方向分配，在：PLDI 2000（2000），pp。35比46[10] 霍尔角A. R. 和N.Wirth，An axiomatic definition of the programming language PASCAL，Acta Informatica2（1973），pp.335-355[11] Lahiri，S.K.， 论文，卡内基梅隆大学（2004），出现。74B.- Y.E. Chang等人理论计算机科学电子笔记131（2005）63[12] Leino，K. R. M.，“走向可靠的模块化程序，”博士。论文，加州理工学院（1995年），技术报告Caltech-CS-TR-95-03。[13] Leino，K. R. M. 和P. Müller，Objectinvarian tsindyamiccontxts，in：ECOOP2004，LNCS第3086（2004）号来文，第308页。491-516.[14] Logozzo，F.，面向对象语言的类级模块化分析，在：SAS 2003，LNCS第2694（2003）号来文，第2694页。37比54[15] Logozzo，F.， 基于类的面向对象语言的独立组合分析，在：AMAST 2004，LNCS3116（2004），pp. 332-346[16] 迈耶湾，[17] Muchnick，S. S.和N. D. Jones，Flow analysis and optimization of Lisp-like structures，in：S. S. Muchnick和N. D. Jones，editors，Program Flow Analysis：Theory and Applications，Prentice-Hall，1981 pp. 102-131[18] Poetzsch-He Schweiter，A.，面向对象程序的规范 和验证，Habilitititionsschr ift，TechnischeUniversitétMunchn（1997）。[19] Sagiv，M.，T. W. 代表和R。Wilhelm，通过3值逻辑的参数形状分析，TOPLAS24（2002），pp.217-298.[20] Steensgaard，B.，在几乎线性时间内的指向分析，在：第23届POPL（1996年），pp。32比41[21] Venet，A.和G. Brat，Precise and Efficient static array bound checking for large embedded Cprograms，PLDI 2004（2004），pp.231-242.