如何在二进制搜索实现中找出循环不变性？

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。首先，所有元素x），所有元素> j且大于x。这是您要维护的不变式。