Pattern-Based Precondition Inference from Method Implementations

Overview & Synopsis

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.