Automatic Generation of Object Usage Specifications from Large Method Traces

Citations Over TimeTop 1% of 2009 papers

Abstract

Formal specifications are used to identify programming errors, verify the correctness of programs, and as documentation. Unfortunately, producing them is error-prone and time-consuming, so they are rarely used in practice. Inferring specifications from a running application is a promising solution. However, to be practical, such an approach requires special techniques to treat large amounts of runtime data. We present a scalable dynamic analysis that infers specifications of correct method call sequences on multiple related objects. It preprocesses method traces to identify small sets of related objects and method calls which can be analyzed separately. We implemented our approach and applied the analysis to eleven real-world applications and more than 240 million runtime events. The experiments show the scalability of our approach. Moreover, the generated specifications describe correct and typical behavior, and match existing API usage documentation.

Related Papers

• → “So my program doesn’t run!” Definition, origins, and practical expressions of students’ (mis)conceptions of correctness(2008)28 cited
• → A Fault-Localization Approach Based on the Coincidental Correctness Probability(2015)6 cited
• → Program Repair by Stepwise Correctness Enhancement(2016)3 cited
• → On the correctness of problem solving in ancient mathematical procedure texts(2021)2 cited
• → Relative Correctness of Real-Time Systems(1992)