基本介紹
- 中文名：循環不變式
- 外文名：loop invariant
- 概念：主要用來檢驗算法
- 例子：插入排序
- 學科：數學
- 領域：數學、計算機
介紹,例子,問題,分析,代碼,代碼最佳化,使用特點,
介紹
循環不變式主體是不變式，也就是一種描述規則的表達式。其過程分三個部分：初始，保持，終止。
（1）初始：保證在初始的時候不變式為真。
（2）保持：保證在每次循環開始和結束的時候不變式都為真。
（3）終止：如果程式可以在某種條件下終止，那么在終止的時候，就可以得到自己想要的正確結果。
（1）初始：保證在初始的時候不變式為真。
（2）保持：保證在每次循環開始和結束的時候不變式都為真。
（3）終止：如果程式可以在某種條件下終止，那么在終止的時候，就可以得到自己想要的正確結果。
例子
問題
給出二分查找的實現,函式原形intbsearch(intnum[],intcount,intgoal);num是保存已經從小到大排序好的數字，count是數組元素個數，goal是待查找的數字；若查找成功則返回元素的下標，否則返回-1。
分析
二分查找的原理很簡單：把數組分成三份，中間一份只有一個元素，其他兩份個數基本相同，如果中間的元素等於目標值，就返回它的下標；如果大於，則去前半數組繼續執行二分查找；如果小於，則去後半數組；直到數組沒有元素為止。這是循環不變式的一個計算機算法套用，我們可以按照它的規則來做，我們的不變式就是：當前數組不為空；循環結束條件是：當前數組為空或找到目標元素。
代碼
int bsearch(int num[], int count, int goal) { //檢測初始時不變式的真值 if ( (num == NULL) || (count <=0) ) return -1; //準備循環 int l = 0;//數組左端下標 int r = count -1;//數組右端下標 int m; //數組中間下標 //循環開始 while(r>=l)//r>=l就是不變式，代表數組中有元素 { m = (r+l)/2; //計算中間位置 if (a[m] == goal)//分支1，中間元素是目標元素 return m;//則返回 else if(a[m] > goal) //分支2，中間元素大於目標元素 r = m - 1;//把數組右端標誌放到m的前面一個元素 else//分支3，中間元素小於目標元素 l = m +1;//把數組左端標誌放到m的後面一個元素 } //運行到這裡表示沒有找到目標元素 return -1; } 代碼最佳化
int bsearch(int num[], int count, int goal) { int l = 0; int r = count -1; int m = (r+l)/2; for(num != NULL; r>=l; m = l+r/2) { if (a[m] > goal) r = m - 1; else if (a[m] < goal) l = m +1; else return m; } return -1; } 