【正文】 iants 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。 and graph g is acyclic. Invariants explicate data structures and algorithms and are helpful for programming tasks from design to maintenance. As one example, they identify program properties that must be preserved when modifying code. Despite their advantages, invariants are usually missing from programs. An alternative to expecting programmers to fully annotate code with invariants is to automatically infer likely invariants from the program itself. This research focuses on dynamic techniques for discovering invariants from execution traces. A dynamic detector of program invariants examines variable values captured during execution over a test suite and reports properties and relationships that hold over those values. This chapter discusses how to obtain invariants (Section ), introduces dynamic in variant detection (Section ), discusses two issues having to do with the use of a dynamic technique (test suites in Section and usage properties in Section ), lists some uses for invariants (Section ), lists the contributions of the dissertation (Section ), and gives a roadmap to the remainder of the document (Section ). Ways to obtain invariants I contend that most programmers have invariants in mind,consciously or unconsciously, when they write or otherwise manipulate programs: they have an idea of how the system works or is intended to work, how the data structures are laid out and related to one another, and the like. Regrettably, these notions are rarely written down, and so most programs are pletely lacking in formal or informal invariants and other documentation. An alternative to expecting programmers to annotate code with invariants is to auto matically infer invariants. Invariant detection recovers a hidden part of the design space: the invariants that the programmer had in mind. This can be done either statically or dynamically. Static analysis examines the program text and reasons over the possible executions and runtime states. The most mon static analysis is dataflow analysis, with abstract interpretation as its theoretical underpinning. The results of a conservative, sound analysis are guaranteed to be true for all possible executions。 n = (for all nodes n)。 x abs(y)。動(dòng)態(tài)檢測(cè)程序不變量可以送入到一個(gè)自動(dòng)化系統(tǒng)，減少人們?nèi)謩?dòng)注釋程序的必要，去支持不變量的屬性 —— 一項(xiàng)很少程序員會(huì)擅長(zhǎng)或享受的任務(wù)。原理證明，流量分析，模型檢查，以 用其它自動(dòng)或半自動(dòng)機(jī)制，能通 5 過(guò)觀察，確認(rèn)安全屬性例如在執(zhí)行時(shí)邊界溢出或空指針引用，建立或終止響應(yīng)，以及其它方法來(lái)在執(zhí)行時(shí)增加，分辨程序正確性。不變量是數(shù)據(jù)結(jié)構(gòu)，而不是內(nèi)存位置或寄存器的不變量，能使整個(gè)數(shù)據(jù)結(jié)構(gòu)作業(yè)，避免或優(yōu)化。舉個(gè)例子，不變量命名別名是在運(yùn)行時(shí)的點(diǎn)同等測(cè)試，專業(yè)化的程序版本中已別名和未別名的用例比普通用例更有效。簡(jiǎn)介直接編譯使 用信息聚集在先前的運(yùn)行來(lái)優(yōu)化。相互的，新的測(cè)試能觀察在程序運(yùn)行的不變量，測(cè)試套件能描程序或部件的實(shí)際，正確的使用。這些不變量能幫助測(cè)試用例以一個(gè)或兩個(gè)不同的方式產(chǎn)生。一個(gè)不變量可能會(huì)揭露程序只能操作小值，或一些值經(jīng)常存在相互間特別關(guān)系。 有效的測(cè)試套件。不尋?；虍惓Ｇ闆r能指示錯(cuò)誤或特別的情況，進(jìn)而引起程序員的注意。動(dòng)態(tài)檢測(cè)不變量也能形成程序范圍，能指出變化的程序?qū)傩曰蜉斎氩⒛茏鳛榱硪环秶褂?。例子包括程序?zhí)行的行集（或路徑），輸出的大小，運(yùn)行時(shí)間，或靜態(tài)屬性，例如資源復(fù)雜 [McC76]。 形成范圍。 不管是靜態(tài)還是動(dòng)態(tài)區(qū)分不變量都作為以上所述使用（除了第一個(gè)，用于程序設(shè)計(jì)）。 幫助程序員避免產(chǎn)生錯(cuò)誤是最初動(dòng)態(tài)不變量檢測(cè)的動(dòng)力。在一點(diǎn)上確 定的不變量可能依賴于其它地方，但如果原始的不變量不是被文檔化，少依賴，那么程序員很容易會(huì)違反它，在程序的某個(gè)遠(yuǎn)部分產(chǎn)生錯(cuò)誤。不變量能阻止程序員因疏忽而違反程序正確行為的假設(shè)而做改變。程序類型是另一種這樣的假設(shè)，能在編譯，運(yùn)行，或兩者都是時(shí)被檢查。 4 檢查假定。先關(guān)聯(lián)的不變量能檢查和定義編程提供不變量；程序自檢通常過(guò)時(shí)，無(wú)效或不正確 [LCKS90]。 定義文檔。例如，他們認(rèn)為程序的理解在某些程度上是每個(gè)程序運(yùn)算的先提條件。 文檔代碼。更正式的思考代碼能影響 更多有規(guī)律的設(shè)計(jì)和執(zhí)行，即使是非正規(guī)的使用不變量也對(duì)程序員有幫助 [HHJ+87b， HHJ+87a].其他作者建