Trace effects and object orientation
Christian Skalka · 2005
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 an Object Oriented setting.