证明二进制搜索问题（迭代）[暂停]

问题是：

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

实现的语言是自由选择，所以我用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 左侧的所有值都小于或等于 . 一旦 l 和 r 平等，......

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

编辑：循环不变（如所要求的）：

∀ 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 ） .

证明二进制搜索问题（迭代）[暂停]

回答(1)

2 years ago

相似问题

Tags

友情链接

帮助