Automatic Generation and Checking of Program Specifications
Jeremy W. Nimmer · DSpace@MIT (Massachusetts Institute of Technology) · 2002
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, comparing specifications generalized from program runs with specifications verified by a static checker.The surprising result is that for a collection of modest programs, small test suites captured all or nearly all program behavior necessary for a specific type of static checking, permitting the inference and verification of useful specifications.For ten programs of 100-800 lines, the average precision, a measure of correctness, was .95 and the average recall, a measure of completeness, was .94.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.Finally, the research shows that combining static and dynamic analyses over program specifications has benefits for users of each technique.