《算法基礎：打開算法之門》一2.3 循環不變式

本節書摘來自華章出版社《算法基礎：打開算法之門》一書中的第2章，第2.3節，作者 ［美］托馬斯 h 科爾曼（thomas h cormen），更多章節内容可以通路雲栖社群“華章計算機”公衆号檢視

對于線性查找的3個算法，我們能很容易地看到每個算法均能生成正确的結果。但是有時候生成正确的結果看起來有點難。這涉及一系列技術，在這裡不能一一講解。

證明正确性的一個常用方法是使用循環不變式證明：即證明循環的每次疊代之前循環不變式為真。循環不變式能夠幫助我們證明正确性，關于循環不變式，我們必須證明以下3條性質。

初始化：循環的第一次疊代之前，它為真。

保持：如果循環的每次疊代之前它為真，那麼下次疊代之前它仍為真。

終止：循環終止時，當它确實終止時，伴随循環終止的原因，循環不變式為我們提供了一個有用的性質。以betterlinearsearch算法為例，以下是一個循環不變式：

在第1步疊代開始時，如果數組a中存在x，那麼x一定在a［i］～a［n］的子數組（數組的一段連續部分）中。我們甚至不需要循環不變式來證明如果程式傳回了一個索引而非notfound，則被傳回的索引是正确的：在第1a步中該程式能傳回索引i的唯一方式是因為x等于a［i］。下面，我們使用循環不變式來證明如果程式是在第2步中傳回notfound，那麼數組中一定不包含x。初始化：初始時，i=1，是以循環不變式的子數組是a［1］～a［n］，此時代表整個數組。保持：假定目前循環變量是i，在疊代開始時，如果數組a中包含x，那麼它一定在從a［i］到a［n］的子數組中。如果執行這次循環疊代而沒有傳回值，我們能得出a［i］≠x，是以能确定地說如果x在數組a内，那麼它一定出現在a［i+1］～a［n］的子數組内。因為i在下次疊代之前會自增1，21是以循環不變式在下次疊代之前仍為真。終止：循環一定會終止，或者因為程式會在第1a步傳回，或者由于i>n。我們已經對程式因在第1a步傳回而導緻循環終止的情況進行了驗證。為了處理因i>n而導緻循環終止的情況，我們依據循環不變式的等價性來證明。命題“如果a那麼b”的逆否命題是“如果非b那麼非a”。一個命題為真當且僅當與它等價的命題也為真。該循環不變式的等價命題為“如果x沒有出現在a［i］～a［n］的子數組中，那麼數組a中就不存在x”。現在，當i>n時，a［i］～a［n］這個子數組為空。是以這個子數組中不可能包含x。是以，根據循環不變式的等價式，x不可能出現在數組a的任意位置上，是以第2步中傳回notfound是恰當的。這一系列的推理僅僅是為了說明這麼一個簡單的循環？每次寫一個循環時，我們都必須添加上述證明嗎？我不會，但是針對每一個簡單的循環，依舊有幾個計算機科學家堅持這樣嚴格的推理。在實際程式設計時，我發現在我寫一個循環的大部分時間裡，我會在頭腦裡想出循環不變式。它可能深藏在我的頭腦中以至于我甚至沒有意識到我的大腦裡會存在該循環不變式，但是如果要求我必須陳述該循環不變式，我能夠完整地将其表述下來。雖然我們中的大多數人認為循環不變式對于了解像betterlinearsearch這樣的簡單循環沒有必要，但是我們想要了解複雜的循環能夠執行正确的操作時使用循環不變式會很友善。