程序不变量外文翻译(编辑修改稿)

程序不变量外文翻译(编辑修改稿)内容摘要：

ariant detector, which is named after an Asian radish. Dynamic invariant detection discovers likely invariants from program executions by in strumenting the target program to trace certain variables, running the instrumented pro gram over a test suite, and inferring invariants over both the instrumented variables and derived variables not manifest in the program. All of the steps are fully automatic (except selecting a test suite). The currentlyexisting instrumenters are sourcetosource translators for C, Java, and Lisp。 we use the terms “instrumenter” and “front end” interchangeably. The inference step tests possible invariants against the values captured from the instru mented variables. Prop erties that are satisfied over all the values, and that also satisfy other tests, such as being statistically justified, not being over unrelated variables, and not being implied by other reported invariants, are reported as likely invariants. Running the program Dynamic analysis requires executing the target program. A test suite’s benefits outweigh its costs even in the absence of dynamic invariant detection, for i t enables other dynamic techniques such as (regression) testing. Indeed, a program lacking a test suite (or that cannot be run or never has) is likely to have many problems that should be addressed using standard techniques before invariants are detected over it. As with other dynamic approaches such as testing and profiling,the accuracy of the inferred invariants depends in part on the quality and prehensiveness of the test cases. Additional test cases might provide new data from which more accurate invariants can be inferred. The inferred invariants can also validate the test suite by revealing properties true when executing it. Thus, users know whether a test suite is adequate and, if not,are directly informed how to improve practice, standard test suites have performed adequately, and detected invariants are relatively insensitive to the particular test suite, so long as it is large enough (see Chapter 6). However, we are not yet sure of the precise properties that make a test suite good for invariant detection. These are not necessarily the 8 same as make a test suite good for detecting bugs. A test suite that strives for efficiency by executing each statement a minimal number of times would be bad for invariant detection, which requires multiple executions as a basis for generalization so that there is statistical support for the inferences. Like any dynamic analysis, dynamic invariant detection cannot guarantee the plete ness or soundness of its results. It is not plete because there are infinitely many potential invariants that could be reported. However, it is plete for the set of invariants checks。 Daikon’s grammar is given in Section and extended later in the dissertation, most no tably in Section . It is not sound because the test suite may not fully characterize all executions: a property that held for the first 10,000 executions does not necessarily hold on the next one. However, the technique is sound over the training data (all the data presented to it). Although dynamic invariant detection is not plete or sound, it is useful, which is a considerably more important property. (This characterization fits other tools, such as testing, Purify [HJ92], ESC [DLNS98], PREfix [PRE99], and many more.) Additionally, it is plementary to other techniques。 it can shore up the weaknesses of static analysis while static analysis covers for its deficiencies. Functional invariants and usage properties Because the results of dynamic invariant detection depend on the particular test suite, not all reported invariants will be true for every possible execution of the program. The Daikon output can be generally classified into functional invariants and usage properties. A functional invariant depends only on the code for a particular data structure or func tion, and the invariant is universally true for any use of that entity. Usage properties, on the other hand, result from specific usage of a data structure or function。 they depend on the context of use and the test suite. Because i t operates on traces, Daikon cannot distinguish between。