Trace effects and object orientation

13 years 9 months ago

Download www.cs.uvm.edu

fects are statically generated program abstractions, that can be model checked for veriﬁcation 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 signiﬁcantly 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 ﬂexible trace effect analysis in an Object Oriented setting. Categories and Subject Descriptors D.3.1 [Programming Languages]: Language Classiﬁcations—Object oriented languages; D.3.3 [Programming Languages]: Language Constructs and Features—Polymorphism General Terms Security, Languages, Theory, Veriﬁcation. Keywords Type and effect, type constraints, temporal ...

Christian Skalka

Real-time Traffic