algorithm - 如何在我的二进制搜索实现中找出循环不变量？

Question

bool binsearch(int x) {
    int i = 0, j = N;
    while(i < j) {
        int m = (i+j)/2;
        if(arr[m] <= x) {
            if(arr[m] == x)
                return true;
            i = m+1;
        }
        else {
            j = m;
        }
    }
    return false;
}

这是我的二分搜索实现，如果 x 在 arr[0:N-1] 中则返回 true，如果 x 不在 arr[0:N-1] 中则返回 false。
而且我想知道如何找出正确的循环不变量来证明这个实现是正确的。
我怎么解决这个问题？
非常感谢 :D

Answer 1

想想在你的循环中保持状态的变量。在您的情况下，它们是变量 i 和 j。您从所有元素 < i 且小于您要搜索的值 ( x) 以及所有元素 > j 且大于的事实开始x。这是您要维护的不变量。