Synthesis of interface specifications for Java classes

While a typical software component has a clearly specified (static) interface in terms of the methods and the input/output types they support, information about the correct sequencing of method calls the client must invoke is usually undocumented. In this paper, we propose a novel solution for automatically extracting such temporal specifications for Java classes. Given a Java class, and a safety property such as "the exception E should not be raised", the corresponding (dynamic) interface is the most general way of invoking the methods in the class so that the safety property is not violated. Our synthesis method first constructs a symbolic representation of the finite state-transition system obtained class using predicate abstraction. Constructing the interface then corresponds to solving a partial-information two-player game on this symbolic graph. We present a sound approach to solve this computationally-hard problem approximately using algorithms for learning finite aut...

• Type: Conference
• Year: 2005
• Where: POPL
• Authors: P. Madhusudan, Pavol Cerný, Rajeev Alur, Wonhong Nam
• Keywords: Partial-information Two-player Game, POPL 2005, Programming Languages, Sample Java2sdk Library, Software Engineering