问题是:
构造基于二分搜索的迭代算法,对于给定的排序数组和数字,找到数组中最小元素的索引,该索引小于或等于给定数字 . 使用循环不变量技术证明算法的正确性 .
实现的语言是自由选择,所以我用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 回答
你可以更简单一点:
现在什么是循环不变量?在每次循环运行中,
r
右侧的所有值都将大于目标,l
左侧的所有值都小于或等于 . 一旦l
和r
平等,......最终测试处理角落情况,即矢量中没有小于目标值的值 .
编辑:循环不变(如所要求的):
要么:
如果在循环之前检查
target < vec[0]
,那么您可以:(注意包含
l
,仍然没有l == 0
) .