這是這個循環的正確不變嗎？

Question

這對於在陣列中的線性搜索僞代碼，如果在陣列A所需元素e被發現返回一個索引i，NIL否則（這是來自CLRS書，第3版，運動2.1-3）：

LINEAR_SEARCH (A, e) 
    for i = 1 to A.length 
     if A[i] == e 
      return i 
    return NIL 

我試圖從中推斷循環不變的，所以根據我的理解，我認爲，一個是由事實來表示，在循環中任何時刻子陣列A[1..i-1]只包含其值平等測試證明是錯誤的。

具體而言，在第一次迭代i-1 == 0這意味着該子陣列的長度爲空之前，因此不能有屬於它使得v == e元件v。在進行任何下一次迭代之前，作爲退出條件的等同性測試，假定的不變性必須保持爲真，否則循環已經結束。一旦終止，它要麼是功能即將返回的索引（在這種情況下，循環不變是平凡真實的），或NIL返回（在這種情況下i == A.length + 1，所以循環不變任何1 < j < i也是如此）。

以上是否正確？如果不是，你能否提供一個正確的循環不變式？

感謝您的關注。

Answer 1

• 循環不變：在for循環的每個迭代開始，我們有A[j] != e所有j < i。

• 初始化：在第一次循環迭代之前，由於數組爲空，所以不變量保持不變。

• 維護：該循環不變式被保持在每一次迭代中，因爲否則在i次迭代有一些j < i使得A[j] == e。但是，在這種情況下，對於循環的第j次循環，返回值j，並且循環沒有第012次迭代，這是一個矛盾。

• 端接當循環終止，可能有兩種情況：一種是其後i <= A.length迭代終止，並且返回i，在這種情況下if條件確保A[i] == e。另一種情況是，i超過A.length，在這種情況下，通過我們對所有j <= A.length，A[j] != e，該返回NIL是正確的循環不變。