【发布时间】：2023-03-11 01:54:01
【问题描述】：
我正在尝试证明以下 RandomSeach-Algorithm 并找出循环的不变量。
由于函数 randomIndex(..) 创建了一个随机数，我不能使用类似的不变量
???? ≥ 0 ∧ ???? < ???? − 1 ⇒ ????[????] ≠ ????????????????e
。也就是说，所有在 0 到 i-1 之间的元素，其中 i 是当前被检查元素的索引，都不是被搜索到的元素。
所以我想我定义了一个假设序列r，它包含已经与搜索值进行比较或将与搜索值进行比较的所有元素。这就是为什么它只是一个假设的序列，因为在真正比较之前，我实际上不知道将要与搜索值进行比较的元素。
这意味着它适用于r.lenght() ≤ runs ，并且在找到搜索元素的情况下
(r[r.lenght()-1] = value) ↔ (r[currentRun] = value).
然后我可以定义一个不变量，如：
???? ≥ 0 ∧ ???? < currentRun ⇒ r[????] ≠ ????????????????e
我可以这样做吗，因为序列 r 不是真实的？感觉不对。有人对不变量有不同的想法吗？
程序：
public boolean RandomSearch (int value, int[] f, int runs) {
int currentRun = 0;
boolean found = false;
while (currentRun < runs || !found) {
int x = randomIndex(0, n-1)
if (value == f[x]) {
found = true;
}
currentRun = currentRun + 1;
}//end while
return found;
}//end RandomSearch
【问题讨论】：
标签： loop-invariant hoare-logic