，在算法

Question

k :=0 
for i ←1 to n 
    c←a[i] 
      k←k+1 

這並沒有改變的事情是要知道元素

Answer 1

技術上的數量algorithim，是的，k <= i是不變的，但不是一個非常有用的一個。我們使用不變量的原因是我們可以使用它們來證明循環後的狀態。隨着你的不變，你可以證明k <= n後循環。雖然非常真實，但這並不能真正幫助你試圖證明循環的真正作用。

那麼什麼樣的不變量會有用？我們想要證明k等於a和b中的元素數量。由於我們正在循環遍歷a中的元素，因此一個不錯的選擇是：k等於也在b中的元素數量達到a[i]。

---

我們現在需要證明這個不變量成立。我會保持一點粗略，所以它仍然由你來形式化。

最初，我們需要證明k = 0是a[1]之前的元素的數量，它們也是b。沒有這樣的元素，所以k = 0是正確的。

現在，考慮到ki是的元素數也是b，我們需要證明該不變量對於i+1成立。有兩種選擇：或者a[i+1]在b中，或者不是。

• 如果ba[i+1]，然後元件高達a[i + 1]是在b的數量比元件的可達a[i]是在b的數量大一個。使用我們的不變量，我們因此需要顯示ki+1 = ki + 1。
• 如果a[i+1]不在b，然後元件高達a[i + 1]是在b的數目等於元素多達a[i]是在b的數量。使用我們的不變量，我們因此需要顯示ki+1 = ki。

我會留給你來證明這些。