吉寶力--K.I.S.S.(Keep It Simple Software)
阿新 • • 發佈：2019-01-07
這個概念主要用來檢驗演算法的正確性。
原文如下：We use loop invariants to help us understand why an algorithm is correct. We must show three things about a loop invariant:
- Initialization: It is true prior to the first iteration of the loop.
- Maintenance: If it is true before an iteration of the loop, it remains true before the next iteration.
- Termination: When the loop terminates, the invariant gives us a useful property that helps show that the algorithm is correct.
1. 初始化（迴圈第一次迭代之前）的時候，A [1 ‥ j -1]的“有序性”是成立的；
2. 在迴圈的每次迭代過程中，A[1 ‥ j -1]的“有序性”仍然保持；
3. 迴圈結束的時候，A[1 ‥ j -1]的“有序性”仍然成立。
另外，我個人認為應該翻譯為“迴圈不變性”，“迴圈不變式”是一種誤導。因為這是一種性質，一種屬性（property），而不是表示式。
以上引自 http://bbs.chinaunix.net/thread-750480-1-1.html
單就這個插入排序來說的話，這個解釋確實不錯，其實就是對原文的翻譯分析。但是對這個loop invariant的作用還是覺得模模糊糊的，書中也說是類似歸納法的一個證明方法，只是最後一步不同而已。
一直就很頭痛有關證明的東西，一些數學公式什麼的，很頭大，這是另一個關於loop invariant的introduction：