[演算法] Loop Invariants

        Loop Invariant 是證明某個不變的條件(稱為Invariant Condition)，這個條件在程式進入迴圈前跟進入迴圈後，此條件仍不變。

通常以while迴圈為例子。
假如有一個while迴圈如下：

while( A )
{
        //Body..
}

        那麼假設一個 Invariant 條件叫做 X ，這個X條件在while檢查A條件時都維持原狀，一進入Body 時可能改變X條件，但一執行完 Body 後 X 又恢復原貌，這種條件就是一個典型的 Invariant Condition。

• 證明Loop Invariant需要三個步驟：
  1.   Initialization：描述 Invariant Condition 在迴圈執行第一個 iteration前，就成立。
  2.   Maintenance：描述 Invariant Condition 在迴圈的任一iteration執行前跟執行後都維持成立。
  3.   Termination：迴圈執行結束後，Invariant Condition 能夠展示整體演算法的正確性。