[科普中国]-循环不变式

循环不变式（loop invariants）不只是一种计算机科学的思想，准确地说是一种数学思想。在数学上阐述了通过循环（迭代、递归）去计算一个累计的目标值的正确性，属于基础数学的范畴，而且在计算机上也应用广泛。1

介绍循环不变式主体是不变式，也就是一种描述规则的表达式。其过程分三个部分：初始，保持，终止。2
（1）初始：保证在初始的时候不变式为真。3

（2）保持：保证在每次循环开始和结束的时候不变式都为真。3

（3）终止：如果程序可以在某种条件下终止，那么在终止的时候，就可以得到自己想要的正确结果。3

例子问题给出二分查找的实现,函数原形intbsearch(intnum[],intcount,intgoal);num是保存已经从小到大排序好的数字，count是数组元素个数，goal是待查找的数字；若查找成功则返回元素的下标，否则返回-1。1

分析二分查找的原理很简单：把数组分成三份，中间一份只有一个元素，其他两份个数基本相同，如果中间的元素等于目标值，就返回它的下标；如果大于，则去前半数组继续执行二分查找；如果小于，则去后半数组；直到数组没有元素为止。1这是循环不变式的一个计算机算法应用，我们可以按照它的规则来做，我们的不变式就是：当前数组不为空；循环结束条件是：当前数组为空或找到目标元素。2

代码int bsearch(int num[], int count, int goal) { //检测初始时不变式的真值 if ( (num == NULL) || (count =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]