如何证明以下算法的正确性？答案

【问题标题】：How can I prove the correctness of the following algorithm?如何证明以下算法的正确性？
【发布时间】：2013-03-11 15:59:02
【问题描述】：

考虑以下算法 min，它以列表 x,y 作为参数并返回 x 和 y 的并集中的第 z 个最小元素。前置条件：X 和 Y 是 int 的升序排序列表，并且它们是不相交的。

注意它的伪代码，所以索引从 1 而不是 0 开始。

Min(x,y,z):
    if z = 1:
        return(min(x[1]; y[1]))
    if z = 2:
        if x[1] < y[1]:
            return(min(x[2],y[1]))
        else:
            return(min(x[1], y[2]))

q = Ceiling(z/2) //round up z/2

if x[q] < y[z-q + 1]:
    return(Min(x[q:z], y[1:(z - q + 1)], (z-q +1)))
else:
    return(Min(x[1:q], B[(z -q + 1):z], q))

我可以证明它终止了，因为 z 不断减少 2 并且最终会达到基本情况之一，但我无法证明部分正确性。

【问题讨论】：

嗨，我认为这更适合计算机科学，对吧？
您能否更详细地说明该算法应该做什么？我了解到您想要x 和y 的元素中的第k 个最小元素，即Mix([1,2], [3, 4], 1) = 1（最小元素）Mix([1, 2], [3, 4], 2) = 2（第二小元素）等。对吗？如果是这样，我认为上述算法做的不对。甚至没有任何递归。
当然，如果没有递归，终止是微不足道的。如果你有递归，你的论点将不能保证终止（假设你真的是指整数，而不是自然数），因为减少负整数可以（理论上）永远持续下去而不会达到基本情况。

标签： proof proof-of-correctness

【解决方案1】：

您的代码不正确。

考虑以下输入：

x = [0,1]
y = [2]
z = 3

然后您将获得q = 2，并在随后的if 子句中访问y[z-q+1]，即y[2]。这是数组边界违规。

【讨论】：