介紹
循環不變式主體是不變式，也就是一種描述規則的表達式。其過程分三個部分：初始，保持，終止。
（1）初始：保證在初始的時候不變式為真。
（2）保持：保證在每次循環開始和結束的時候不變式都為真。
（3）終止：如果程式可以在某種條件下終止，那么在終止的時候，就可以得到自己想要的正確結果。
例子
問題
給出二分查找的實現,函式原形intbsearch(intnum[],intcount,intgoal);num是保存已經從小到大排序好的數字，count是數組元素個數，goal是待查找的數字；若查找成功則返回元素的下標，否則返回-1。
分析
二分查找的原理很簡單：把數組分成三份，中間一份只有一個元素，其他兩份個數基本相同，如果中間的元素等於目標值，就返回它的下標；如果大於，則去前半數組繼續執行二分查找；如果小於，則去後半數組；直到數組沒有元素為止。這是循環不變式的一個計算機算法套用，我們可以按照它的規則來做，我們的不變式就是：當前數組不為空；循環結束條件是：當前數組為空或找到目標元素。
代碼
代碼最佳化
使用特點
1、在循環，疊代，遞歸等用上次結果作為下次初始值的累計過程都可以準確無誤的使用。
2、在循環不變式三要素，初始，保持，結束。初始一定要正確，循環的時候也要保證不變式為真，循環一定要可以結束才能得到正確結果。其中後兩條比較容易疏漏，解題時要慎而又慎嚴謹對待循環中不變式和結束條件。
3、可以把三要素再進行一次轉化，使之更適合電腦程式：一次循環開始時候不變式為真，一次循環完畢時為真，總循環可以結束，結果必定正確。
