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

【问题标题】：How can I figure out loop invariant in my binary search implementation?如何在我的二进制搜索实现中找出循环不变量？
【发布时间】：2020-01-07 05:40:26
【问题描述】：

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] 或如果 x 不在 arr[0:N-1] 中，则返回 false。
我想知道如何找出正确的循环不变量来证明这个实现是正确的。
我该如何解决这个问题？
非常感谢：D

【问题讨论】：

到目前为止，您对如何证明二分搜索的正确性进行了哪些研究？他的 www 上应该有很多。

标签： algorithm binary-search induction loop-invariant

【解决方案1】：

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

【讨论】：