循環(huán)不變式，是指讓每次循環(huán)都成立的邏輯表達(dá)式趾徽，用于證明整個算法的正確性续滋。
它通過證明循環(huán)體三條性質(zhì)的正確性來證明整個算法的正確性。
三條性質(zhì)：
初始化：循環(huán)的第一次迭代前孵奶，循環(huán)不變式為真疲酌。
即初始化的數(shù)據(jù)結(jié)構(gòu)與原始數(shù)據(jù)都是正確的。
保持：如果某次迭代前它為真了袁，那么下次迭代之前它仍為真朗恳。
即每次迭代都保證正確的處理。
終止：在循環(huán)終止時载绿，不變式為我們提供一個有用的性質(zhì)粥诫，該性質(zhì)有助于證明算法是正確的。
即研究在循環(huán)終止時發(fā)生了什么崭庸，并對循環(huán)結(jié)果進(jìn)行判斷怀浆。
在實際寫算法的過程中，我們可以選擇非形式化地通過分析循環(huán)不變式的真假來保證算法的正確性怕享，也可以通過設(shè)置布爾值执赡，并在每次循環(huán)前都利用某種判定規(guī)則得出布爾值并進(jìn)行判斷，來保證算法的正確性函筋。
References:
《算法導(dǎo)論》第3版第10沙合，11頁
圖靈社區(qū)-循環(huán)不變式
