Types and trace effects for object orientation

11 years 1 months ago
Types and trace effects for object orientation
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. Keywords Static type analysis
Christian Skalka
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2008
Where LISP
Authors Christian Skalka
Comments (0)