Trace effects and object orientation

fects 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. Categories and Subject Descriptors D.3.1 [Programming Languages]: Language Classifications—Object oriented languages; D.3.3 [Programming Languages]: Language Constructs and Features—Polymorphism General Terms Security, Languages, Theory, Verification. Keywords Type and effect, type constraints, temporal ...

• Type: Conference
• Year: 2005
• Where: PPDP
• Authors: Christian Skalka
• Keywords: Effect Analysis, Object Oriented, PPDP 2005, Temporal Program Logic