Pages

2012年3月3日 星期六

[演算法] 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 能夠展示整體演算法的正確性。

沒有留言:

張貼留言