Producing specifications by dynamic (runtime) analysis of program executions is potentially unsound, because the analyzed executions may not fully characterize all possible executions of the program. In practice, how accurate are the results of a dynamic analysis? This paper describes the results of an investigation into this question, determining how much specifications generalized from program runs must be changed in order to be verified by a static checker. Surprisingly, small test suites captured nearly all program behavior required by a specific type of static checking; the static checker guaranteed that the implementations satisfy the generated specifications, and ensured the absence of runtime exceptions. Measured against this verification task, the generated specifications scored over 90% on precision, a measure of soundness, and on recall, a measure of completeness.This is a positive result for testing, because it suggests that dynamic analyses can capture all semantic information of interest for certain applications. The experimental results demonstrate that a specific technique, dynamic invariant detection, is effective at generating consistent, sufficient specifications for use by a static checker. Finally, the research shows that combining static and dynamic analyses over program specifications has benefits for users of each technique, guaranteeing soundness of the dynamic analysis and lessening the annotation burden for users of the static analysis.

Static checking can verify the absence of errors in a program, but often requires written annotations or specifications. As a result, static checking can be difficult to use effectively: it can be difficult to determine a specification and tedious to annotate programs. Automated tools that aid the annotation process can decrease the cost of static checking and enable it to be more widely used.This paper describes an evaluation of the effectiveness of two techniques, one static and one dynamic, to assist the annotation process. We quantitatively and qualitatively evaluate 41 programmers using ESC/Java in a program verification task over three small programs, using Houdini for static inference and Daikon for dynamic inference. We also investigate the effect of unsoundness in the dynamic analysis.Statistically significant results show that both inference tools improve task completion; Daikon enables users to express more correct invariants; unsoundness of the dynamic analysis is little hindrance to users; and users imperfectly exploit Houdini. Interviews indicate that beginning users found Daikon to be helpful; Houdini to be neutral; static checking to be of potential practical use; and both assistance tools to have unique benefits.Our observations not only provide a critical evaluation of these two techniques, but also highlight important considerations for creating future assistance tools.