程序不變量外文翻譯

1、<p>　　本科畢業(yè)論文（設(shè)計）</p><p><b>　　譯文和原文</b></p><p><b>　　二〇一二年二月八日</b></p><p><b>　　第一章 前言</b></p><p>　　程序不變量是在特定的一個或多個程序點上永保真值的屬性，如可存

2、在某一斷言語句，形式化規(guī)格說明，或不變式的描述。例如Y=4*X+3；數(shù)組a不包含復(fù)制；n=n；子節(jié)點：父親節(jié)點(給所有節(jié)點n)；size(key)=size(contents)；以及有向無環(huán)圖。</p><p>　　不變量表明了程序的數(shù)據(jù)結(jié)構(gòu)和變量運算規(guī)則，并且有利于程序的維護。例如，當修改代碼時他們定義的程序?qū)傩员仨毐４?。盡管有這些優(yōu)勢，不變量還是經(jīng)常在編程中丟失。此外程序員應(yīng)能從程序中自動推斷出疑似不變量來充

3、分注釋代碼。動態(tài)技術(shù)的研究專注于動態(tài)技術(shù)從運行的軌跡中發(fā)現(xiàn)不變量。一個程序不變量的動態(tài)檢測是檢查變量在一系列測試用例的值并記錄在這些值中的屬性和關(guān)系。</p><p>　　本章節(jié)討論了如何獲得不變量(1.1章節(jié))，介紹動態(tài)不變量檢測(1.2章節(jié))，討論關(guān)于兩個與動態(tài)技術(shù)的運用有關(guān)的觀點(測試集在1.3章節(jié)，屬性的使用在1.4章節(jié))，列舉不變量的使用(1.5章節(jié))，列舉關(guān)于論文的貢獻者(1.6章節(jié))，給出其余文件的

4、路線圖(1.7章節(jié))。</p><p>　　1.1 獲取不變量的方法</p><p>　　程序員在寫程序或者用其他方式操作程序時，應(yīng)該有意識的加入程序不變量，因為這樣可以很好的把握系統(tǒng)的運行情況，可以清楚的描述數(shù)據(jù)結(jié)構(gòu)以及表達變量之間的關(guān)系等。但是比較可惜的是，這一主張在實際編碼過程中幾乎沒有得到應(yīng)用，因此大多數(shù)程序完全缺乏正式的或者非正式的不變量分析。</p><p&

5、gt;　　另一方面，程序員應(yīng)在用不變量注釋代碼時能自動的推測出不變量。不變量檢測包含在設(shè)計空間的隱藏部分：程序員腦海里所想的不變量。不變量檢測是動態(tài)或靜態(tài)的。</p><p>　　靜態(tài)分析檢測程序測試并找出可能的執(zhí)行和運行時間狀態(tài)。最普遍的靜態(tài)分析是數(shù)據(jù)流分析，用抽象作為其理論解釋依據(jù)。傳統(tǒng)，健全的分析結(jié)果能保證所有可能的執(zhí)行為真；由于編譯器和其它一些系統(tǒng)不是面向用戶，它在一些對正確性要求嚴格時非常合適。<

6、/p><p>　　靜態(tài)分析有局限性。它不能真實的報告除了不可判定的屬性或程序上下文的屬性。在靜態(tài)分析程序中運用了語言的特征，例由于堆棧近似值的精度缺失而難以表示并會產(chǎn)生較弱的結(jié)果，指針會余留在技術(shù)狀態(tài)那邊。動態(tài)分析在這些執(zhí)行中運行程序，檢查執(zhí)行并報告屬性，且不受這些缺點影響同時互補靜態(tài)分析。</p><p>　　1.2 動態(tài)不變量檢測</p><p>　　本研究主要專注

7、動態(tài)發(fā)現(xiàn)不變量：這個技術(shù)是通過執(zhí)行一個關(guān)于程序集的輸入以及從獲得的不變量軌跡中推測出的不變量。圖1.1顯示的是以一亞洲人命名的不變量檢測工具Daikon的高層體系結(jié)構(gòu)。</p><p>　　動態(tài)不變量檢測從程序執(zhí)行中發(fā)現(xiàn)疑似不變量，通過指令目標程序去產(chǎn)生一些確定值，通過測試套件運行機器程序，推論編譯的不變量并獲得未在程序中顯露不變量。</p><p>　　所有的步驟都是自動的（除了選擇測試

8、套件）?，F(xiàn)在存在的工具是資源到資源翻譯的C，Java，Lisp；我們使用的是工具和前后交互模式。</p><p>　　推論步驟測試可能的不變量對于那些從指令值獲得的值。滿足所有值，并能滿足其它測試，例如數(shù)據(jù)合理性，不被相關(guān)聯(lián)值，不被其它報告的不變量所包含的屬性才稱為可能不變量。</p><p><b>　　1.3運行程序</b></p><p>

9、;　　動態(tài)分析需要執(zhí)行的目標程序。一個好的測試套件的好處大于它的花費，即使是沒有動態(tài)不變量的檢測下，它還能使用于其它動態(tài)技術(shù)例如（回歸）測試。的確，一個程序缺少測試套件（不能運行或沒有）可能會出現(xiàn)很多問題，并應(yīng)在不變量檢測前用標準技術(shù)來改正之。</p><p>　　與其它的動態(tài)測試或研究方法相比，推斷不變量的準確性取決于測試用例的質(zhì)量及理解性。額外的測試用例可能會提供一些新數(shù)據(jù)，以推斷出更準確的不變量。推斷的不變

10、量可在執(zhí)行時通過揭示屬性為真來驗證測試套件。這樣，用戶才知道這個測試套件是否足夠，如果不是，則直接告知怎樣改進它。</p><p>　　事實上，標準的測試套件是很合適的，且能從特別的相對不敏感套件中檢測不變量，只要它足夠大（參見第6章）。然而，我們還不知道確切的屬性從而使測試套件能良好檢測錯誤。這些不盡相同使測試套件能夠檢測缺陷。測試套件執(zhí)行的效率如果是通用最小次數(shù)來執(zhí)行每條語句，那么它對不變量檢測不好，它需要重

11、復(fù)的執(zhí)行作為歸納基礎(chǔ)，并有統(tǒng)計數(shù)據(jù)作為推論的支持。</p><p>　　在任何動態(tài)分析中，動態(tài)不變量檢測都不能保證其結(jié)果的完整性或正確性。它不完整因為這可能報告出很多不確定的潛在不變量。然而，它又是完整的，因為它檢查的不變量集；Daikon的語法在3.2節(jié)給出并在后面的論文中擴展，大多數(shù)在4.3節(jié)。它不準確因為測試套件不能列出所有的執(zhí)行：存在前10000次執(zhí)行后的屬性不一定存在下一個里。然而，技術(shù)在這些訓(xùn)練數(shù)據(jù)（

12、所有呈現(xiàn)的數(shù)據(jù)）又是準確的。</p><p>　　雖然動態(tài)不變量檢測不夠完整和準確，它還是很有用的，也是相當重要的財產(chǎn)。（這包括適合其它工具，例如測試，Purify[HJ92]，ESC[DLNS98],PREfix[PRE99]，等等。）此外，它能與其它工具互補；能彌補靜態(tài)分析的缺陷，而靜態(tài)分析也能覆蓋它的缺陷。</p><p>　　1.4 功能不變量和使用性能</p>&l

13、t;p>　　動態(tài)不變量檢測的結(jié)果取決于特別的測試套件，不是所有報告的不變量能在每一可能執(zhí)行的程序為真。Daikon輸出分為功能不變量和使用內(nèi)容。</p><p>　　功能不變量只取決于特定數(shù)據(jù)結(jié)構(gòu)或功能的代碼，不變量普遍適用于此種實體。另一方面，使用屬性是由數(shù)據(jù)結(jié)構(gòu)或功能的特別功能所產(chǎn)生的；它們?nèi)Q于使用背景和測試套件。因為它依賴于操作的軌跡。（第4章和第4.5章的統(tǒng)計明顯表明能區(qū)分它們。也能區(qū)分測試套件。

14、）人們通常不能分辨兩者。功能不變量和使用屬性的區(qū)別是在一系統(tǒng)的入口和出口—Java或C語言主程序的開始或結(jié)束。在其他程序點它們的區(qū)別更清楚。比如，關(guān)于一個程序的論證是有效的這么一個前提陳述，可以作為程序功能不變量或訪問者的使用屬性，并注意不要提供提供不合法的值。（在正式詳細文獻上，如果前提條件，如果符合，并保證了后置條件在出口處為真，則退出。所有由Daikon所報告的前提條件和后置條件要符合此準則，即使Daikon的前提條件不會成為最弱

15、的前提條件。）</p><p>　　使用內(nèi)容在解釋文檔操作或一個數(shù)據(jù)結(jié)構(gòu)使用的功能的界限文檔時很有用。因為功能不變量和使用屬性間的區(qū)別與程序員的工作狀態(tài)有關(guān)，我們會從此把檢測作為首要目標。</p><p>　　1.5 不變量的使用</p><p>　　不變量對人類和工具，程序的所有方面，包括設(shè)計，編程，測試，優(yōu)化以及維護都很有用。這一章節(jié)列了不變量的一些應(yīng)用，去作為

16、程序員們?yōu)槭裁搓P(guān)注它們并從程序中跟蹤它們并是很值得的目標的動力。</p><p>　　編寫更好的程序。一些作者已經(jīng)注明了好的程序?qū)Υa的軌跡有影響當不變量運用在他們的設(shè)計時[Gri81,LG86]，不變量準確的正式化代碼的合約，能區(qū)分它有意的操作并在完成時指示。更正式的思考代碼能影響更多有規(guī)律的設(shè)計和執(zhí)行，即使是非正規(guī)的使用不變量也對程序員有幫助[HHJ+87b，HHJ+87a].其他作者建議把不變量作為注釋的一

17、個必要部分，在程序中定義個說明[CM88,BG93，F(xiàn)M97]。雖然這些使用是有用的，論文關(guān)注不變量在已構(gòu)建程序中的使用。</p><p>　　文檔代碼。不變量注重程序執(zhí)行某些方面和提供有用的程序操作文檔，算法和數(shù)據(jù)結(jié)構(gòu)。例如，他們認為程序的理解在某些程度上是每個程序運算的先提條件。文檔是從至今為止的程序中自動提取出來的，不像人們所寫的的信息，當代碼變了時則需被更新。 </p><p>

18、　　定義文檔。自動關(guān)聯(lián)不變量對已注注釋文檔，斷言陳述，或規(guī)格說明的代碼很有用。先關(guān)聯(lián)的不變量能檢查和定義編程提供不變量；程序自檢通常過時，無效或不正確[LCKS90]。此外，人們相互檢查是比較弱的因為不同的人傾向于犯同樣的錯[KL86]。</p><p>　　檢查假定。不變量能插入程序中作為斷言陳述為以后的測試或確認檢測不變量不是違反后來的代碼演變。程序類型是另一種這樣的假設(shè)，能在編譯，運行，或兩者都是時被檢查。

19、</p><p>　　避免缺陷。不變量能阻止程序員因疏忽而違反程序正確行為的假設(shè)而做改變。當改變時，現(xiàn)有的程序中明確的不變量的缺失使得程序員更易產(chǎn)生錯誤。在一點上確定的不變量可能依賴于其它地方，但如果原始的不變量不是被文檔化，少依賴，那么程序員很容易會違反它，在程序的某個遠部分產(chǎn)生錯誤。程序維護產(chǎn)生錯誤[OC89，GKMS00]，以及更多，大多數(shù)是因為違反不變量。</p><p>　　幫助

20、程序員避免產(chǎn)生錯誤是最初動態(tài)不變量檢測的動力。這個活動和檢測缺陷一樣有價值（即使數(shù)量困難少量），因為阻止一個問題比后來再修改更簡單也更便宜。</p><p>　　不管是靜態(tài)還是動態(tài)區(qū)分不變量都作為以上所述使用（除了第一個，用于程序設(shè)計）。其它的運用，動態(tài)檢測不變量比靜態(tài)不變量檢測更有用。</p><p>　　形成范圍。一個程序范圍[AFMS96，RBDL97，HRWY98]是程序任何可度量

21、的屬性或它的執(zhí)行。例子包括程序執(zhí)行的行集（或路徑），輸出的大小，運行時間，或靜態(tài)屬性，例如資源復(fù)雜[McC76]。通常，一個范圍可以當做一個摘要或哈希代碼；程序范圍的不同能指出或描繪程序，輸入或執(zhí)行的不同。動態(tài)檢測不變量也能形成程序范圍，能指出變化的程序?qū)傩曰蜉斎氩⒛茏鳛榱硪环秶褂谩?lt;/p><p>　　找出不同的條件。不尋?；虍惓Ｇ闆r能指示錯誤或特別的情況，進而引起程序員的注意。一個近而真的不變量能指示環(huán)境需

22、要特別注意或一個異常輸入。</p><p>　　有效的測試套件。動態(tài)檢測不變量能揭露程序本身測試套件，因為屬性反映了程序在運行測試套件。一個不變量可能會揭露程序只能操作小值，或一些值經(jīng)常存在相互間特別關(guān)系。這些屬性可能會指示程序值（和狀態(tài)）覆蓋不足和程序行為鍛煉不足，即使套件覆蓋程序的每行或路徑。這些不變量能幫助測試用例以一個或兩個不同的方式產(chǎn)生。新的測試能明顯違反不變量[TCMM98]，通過擴大值的覆蓋來提升套

23、件（類似擴大而不是操作范圍[CR99]，它需要兩個值必須有不同的值）。相互的，新的測試能觀察在程序運行的不變量，測試套件能描程序或部件的實際，正確的使用。</p><p>　　優(yōu)化公共用例。簡介直接編譯使用信息聚集在先前的運行來優(yōu)化。如果一個特別的值或情況是普遍，便宜去測試，以用允許有用的專門化當它運行時，那么一個編譯（在其它技術(shù)中）能插入檢查和擴展成一個專門化代碼版本，并假設(shè)制約。舉個例子，不變量命名別名是在運

24、行時的點同等測試，專業(yè)化的程序版本中已別名和未別名的用例比普通用例更有效。</p><p>　　低級執(zhí)行信息用于預(yù)置文件編輯（通常是最常用的單變量值），它能擴張高級不變量，更好的優(yōu)化普通用例。不變量是數(shù)據(jù)結(jié)構(gòu)，而不是內(nèi)存位置或寄存器的不變量，能使整個數(shù)據(jù)結(jié)構(gòu)作業(yè)，避免或優(yōu)化。</p><p>　　自舉證明。原理證明，流量分析，模型檢查，以用其它自動或半自動機制，能通過觀察，確認安全屬性例如

25、在執(zhí)行時邊界溢出或空指針引用，建立或終止響應(yīng)，以及其它方法來在執(zhí)行時增加，分辨程序正確性。然而，它們是單調(diào)而易出錯的，人們很難去區(qū)分將證明的屬性，現(xiàn)在的系統(tǒng)難以假設(shè)它們；某些研究者認為任務(wù)比演示證明更難[Weg74,BLS96]。動態(tài)檢測程序不變量可以送入到一個自動化系統(tǒng)，減少人們?nèi)謩幼⑨尦绦虻谋匾?，去支持不變量的屬性——一項很少程序員會擅長或享受的任務(wù)。</p><p>　　Chapter 1</p&

26、gt;<p>　　Introduction</p><p>　　A program invariant is a property that is true at a particular program point or points, such as might be found in an assert statement, a formal specification, or a repr

27、esenta- tion invariant. Examples include y = 4 ? x + 3; x > abs(y); array a contains no duplicates; n = n.child.parent (for all nodes n); size(keys) = size(contents); and graph g is acyclic.</p><p>　　Inva

28、riants 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

29、 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 resea

30、rch focuses on dynamic techniques for discovering invari</p><p>　　This chapter discusses how to obtain invariants (Section 1.1), introduces dynamic in- variant detection (Section 1.2), discusses two issues h

31、aving to do with the use of a dynamic technique (test suites in Section 1.3 and usage properties in Section 1.4), lists some uses for invariants (Section 1.5), lists the contributions of the dissertation (Section 1.6),

32、and gives a roadmap to the remainder of the document (Section 1.7).</p><p>　　1.1 Ways to obtain invariants</p><p>　　I contend that most programmers have invariants in mind,consciously or uncon

33、sciously, 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, th

34、ese notions are rarely written down, and so most programs are completely lacking in formal or informal invariants and other documentation.</p><p>　　An alternative to expecting programmers to annotate code wi

35、th 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.<

36、;/p><p>　　Static analysis examines the program text and reasons over the possible executions and runtime states. The most common static analysis is dataflow analysis, with abstract interpretation as its theoret

37、ical underpinning. The results of a conservative, sound analysis are guaranteed to be true for all possible executions; itis most appropriate when correctness is crucial, as for compilers and some other systems whose con

38、sumer is not a human.</p><p>　　Static analysis has a number of limitations. </p><p>　　It cannot report true but undecidable properties or properties of the program context. Static analysis of

39、programs using language features such as pointers remains beyond the state of the art because the difficulty of representing the heap forces precision-losing approximations and produces weak results. Dynamic analysis, w

40、hich runs the program, examines the executions, and reports properties over those executions, does not suffer these drawbacks and so complements static analysis.</p><p>　　1.2 Dynamic invariant detection</

41、p><p>　　This research focuses on the dynamic discovery of invariants: the technique is to execute a program on a collection of inputs and infer invariants from captured variable traces. Figure 1.1 shows the hi

42、gh-level architecture of the Daikon invariant detector, which is named after an Asian radish.</p><p>　　Dynamic invariant detection discovers likely invariants from program executions by in- strumenting the t

43、arget 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.</p>

44、<p>　　All of the steps are fully automatic (except selecting a test suite). The currently-existing instrumenters are source-to-source translators for C, Java, and Lisp; we use the terms “instrumenter” and “front e

45、nd” interchangeably.</p><p>　　The inference step tests possible invariants against the values captured from the instru- mented variables. Properties that are satisfied over all the values, and that also sati

46、sfy 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.</p><p>　　1.3 Running the pro

47、gram</p><p>　　Dynamic analysis requires executing the target program. A test suite’s benefits outweigh its costs even in the absence of dynamic invariant detection, for it enables other dynamic techniques su

48、ch 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

49、 over it.</p><p>　　As with other dynamic approaches such as testing and profiling,the accuracy of the inferred invariants depends in part on the quality and comprehensiveness of the test cases. Additional te

50、st 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 tes

51、t suite is adequate and, if not,are directly informed how to improve it.In practice, standar</p><p>　　Like any dynamic analysis, dynamic invariant detection cannot guarantee the complete- ness or soundness o

52、f its results. It is not complete because there are infinitely many potential invariants that could be reported. However, it is complete for the set of invariants checks; Daikon’s grammar is given in Section 3.2 and ext

53、ended later in the dissertation, most no- tably in Section 4.3. It is not sound because the test suite may not fully characterize all executions: a property that held for the </p><p>　　Although dynamic invar

54、iant detection is not complete 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 m

55、ore.) Additionally, it is complementary to other techniques; it can shore up the weaknesses of static analysis while static analysis covers for its deficiencies.</p><p>　　1.4 Functional invariants and usage

56、 properties</p><p>　　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 o

57、utput can be generally classified into functional invariants and usage properties.</p><p>　　A functional invariant depends only on the code for a particular data structure or func- tion, and the invariant is

58、 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 it operates o

59、n traces, Daikon cannot distinguish between these classes, which are intermingled in its output. (The heuristics of Chapter 4, and notably the statistical checks o</p><p>　　People cannot necessarily discri

60、minate between the two, either. The distinction between functional invariants and usage properties is clear only at a system’s entry and exit — for a standalone Java or C program, at the beginning and end of the main ro

61、utine. At other points in the program, the differences are less clear. For instance, a precondition stating that a procedure’s arguments are valid can be viewed as a functional invariant of the procedure or as a usage pr

62、operty of the callers, which</p><p>　　1.5 Uses for invariants</p><p>　　Invariants are useful, to humans and to tools, in all aspects of programming, including design, coding, testing, optimizati

63、on, and maintenance. This section lists some uses of invariants, to motivate why programmers care about them and why extracting them from programs is a worthwhile goal.</p><p>　　Write better programs. A

64、number of authors have noted that better programs result when invariants are used in their design [Gri81, LG86]. Invariants precisely formal- ize the contract of a piece of code, clarifying its inte

65、nded operation and indicating when it is complete.Thinking about code formally can result in more disciplined design and implementation, but even informal use of invariants can help program- mers [HHJ+87b, HHJ+87a]. Oth

66、er authors suggest making invariant</p><p>　　Document code. Invariants characterize certain aspects of program execution and provide valuable documentation of a program’s operation, algorithms, and data stru

67、ctures. As such, they assist program understanding, some level of which is a prerequisite to every program manipulation. Documentation that is automatically extracted from the program is guaranteed to be up-to-date, un

68、like human-written information that may not be updated when the code is.</p><p>　　Refine documentation. Automatically inferred invariants are useful even for code that is already documented with comments, a

69、ssert statements, or specifications. The inferred invariants can check or refine programmer-supplied invariants; program self- checks are often out-of-date, ineffective, or incorrect [LCKS90]. Furthermore, human cross-c

70、hecks are weak because different people tend to make the same mistakes [KL86].</p><p>　　Check assumptions. Invariants can be inserted into a program as assert statements for further testing or to ensure that

71、 detected invariants are not later violated as code evolves. Program types are another such assumption that can be checked at compile time, at run time, or both.</p><p>　　Avoid bugs. Invariants can protect

72、a programmer from making changes that inadvertently violate assumptions upon which the program’s correct behavior depends. The near absence of explicit invariants in existing programs makes it all too easy for programmer

73、s to introduce errors while making changes. An invariant that is established at one point is likely to be depended upon elsewhere, but if the original invariant is not documented, much less the dependence, then it is

74、easy for a programmer to </p><p>　　Helping programmers avoid introducing bugs was the original motivation for dynamic invariant detection. This activity is as valuable as detecting bugs (even if harder to q

75、uantify and less glamorous), because preventing a problem is easier and cheaper than setting it right later on.</p><p>　　Either statically or dynamically specified invariants serve for the uses listed above

76、(ex- cept the first one, use in program design). For the remaining uses, dynamically detected invariants can be even more useful than static ones.</p><p>　　Form a spectrum. A program spectrum [AFMS96, RBDL9

77、7, HRWY98] is any measur- able property of a program or its execution. Examples include the set of lines (or paths) executed by a program, the size of the output, runtime, or static properties such as cyclomatic complexi

78、ty [McC76] of the source. Informally, a spectrum can be thought of as a summary or a hash code; differences between program spectra can indicate or characterize differences between programs, inputs, or executions. Dynami

79、- cally d</p><p>　　Locate unusual conditions. Unusual or exceptional conditions may indicate bugs or spe- cial cases that should be brought to a programmer’s attention. A nearly-true invariant could indicate

80、 a situation requiring special care or an input anomaly.</p><p>　　Validate test suites. Dynamically detected invariants can reveal as much about a test suite as about the program itself, because the properti

81、es reflect the program’s execu- tion over the test suite. An invariant might reveal that the program manipulates only small values, or only positive ones, or that some variables are always in a particular relationship to

82、 one another. These properties may indicate insufficient coverage of program values (and states) and inadequate exercising of program beh</p><p>　　Optimize common cases. Profile-directed compilers optimize

83、 programs using informa- tion gathered on previous runs. If a particular value or condition is common, cheap to test, and permits useful specialization when it holds, then a compiler can (among other techniques) insert c

84、hecks and branch to a specialized version of the code that assumes the condition. As one example, variable aliasing is a pointer equality test at runtime, and the specialized versions of a routine for the aliased and not

85、-a</p><p>　　The low-level execution information used in profile-directed compilation (usually just the most common values for single variables) can be augmented with higher-level invariants to enable better

86、 optimization for the common case. Invariants that refer to program structures rather than memory locations or registers could permit entire data structure operations to be avoided or optimized.</p><p>　　Boo

87、tstrap proofs.Theorem-proving, dataflow analysis, model-checking, and other auto- mated or semi-automated mechanisms can verify the correctness of a program with respect to a specification, confirm safety properties suc

88、h as lack of bounds overruns or null dereferences, establish termination or response properties, and otherwise in- crease confidence in an implementation. However, it can be tedious and error-prone for people to specify