Hoare-Logic 在 RandomSearch 上的不变量
Invariant for Hoare-Logic on RandomSearch
我正在尝试证明以下 RandomSeach 算法并找出循环的不变量。
由于函数 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
好的,
我使用以下不变量
currentRun <= runs & f.length > 0
我可以证明算法:)
我正在尝试证明以下 RandomSeach 算法并找出循环的不变量。
由于函数 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
好的,
我使用以下不变量
currentRun <= runs & f.length > 0
我可以证明算法:)