Types and trace effects for object orientation
Types and trace effects for object orientation
复制标题
面向对象的类型和跟踪效果
DOI：
10.1007/s10990-008-9032-6
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
C. Skalka
中科院分区：
文献类型：
--
作者：
C. Skalka
跟踪效果是静态生成的程序抽象，可以通过模型检查来验证时态程序逻辑中的断言。在本文中，我们开发了一个类型和效果分析，以获得跟踪效果的面向对象程序在轻量级Java。我们观察到，跟踪行为与继承和其他面向对象的功能，特别是覆盖的方法，动态调度和向下转换的相互作用，分析显着复杂。我们提出了一个表达类型和效果推理算法相结合的多态性和子类型/subeffecting约束，以获得一个灵活的跟踪效果分析，在这种情况下，并显示这些技术是如何适用于面向对象的功能。我们还扩展了基本的语言模型与异常和基于堆栈的事件上下文，并显示如何跟踪效果的规模，这些扩展的结构转换。
Trace effects are statically generated program abstractions, that can be model checked for verification of assertions in a temporal program logic. In this paper we develop a type and effect analysis for obtaining trace effects of Object Oriented programs in Featherweight Java. We observe that the analysis is significantly complicated by the interaction of trace behavior with inheritance and other Object Oriented features, particularly overridden methods, dynamic dispatch, and downcasting. We propose an expressive type and effect inference algorithm combining polymorphism and subtyping/subeffecting constraints to obtain a flexible trace effect analysis in this setting, and show how these techniques are applicable to Object Oriented features. We also extend the basic language model with exceptions and stack-based event contexts, and show how trace effects scale to these extensions by structural transformations.