证明二进制搜索问题(迭代)[暂停]

问题是:

构造基于二分搜索的迭代算法,对于给定的排序数组和数字,找到数组中最小元素的索引,该索引小于或等于给定数字 . 使用循环不变量技术证明算法的正确性 .

实现的语言是自由选择,所以我用C . 这是我构建的算法:

int FindLessEqual(vector<int>&vec, int target){
    int n = vec.size();

    int l = 0;
    int r = n - 1;
    while(l<=r){
        int mid = (l+r)/2;

        if(vec[mid] > target){
            r = mid - 1;
        }else{
            if (mid == n - 1 || vec[mid+1] > target) return mid;
            l = mid + 1;
        }

    }
    return -1;
}

如您所见,我的想法很简单:

使用标准二进制搜索方法(如问题所示) . 如果当前元素大于目标元素,则移动到左子数组 . 如果当前元素小于或等于目标,则有几个选项:

  • 情况1:当前元素是整个数组的最后一个元素,这意味着这是我们正在寻找的元素 .

  • 情况2:当前元素之后的元素大于目标,使得此元素在数组中最远,以满足条件,这意味着这是我们正在寻找的元素 .

  • 情况3:这既不是最后一个元素,也不是小于或等于目标的最远元素,继续在右子数组中搜索 .

但是,由于我使用的“案例分析”相当复杂,我发现很难证明这种算法的正确性 . 我已经搜索了一般二进制搜索的证明(所以我可以尝试从那里得到一些线索)但是我发现的所有证据都集中在递归实现上,这并没有真正帮助我 .

那么,这里有什么想法吗?

谢谢 .

回答(1)

2 years ago

你可以更简单一点:

int l = 0;
int r = vec.size() - 1;
while(l < r) // as long as bounds are not equal!
{
    int mid = (l + r + 1) / 2; // +1: round mid up!
                               // this prevents l being assigned mid again and again
                               // if r - l == 1, ending up in an endless loop

    if(vec[mid] > target)
    {
        r = mid - 1; // vec[mid] is out of desired range -> exclude it!
                     // additionally, the - 1 prevents an endless loop
                     // again (avoids re-assigning mid to r again and again)
    }
    else
    {
        l = mid;
    }
}
return l == 0 && vec[0] > target ? -1 : l;

现在什么是循环不变量?在每次循环运行中, r 右侧的所有值都将大于目标, l 左侧的所有值都小于或等于 . 一旦 lr 平等,......

最终测试处理角落情况,即矢量中没有小于目标值的值 .

编辑:循环不变(如所要求的):

∀ n ∈ [0 ... l):          vec[n] <= target
∀ n ∈ (r ... vec.size()): vec[n] > target

要么:

∀ n ∈ [0 ... l]:          vec[n] <= target | l == 0
∀ n ∈ (r ... vec.size()): vec[n] > target

如果在循环之前检查 target < vec[0] ,那么您可以:

∀ n ∈ [0 ... l]:          vec[n] <= target
∀ n ∈ (r ... vec.size()): vec[n] > target

(注意包含 l ,仍然没有 l == 0 ) .