複製鏈接
請複製以下鏈接發送給好友
https://baike.baidu.hk/item/循環不變代碼外提/22787423
複製
複製成功

循環不變代碼外提

鎖定
在計算機科學中，循環不變量是程序循環的一個屬性，在每次迭代之前（和之後）都是真的。 這是一個邏輯斷言，有時通過斷言調用在代碼中檢查。 瞭解其不變量對於理解循環的影響至關重要。
在正式程序驗證中，特別是Floyd-Hoare方法，循環不變量由形式謂詞邏輯表示，並用於證明循環的屬性和通過使用循環的擴展算法（通常是正確性屬性）。 循環不變量在進入循環並且在每次迭代之後都是真的，因此在從循環退出時，可以保證循環不變量和循環終止條件。
中文名
循環不變代碼外提
領    域
計算機科學

目錄

  1. 1 非正式的例子
  2. 2 編程語言支持
  3. ▪ Eiffel
  4. ▪ Whiley
  5. 3 使用循環不變量

循環不變代碼外提非正式的例子

下面的C子例程max（）返回其參數數組a []中的最大值，前提是它的長度n至少為1.註釋在第3,6,9,11和13行提供。每個註釋都有一個關於它的斷言 函數該階段的一個或多個變量的值。 循環體內，循環開始和結束時（第6行和第11行）的突出顯示的斷言完全相同。 因此，它們描述了循環的不變屬性。 當到達第13行時，該不變量仍然成立，並且已知來自第5行的循環條件i！= n變為假。 兩個屬性一起暗示m等於[0 ... n-1]中的最大值，即，從第14行返回正確的值。
int max(int n,const int a[]) {
    int m = a[0];
        // m equals the maximum value in a[0...0]
    int i = 1;    
    while (i != n) {
            // m equals the maximum value in a[0...i-1]        
            if (m < a[i])            
            m = a[i];
                    // m equals the maximum value in a[0...i]        
                    ++i;        // m equals the maximum value in a[0...i-1]    }
                        // m equals the maximum value in a[0...i-1]
                        , and i==n 
      return m;}
在防禦性編程範例之後，第5行中的循環條件i！= n應該更好地修改為i <n，以避免對n的非法負值進行無限循環。 雖然代碼中的這種變化直觀地應該沒有區別，導致其正確性的推理變得有點複雜，因為那時只有i> = n在第13行中已知。為了獲得它，i <= n成立， 條件必須包含在循環不變量中。 很容易看出i <= n也是循環的不變量，因為第6行中的i <n可以從第5行中的（修改的）循環條件獲得，因此i <= n保持在行中 在第10行中增加了i之後的情況。但是，當必須手動提供循環不變量以進行正式程序驗證時，諸如i <= n之類的直觀明顯的屬性經常被忽略。

循環不變代碼外提編程語言支持

循環不變代碼外提Eiffel

Eiffel編程語言為循環不變量提供原生支持。[4] 循環不變量用與類不變量相同的語法表示。 在下面的示例中，循環不變表達式x <= 10必須在循環初始化之後為真，並且在每次執行循環體之後; 這在運行時檢查。
 from        x := 0    invariant        x <= 10    until        x > 10    loop        x := x + 1    end

循環不變代碼外提Whiley

Whiley編程語言還為循環不變量提供了一流的支持。循環不變量使用一個或多個where子句表示，如下所示：
function max(int[] items) -> (int r)// Requires at least one element to compute maxrequires |items| > 0// (1) Result is not smaller than any elementensures all { i in 0..|items| | items[i] <= r }// (2) Result matches at least one elementensures some { i in 0..|items| | items[i] == r }:    //    nat i = 1    int m = items[0]    //    while i < |items|    // (1) No item seen so far is larger than m    where all { k in 0..i | items[k] <= m }    // (2) One or more items seen so far matches m    where some { k in 0..i | items[k] == m }:        if items[i] > m:            m = items[i]        i = i + 1    //    return m
max（）函數確定整數數組中的最大元素。要定義它，數組必須至少包含一個元素。 max（）的後置條件要求返回的值為：（1）不小於任何元素;並且，（2）它匹配至少一個元素。循環不變量通過兩個where子句歸納地定義，每個子句對應於後置條件中的子句。根本區別在於循環不變量的每個子句將結果標識為正確到當前元素i，而後置條件將結果標識為對所有元素都是正確的 [1]  。

循環不變代碼外提使用循環不變量

循環不變量可以用於以下目的之一：
純粹的紀錄片
通過斷言調用在代碼中進行檢查。
根據Floyd-Hoare方法進行驗證。
對於1.，自然語言註釋（如// m等於上例中[0 ... i-1]中的最大值）就足夠了。
對於2.，需要編程語言支持，例如C庫assert.h，或上面顯示的Eiffel中的不變子句。通常，運行時檢查可以通過編譯器或運行時選項打開（用於調試運行）和關閉（用於生產運行）。
對於3.，存在一些工具來支持數學證明，通常基於上面給出的Floyd-Hoare規則，給定的循環代碼實際上滿足給定的（一組）循環不變量。
抽象解釋技術可用於自動檢測給定代碼的循環不變量。但是，這種方法僅限於非常簡單的不變量（例如0 <= i && i <= n && i%2 == 0）。
參考資料