2

我们知道循环变体被定义为在循环的每次迭代之前和之后都为真的语句。但是这个定义是不是太宽松了？让我们看一个具体的例子：线性搜索。

输入：一个由 n 个数字组成的序列 A = (a 1 , a 2 , a 3 , ..., a n ) 和一个值 v

输出：一个索引 i 使得 v = A[i] 或 NIL 如果在 A 中找不到 v

这是我的伪代码：

linear_search(A, v)
1 for i ∈ {1, 2, ..., n}
2     if A[i] = v
3         return i
4 return NIL

因此，一个典型的循环不变量是（因为我们是从左到右搜索）v 不在当前索引的左侧，或者在数学上，P: ∀p ∈ {1, 2, ..., i - 1}, A[p] ≠ v.这显然是正确的，即使在开始时也是如此，因为 p ∈ Ø 是假的，这使 P 为真，记住每一个全称量化的陈述都可以被认为是一个条件陈述。（但非正式地认为它更容易：开始时，v 的左侧什么都没有。）

我们还可以使用限制较少的条件语句。在这种情况下，Q: If A[i] = v, then 1 ≤ i ≤ n.显然，如果找到 v，这是正确的。如果未找到 v，则 A[i] = v 为假，Q 变为真，无论 i 的值如何。如果我们将算法更改为从右到左搜索，Q 也是正确的。

也许我们希望限制更少。使用始终正确的陈述怎么样？R: Either A[i] = v or A[i] ≠ v.R 在循环的每次迭代之前和之后都成立。

哪些语句 P、Q 和 R 可有效用作循环不变量？

4

1 回答 1

0

你想要什么循环不变量？也许您想证明您的算法是正确的，即：

linear_search(A,v) = i ⇒ A[i] = v

和

linear_search(A,v) = NIL ⇒ v ∉ A

第一个很容易。为了证明第二个，你可以利用你的循环不变量 P。因为如果函数返回 NIL，i=n 是真的，你有

linear_search(A,v) = NIL
⇒ ∀p ∈ {1, 2, ..., n}, A[p] ≠ v
⇒ v ∉ A

您的候选人 P 对此很有用，而其他人则不然。

此外，你不能只选择一个循环不变量——你必须证明它才能证明你的算法是正确的。循环的迭代性质使其可以通过归纳来证明，并且像候选 P 这样的不变量很容易以这种方式证明。

于 2016-11-10T05:14:02.900 回答