我們如何定義一個循環不變式？

我們知道循環變體被定義爲在循環的每次迭代之前和之後都是真的語句。但是這個定義太鬆了嗎？讓我們看一個具體的例子：線性搜索。我們如何定義一個循環不變式？

輸入：索引：n個A =（A 1 ，一個，一個，...，一個_Ñ）和一個值v

輸出的序列我使得v = A [1]或NIL如果v是沒有在甲

這裏發現是我的僞代碼：

linear_search(A, v) 
1 for i ∈ {1, 2, ..., n} 
2  if A[i] = v 
3   return i 
4 return NIL

因此，一個典型循環不變將會是（因爲我們從左到右搜索）v不在當前索引的左側，或者在數學上不在這個位置P: ∀p ∈ {1, 2, ..., i - 1}, A[p] ≠ v.這很明顯，甚至在開始時也是如此，因爲p∈Ø是假的，這使得P真的，記住每一個普遍量化的陳述都可以被看作是一個有條件的陳述。（但是非正式地考慮它更容易：在開始時，v的左側沒有任何內容。）

我們也可以使用一個條件限制較少的條件語句。在這種情況下，Q: If A[i] = v, then 1 ≤ i ≤ n.很明顯，如果找到v，則情況如此。如果沒有找到v，則A [i] = v是假的，並且無論i的值如何，Q都變爲真。如果我們將算法改爲從右向左搜索，Q也是如此。

也許我們想要的不那麼嚴格。如何使用一個始終如此的陳述？ R: Either A[i] = v or A[i] ≠ v. R在循環的每次迭代之前和之後保持不變。

哪些語句P，Q和R有效用作循環不變式？

來源

2016-11-10 W. Zhu

循環不變應該是循環本身的'有用'屬性。無論循環如何，你的財產R更多是一種重言式。所以IMO只有P和Q可以被認爲是循環不變式，儘管Q較弱。 –

我強烈推薦David Gries，編程科學，它給出了這個主題的系統開發等等。 – Gene

可能的重複 - http://stackoverflow.com/questions/3221577/what-is-a-loop-invariant –

你想要一個循環不變式爲？也許你想證明你的算法是正確的，即是：

linear_search(A,v) = i ⇒ A[i] = v

和

linear_search(A,v) = NIL ⇒ v ∉ A

第一個是容易的。爲了證明第二個，你可以利用你的循環不變P.因爲它，我是真正的= N如果函數返回NIL，你有

linear_search(A,v) = NIL 
⇒ ∀p ∈ {1, 2, ..., n}, A[p] ≠ v 
⇒ v ∉ A

你的候補P用於此目的是有用的，而其他人不是。

此外，你不能只選擇一個循環不變 - 你必須證明它，以證明你的算法是正確的。循環的迭代本質可以通過歸納證明自己，像候選P這樣的不變量很容易以這種方式證明。

來源

2016-11-10 05:14:02

我們如何定義一個循環不變式？

回答

相關問題