理论计算机科学电子笔记131（2005）75-84www.elsevier.com/locate/entcs抽象解释和面向对象编程：Quo Vadis？FrancescoLogozzoE'collepolytechniqueeF-91128 Palaiseau，FranceAgostino Cortesi阿戈斯蒂诺·科尔特斯2，3Dipartimento diInformaticaUniversit`aCa意大利威尼斯摘要这份立场文件的目的是对面向对象程序的抽象解释的主要贡献进行快速概述，并在这一领域中绘制可能的研究路线。关键词：抽象解释，面向对象编程，静态分析1介绍抽象解释（Abstract Interpretation）是软件系统静态分析的理论，它在数学环境中形式化了近似和抽象的概念，并且独立于特定的语言和应用程序。然而，当我们看过去20年1 电子邮件：Francesco. polytechnique.edu2 电子邮件地址：cortesi@dsi.unive.it3Partilysup pordyMURFIRBgranntn. RBAU018RCZandbyMIURPRIN1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.01.02476F. Logozzo，A.Cortesi/Electronic Notes in Theoretical Computer Science 131（2005）75(see[14]的扩展参考书目的电子版），适合抽象解释设置的惊人丰富的问题和解决方案套件通常依赖于特定的编程语言和要分析的给定属性（也可能是语言依赖的）。由于抽象解释具有非常基于语义的特征，因此具有强大语义基础的语言范式（例如函数和逻辑编程）在过去一直是开发复杂抽象域和专用定点算法的非常肥沃的试验床，另一方面，在面向对象编程领域的贡献时，图片仍然是支离破碎的，这可能会掩盖抽象解释在主流编程平台上的巨大潜力，OO范式正在取得领导地位。本文旨在对面向对象语言的抽象解释的现有文献进行综述，并对该领域的研究如何取得进一步的进展提出一些建议。2所做的一切...首先，让我们试着重温一些有趣的贡献（没有声称是完整的！）面向对象语言的静态分析。它们主要关注优化问题。2.1阶级分析对于每个程序点PP和每个变量xPP，类分析计算一组类CxPP，使得如果在程序x的执行中，在程序点PP处，具有运行时类型C，则C∈ CxPP。类分析是有用的（i）面向对象程序的优化，从而静态地解决虚调用，以及（ii）用于程序的控制流图的静态构造，从而为进一步分析提供第一步事实上，如果阶级分析推断一个给定的程序点，对应于一个方法调用，CxPP是一个单例，那么就不需要在类层次结构中查找过程来确定要在运行时调用的方法。文献中提出了几种类别分析，它们考虑了精度/成本比的不同值。例如，Palsberg和Schwartzbach的开创性工作，[37]，提出了一个非常精确，但也昂贵的，对无类型面向对象语言的分析。这些结果已经被相同的作者[36]以及其他人[4，18，15，45]改进，他们考虑快速但也不精确的类分析，以消除C++中的虚F. Logozzo，A.Cortesi/Electronic Notes in Theoretical Computer Science 131（2005）7577另一种降低分析成本的方法是将其模块化：Besson和Jensen引入了基于DAT- ALOG的模块化类分析，[5]，Probst描述了一种增量构建Java程序控制流图的分析，[39]。Spoto和Jensen [44，24]对这种分析提供了一种统一的、基于抽象解释的观点。作者定义了一个具体的跟踪语义，并证明了现有的分析是如何抽象这种语义 的。给定 执行轨 迹σ0σ1σ2.σn和返 回对象运 行时类 型的函 数typeOf ，Palsberg和Schwartzbach的分析通过考虑抽象函数得到，使得αPS（σ0σ1σ2.σn）= λPP。λx。{typeOf（σi（x））|i∈ [0. n]，σi（pp）=PP}. Bacon和Sweeney的快速类型分析是通过考虑进一步的抽象来获得的，该抽象通过以下方式将给定变量的类型收集在一起：所有程序点：αBS（σ0σ1σ2.σn）= λx。αPS（σ0σ1σ2. σn）（pp）（x）.pp∈Program作为其形式化的必然结果，斯波托和詹森通过考虑相应抽象域的相对精度，将分析的相对精度正式联系起来。2.2指针分析指针分析为每个程序点PP和每个变量x计算堆对象的集合AxPP，使得如果在程序的执行中，在程序点PP，x指向堆对象h，则h∈ AxPP。一个精确的和可扩展的指针分析是一个有效的面向对象程序静态分析的基本要求。事实上，在现实世界的面向对象语言中，对象是堆分配的，它们明确地由它们的堆地址标识。因此，精确确定变量可能指向的地址可以使人们获得精确的信息，关于构成程序的对象的信息。此外，指针分析意味着类分析。事实上，给定指针分析的结果AxPP，类x在程序点PP处可以求值的集合由抽象函数αL给出，该抽象函数α L收集地址在AxPP中的堆对象的类型：（1）A（A）= A（A）|h∈ AxPP}= CxPP.对面向对象语言的有效指针分析的第一次尝试集中在对现有C语言指针分析的修改/改编上。例如，Rountev，Milanova和Ryder提出了Java的指针分析，78F. Logozzo，A.Cortesi/Electronic Notes in Theoretical Computer Science 131（2005）75[41，34]，它将Anderesen的指针分析用于最近，Pollet，Le Charlier和Cortesi引入了两个抽象域来表达动态创建的对象的类型，结构和共享信息，[38];Chang和Leino提出了一个抽象域的代数，本质上是对堆分配对象的精确别名分析和通用抽象域（代数的参数）的简化产物，[9]。2.3逸出分析转义分析确定对象的生存期是否超出其静态作用域。如果PP是方法的出口点，那么逃逸分析计算PP处堆分配对象的集合EPP。 逸出分析用于程序优化，特别是用于（i）堆栈分配对象和（ii）删除同步。转义分析与指针分析密切相关。事实上，如果A是通过指针分析计算的信息，对于所有的程序点和变量，那么αB（A）=x∈VarsAPPx= EPP。Gay和Steensgaard对Java中的stackallocation应用了一种非常快速但不精确的转义分析[21];Bogda和Hüoltz通过使用更精确的分析[8]解决了并发Java程序中同步消除的问题; Blanchet为完整的Java开发了一种转义分析，其可靠性证明依赖于指针分析[7，6]。Blanchet的分析是精确和有效的，足以应用于推进堆栈分配和同步清除任务。已经开发了其他几种逃逸分析，具有不同的精度/成本比值。我们回顾Whaley-Rinard和Viven-Rinard分析，基于点逃逸图，[47，46]; Choi et. al分析，基于连接图，[10]; Ruf分析，利用静态场，[42]。2.4类不变量类不变量代表了面向对象程序的良好软件工程的基础，[33]。一个类的属性是一个类的属性，在类的任何方法执行之前和之后都有效。它可以被描述为跟踪语义的抽象，其中只保留与类实例的方法调用的入口点和出口点相对应的状态，[30，29]。F. Logozzo，A.Cortesi/Electronic Notes in Theoretical Computer Science 131（2005）7579抽象解释类层次结构抽象领域类近似阶数（±）子类关系（≤）最抽象域（TD）对象还原产物多重继承域名优化类扩展Fig. 1. 抽象域和类层次结构之间的相似性。自动推断的类不变量对于类的模块化软件验证、优化、代码文档和编译器设计是有用的。Ghemawat，Randall和Scales [22]以及随后的Ag-garwal和Randall [1]提出了一种静态分析，用于删除对数组边界的检查，其本质上是以以下形式计算类不变式：a== null <$0 ≤ b ≤ a。长度 Detlefs对推断正确的长寿命数据结构元素的显式释放[16]。Flanagan和Leino开发了Houdini，一个基于ESC/Java的工具，用于不变量的推理，[20]。Ernst设计了Daikon，一个用于推断伪类不变量的工具，[19]。Logozzo引入了一个通用的框架来推断类不变量，它考虑了继承，多态性，互递归类[32，28，26，27]。2.5其他分析在为面向对象语言设计的其他分析中，我们回顾了Christensen，Møller和Schwartzbach的分析，它近似了字符串表达式的结果[11]; Distefano，Katoen和Rensik的分析，他们提出了面向对象程序的时态逻辑和相应的模型检查算法[17]; Owen 和 Watson 的 分 析 ， 他 们 提 出 了 一 种 分 析 ， 以 消 除 不 必 要 的box/unboxing操作[35]; Zee和Rinard的分析，它允许人们消除写障碍[48];Zurr，Cerny，Madhusudan和Nam的分析，它综合了Java类的接口规范[2];Salcianu和Rinard的分析，检查Java方法是否是纯的[43]。80F. Logozzo，A.Cortesi/Electronic Notes in Theoretical Computer Science 131（2005）753...我们能做些在前面的调查中，我们已经看到了抽象解释是如何有效地分析、验证和优化面向对象语言的技术。我们认为它也可以用于面向对象系统的形式化和描述。事实上，抽象解释理论和类层次结构之间有相似之处。抽象解释理论的一个基本结果是，如果具体域是一个完备格，则它的所有抽象的集合 也是一个完整的网格[13]。设D是一个抽象格，H是一个类层次结构。D上的阶是抽象域的相对精度，即， D1±D2i是D2的抽象. 直观地说，这意味着D1至少捕获了所有D2的信息，即，D2是D1的一种改进[23]。另一方面，H上的顺序是子类关系，即， C1≤C2i <$C1是C2的子类。直觉上，这意味着类C1是类C2的特化或精化。不同地说，C2是一个比C1更抽象的类。作为一个结果，（i）TD，D的最大元素，是最抽象的域;和（ii）对象，H中所有类的公共超类，是最抽象的类。利用抽象域格和类层次这两个概念之间的这种平行性，我们可以说D上的相遇操作的H-对应物是多重继承。实际上，两个抽象DomainD1和D2的交运算是约化积，即最抽象域D3，包含D1和D2的所有信息，[13]。另一方面，如果C3是C1和C2的子类，则它包含其超类的所有域，并且可以表现为超类。此外，抽象域精化和类的扩展也是相关的概念事实上，一个给定抽象域的精化是一个域，它捕获了精化域捕获的所有属性加上一些其他属性（具体到精化）。另一方面，给定基类的扩展是继承所有祖先的行为，加上其他一些行为（考虑，例如，经典的2DPoints和3DPoints类，[12]）。我们认为，图1中总结的两个概念之间的类比值得进一步研究，从而产生结果的例如，（i）在类层次结构中，减少基数幂;（ii）在抽象域中，接口和多态性是什么？我们已经开始了一项研究，在这项研究中，我们将抽象解释技术应用于阶级结构的定义和操纵，[31]，第一个结果非常令人鼓舞。F. Logozzo，A.Cortesi/Electronic Notes in Theoretical Computer Science 131（2005）7581面向对象语言的抽象解释的未来研究可能会考虑整个面向对象软件工程过程的验证问题：分析（OOA），设计（OOD）和实现（OOI）。也就是说，研究抽象解释如何为需求规范（只是所需系统行为的抽象）提供一种替代的形式化方法，以及软件设计（通过利用类不变量），其实现（通过利用对象不变量）和系统集成（通过非功能需求的适当抽象表示）的指导方针可能是有趣的。4结论在这个位置上，我们快速概述了面向对象语言的抽象解释的主要贡献，并概述了两个领域的两个核心概念之间的一些类比，分别是抽象域和类层次结构。引用[1] A. Aggarwal和K. H.兰德尔相关领域分析。在ACM SIGPLAN Conference on ProgrammingLanguage Design and Implementation（PLDIACM Press，June 2001.[2] R. P. Cerny，P. Madhusudan， and W. 南Java 类接口规范的合成。第31届ACM SIGPLANSymposium on Principles of Programming Languages（POPLACM Press，2005.[3] L. O. 安徒生程序分析和C语言的专门化。博士论文，丹麦哥本哈根大学，1994年。[4] D.F.培根和P·斯威尼 C++虚函数调用的快速静态分析。 法律程序中1996年ACM SIGPLAN面向对象编程系统会议，语言&应用（OOPSLA'96）。ACM Press，1996.[5] F. Besson和T.詹森。使用数据库进行模块化类分析。第10届国际静态分析研讨会（SASSpringerVerlag，2003年。[6] B.布兰切特面向对象语言的转义分析。 应用到Java。 第14届ACM面向对象编程、系统、语言和应用会议（OOPSLA[7] B. 布 兰 切 特 JavaTM 的 转 义 分 析 ： 理 论 与 实 践 。 ACM Transactions on ProgrammingLanguages，25（6）：713[8] J. 我是你的朋友。 你好。 在日本，恢复不必要的开支是一个棘手的问题。在ACM面向对象编程系统会议上，语言应用（OOPSLAACM Press，1999.[9] B.- Y. E. Chang和K.R.M.莱诺用外来表达式和堆结构进行抽象解释。第六届验证、模型检查和抽象解释国际会议（VMCAISpringer-Verlag，2005.82F. Logozzo，A.Cortesi/Electronic Notes in Theoretical Computer Science 131（2005）75[10] J. D. 崔，M。 古普塔，M。 J.塞拉诺，V.C. Sreedhar，和Midki， P.逃逸分析 对于Java。在ACM SIGPLAN会议上，面向对象编程系统，语言应用（OOPSLAACM Press，1999.[11] A. S.克里斯滕森，A. Moller和M. I. 施瓦茨巴克 精确分析字符串表达式。国际静态分析研讨会论文集（SASSpringer-Verlag，2003.[12] W. R. 库克和J.帕尔斯伯格。继承的指称语义及其正确性。信息与计算，114（2）：329[13] P. Cousot和R.库索程序分析框架的系统设计。第六届ACM SIGPLAN-SIGACT Symposiumon Principles of Programming Languages（POPL北京：人民出版社，1979年。[14] P. Cousot和R.库索嵌入式软件的静态分析：问题和前景，邀请论文。三纪元Henzinger和C.M.Kirsch编辑，Proc.First Int. Workshop on Embedded Software，EMSOFT 2001，计算机科学讲义第2211卷，第97-113页。Springer，2001年。[15] J. Dean，D. Grove和C.钱伯斯用静态类层次分析法优化面向对象程序。在第九届欧洲面向对象编程会议（ECOOPSpringer-Verlag，1995.[16] D.德特勒夫斯引用计数不变量的自动推断。 在第二届ACM研讨会上，语义，语义分析和内存管理的计算环境。ACM Press，2004.[17] D. Distefano、J.P. Katoen和A.伦西克 基于对象系统的时态逻辑。 在第四届开放式基于对象的分布式系统的形式方法国际会议，IFIP会议论文集第177卷，第285-304页，Stanford，CA，U.S.A.，2000年9月。Kluwer Academic Publishers.[18] K. 我和你。霍泽尔 在C++中直接调用virtualf u nctionccc o s。在第11届ACM面向对象编程、系统、语言和应用会议（OOSLA '96）ACM Press，1996.[19] M.恩斯特动态发现可能的程序不变量。博士论文，华盛顿大学计算机科学与工程系，2002年。[20] C. Flanagan和K. R. M.莱诺Houdini，一个ESC/Java的注释助手。 欧洲形式方法国际研讨会论文集（FME 2001），计算机科学讲义第2021卷，第500-517页Springer-Verlag，2001年3月。[21] D.盖伊和B。斯坦斯加德基于对象程序的快速转义分析和堆栈分配。在第九届国际会议的论文集建筑（CCSpringer-Verlag，2000.[22] S. 盖马瓦特湾 H. Randall和D. J. Scales. 现场分析： 变得有用和低级- 成本过程间信息。 在Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Designand Implementation（PLDIACM Press，June 2000.[23] R. Giacobazzi 和 F. 兰 扎 托 细 化 和 压 缩 抽 象 域 。 自 动 机 、 语 言 和 编 程 国 际 会 议 论 文 集（ICALPSpringer-Verlag，1997.[24] T. Jensen和F.斯波托通过抽象解释进行面向对象程序的类分析。第四届软件科学和计算结构基础国际会议论文集（FOSSACS 2001），计算机科学讲义第2030卷，第261-275页Springer-Verlag，2001年4月。[25] T. Lev-Ami 和M.萨吉 夫 Tvla ：一 个实现 静态分 析的系 统。第七届 国际静 态分析 研讨会（SASSpringer-Verlag，2000.F. Logozzo，A.Cortesi/Electronic Notes in Theoretical Computer Science 131（2005）7583[26] F. 洛 格 佐 面 向 对 象 语 言 的 类 级 模 块 化 分 析 。 在 Proceedings of the 10th Static AnalysisSymposium 2003（SASSpringer-Verlag，2003年6月。[27] F.洛格佐一种基于静态分析的行为子类型化方法。 在基于组件的系统测试和分析国际研讨会（TACoS 2004）的会议录中，理论计算机科学电子笔记。Elsevier Science，2004年4月。[28] F.洛格佐类不变量的自动推理。在第五届验证、模型检查和抽象解释国际会议（VMCAI '04）Springer-Verlag，2004年1月。[29] F.洛格佐面向对象语言的模块化静态分析。博士论文，Ecole Polytechnique，2004年6月。[30] F.洛格佐类不变量作为跟踪语义的抽象解释。 计算机语言，系统和结构，2005年。[31] F. Logozzo和A.科特斯抽象解释的语义类层次结构2005年提交出版[32] 弗朗西斯科·洛戈佐。基于类的面向对象语言的独立组合分析。 在Proceedings of the 10 thInternational Conference on Algesthetics Methodology And Software Technology（AMAST346. Springer-Verlag，2004年7月。[33] B.迈耶面向对象软件构造（第二版）。专业技术参考。Prentice Hall，1997年。[34] A. Milanova，A. Rountev和Ryder B. G. java的点对和边对分析的参数化对象敏感性。软件测试与分析国际研讨会论文集（ISSTA 2002）。ACM Press，2002.[35] T. Owen和D.华生降低对象装箱的成本。在第13届国际会议的论文集建筑（CCSpringer-Verlag，2004.[36] N. Oxhj、J. Palsberg和M.I.施瓦茨巴赫使类型推理实用化。 在欧洲面向对象编程会议论文集（ECOOPSpringer-Verlag，1992.[37] J. Palsberg 和 M. I. 施 瓦 茨 巴 赫 面 向 对 象 的 类 型 推 理 。 ACM SIGPLAN 面 向 对 象 编 程 会 议（OOPSLAACM Press，1991.[38] I.波莱湾Le Charlier和A.科特斯Java程序静态分析的区分和共享域。在Proceedings of theEuropean Conference on Object Oriented Programming（ECOOPSpringer-Verlag，2001.[39] C.普罗布斯特图书馆模块化控制流程分析。在Proceedings of the Static Analysys Symposium（SASSpringer-Verlag，2002.[40] G. Ramalingam，A. Warshavsky，J. Field，D. Goyal和M. 萨吉夫 为验证组件-客户机一致性而导出专门的程序分析。在ACM SIGPLAN 2002年编程语言设计和实现会议（PLDIPress.[41] A. Rountev，A. Milanova和B. G.赖德使用注释约束的Java指向分析。第16届ACM面向对象编程、系统、语言和应用会议ACM Press，November 2001.[42] E.鲁夫有效的java同步删除。在ACM SIGPLAN编程语言设计与实现会议（PLDI北京：人民出版社，2000年。84F. Logozzo，A.Cortesi/Electronic Notes in Theoretical Computer Science 131（2005）75[43] A. Salcianu和M. 里纳德java程序的纯度分析。In Proceedings of the第六届验证、模型检查和抽象解释国际会议（VMCAI'05），LNCS第3385卷。Springer-Verlag，2005.[44] F. Spoto和T.詹森。类分析作为痕迹语义学的抽象解释。ACM Transactions on ProgrammingLanguages and Systems（TOPLAS），25（5）：578[45] F.蒂普和J·帕尔斯伯格。可扩展的基于传播的调用图构造算法。在2000年ACM SIGPLAN会议上，面向对象编程系统，语言应用（OOPSLA 2000）。北京：人民出版社，2000年。[46] F. Vivien和M. C. 里纳德 递增指针和转义分析。 在ACM SIGPLAN编程语言设计与实现会议（PLDIACM Press，2001.[47] J. Whaley和M. C. 里纳德 java程序的组合指针和转义分析。在ACM SIGPLAN会议上，面向对象编程系统，语言应用（OOPSLAACM Press，1999.[48] K. Zee和M.里纳德通过静态分析编写屏障移除。在第17届面向对象编程、系统、语言和应用年度ACM会议（OOPSLAACM Press，November 2002.
