Mining Temporal Specifications from Object Usage

A caller must satisfy the callee\´s precondition--that is, reach a state in which the callee may be called. Preconditions describe the state that needs to be reached, but not how to reach it. We combine static analysis with model checking to mine Computation Tree Logic (CTL) formulas that describe the operations a parameter goes through: "In parseProperties (String xml), the parameter xml normally stems from getProperties()." Such operational preconditions can be learned from program code, and the code can be checked for their violations. Applied to AspectJ, our Tikanga prototype found 189 violations of operational preconditions, uncovering 9 unique defects and 36 unique code smells-with 44% true positives in the 50 top-ranked violations.