Mining Temporal Specifications from Object Usage

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