使用循环不变量证明算法是正确的答案

【问题标题】：Proving that an algorithm is correct using a loop invariant使用循环不变量证明算法是正确的
【发布时间】：2015-11-11 17:00:47
【问题描述】：

来自 Cormen 等人的算法简介。（第 3 版），我正在做练习 2.1-3。基本上，给定一个长度为n 的向量A 和一个值v，该算法输出一个索引i（索引从1 开始，而不是0）使得v = A[i] 或@ 987654329@ 如果这样的索引不存在。

我的伪代码如下：

for j = 1 to length(A):
    value = A[j]
    if v == value:
        return j
return 'NIL'

如何使用循环不变量来证明这是正确的？我不知道如何将他们关于插入排序算法的循环不变量的讨论扩展到这里的算法（称为线性搜索算法）。

我想，当j = 1 时，你有一个长度为1 的（子）向量，它的分量要么是v，要么不是v。

当您有一个长度为j = k 的子向量时，如果我们假设该算法有效，那么对于j = k+1，这是微不足道的（我认为？）。

我显然不明白这种证明算法正确的方法，虽然我非常熟悉数学归纳法，但我不知道如何解决这个问题。

【问题讨论】：

OP：像“当我在循环中时，A[j] 之前的任何元素都不等于 v”这样的属性可以帮助你证明吗？
分配中是否使用了Hoare logic这样的形式？
我在这里使用的不变量是“在循环的顶部，我们知道 A[1], ..., A[j-1] 都不等于 v。”当 j=1 时，这是微不足道的，并且也很容易显示归纳情况（假设它适用于 j=k，然后用它来证明它适用于 j=k+1）。如果我们到达return 'NIL'，那么它一定是在上一时刻我们处于循环的顶部，j=length(A)+1，这与不变量一起意味着 v 不在 A 中。
这表明如果算法返回 NIL 那么这样做是正确的。您还需要证明，如果它返回一些非 NIL 值，那么它也是一个正确答案（这很容易，因为只有一个 return 语句可以用于产生这样的返回值，并且紧接在前面的 if 保证它）。为了彻底，您还需要表明它终止了（尽管这在这里很明显）。

标签： algorithm

【解决方案1】：

循环不变量是：A[i] != v 对所有 1 <= i < j

循环不变量始终在每次迭代中保持不变。否则假设存在i < j 使得A[i] = v。该算法将在到达jth-iteration 之前返回i。

循环不变量有助于证明正确性，因为在终止时有两种可能的情况。 (1) j <= length(A)，其中循环不变量和 if 语句表明 A[j] = v 并且算法正确返回 j；或 (2) j > length(A)，其中循环不变量意味着对于所有 i <= length(A)、A[i] != v，算法正确返回 NIL。

【讨论】：