Pattern analysis uncovers hidden method requirements in Java code
Pattern-Based Precondition Inference from Method Implementations
Software Engineering
Summary
Many methods in programs need certain conditions to be true before they run correctly, but these conditions are often not clearly explained. The authors created Prex, a tool that looks inside Java code to find these hidden rules by spotting checks that stop bad inputs. Prex also tries to rewrite these rules so other code can check them before calling the method. Their tests showed Prex was accurate and found many rules that programmers hadn’t written down.
What this means in practice
- •For java developers: Automatically extract method preconditions from existing code to improve code safety and maintainability without extra documentation effort.
- •For software quality engineers: Integrate inferred preconditions into testing and verification tools to catch incorrect method usage early in development.
Authors
Shanyue Zhou, Martin P. Robillard
Abstract
Method preconditions define the conditions that must be satisfied before a method is called. Often, such conditions are not documented and must be inferred. We present Prex, a pattern-based static analysis approach that infers preconditions from explicit checks in Java source code. For each precondition, Prex reports the condition required for a valid call and the reported exception in the case of a violation. Prex also attempts code transformations to convert the condition detected within a method's implementation into an expression that can be evaluated by client code. It leverages the concept of a mutation boundary to separate precondition checks from exceptions that may occur after the method changes the program state. We evaluated Prex from 46 open source Java projects and manually reviewed independent samples of 150 reports. Among the 150 Prex reports, 149 were correct and 125 of the correct reports were executable by client code. In a systematic comparison with an alternative approach based on path expansion, Prex provided more precise results. In total, 122 of the 149 correct reports had no relevant method documentation, and 41 required nontrivial source code analysis to recover manually. Overall, explicit source-code checks provide precondition information that can be absent from method documentation, and Prex can help recover it.