0

我正在尝试使用 Hoare-Logic 来证明以下 LinearSearch，但我得到了矛盾证明 (1) => (2)。我相信我的不变量应该是不同的。

目前我使用 {s ≥ 0 & s < i → f[s] ≠ value} 作为不变量。这意味着从 0 到 i-1 的所有元素都已经与搜索的值进行了比较，因此从 f[0] 到 f[i-1] 的所有元素都不等于搜索的值。

我开始将规则从算法的底部应用到顶部。

当我试图证明（1）隐含（2）时，矛盾就出现了。因为它在 (1) 中适用于 {f[i] = value} 并且对于所有 s < i 它适用于 f[s] ≠ value。到目前为止这是正确的。

但在 (2) 中，它适用于所有 s <i+1，即 f[s] ≠ 值，因此 f[i] ≠ 值。

矛盾是：证明

(1) → (2)

我必须证明

f[i] = value → f[i] ≠ value

这不是真的。

这就是为什么我认为我需要改变我的不变量。但我不知道怎么办？

public boolean LinearSearch (int value, int[] f) {
//Precondition = {f.length() > 0}

int i = 0;

boolean found = false;

//{s ≥ 0 & s < i → f[s] ≠ value}
while (i < f.length()-1 || !found) {
//{(s ≥ 0 & s < i → f[s] ≠ value) & (i < f.length()-1 || found = false)}

    if (value == f[i]) {
(1) //{(s ≥ 0 & s < i → f[s] ≠ value) & (i < f.length()-1 || found = false) & (value = f[i])} 

(2) //{(s ≥ 0 & s < i+1 → f[s] ≠ value)}
    ↕
    //{(s ≥ 0 & s < i+1 → f[s] ≠ value) & true = true}
    found = true;

    //{(s ≥ 0 & s < i+1 → f[s] ≠ value) & found = found} 
    }

    //{(s ≥ 0 & s < i+1 → f[s] ≠ value) & found = found} 
    ↕
    //{s ≥ 0 & s < i+1 → f[s] ≠ value}
    i = i + 1;

//{s ≥ 0 & s < i → f[s] ≠ value}
}//end while
//{(s ≥ 0 & s < i → f[s] ≠ value) & !(i < f.length()-1 || found = false)}
↓
//Postcondition = {i = f.length()-1 | f[i] = value}
return found;
}//end LinearSearch
4

1 回答 1

0

谢谢@aioobe 的回答。

我试过了

{s ≥ 0 & s < i-1 → f[s] ≠ value}

并得到以下证明。我认为它有效。如果您看到错误，请告诉我。也许它可以帮助其他需要使用 Hoare-Logic 的人。

public boolean LinearSearch (int value, int[] f) {
//Precondition = {f.length() > 0}
↓
//{true & true}
↕
//{true & false = false}
↕
//{false → f[s] ≠ value & false = false}
↕
//{s ≥ 0 & s < 0-1 → f[s] ≠ value & false = false}
int i = 0;
//{s ≥ 0 & s < i-1 → f[s] ≠ value & false = false}
boolean found = false;
//{s ≥ 0 & s < i-1 → f[s] ≠ value & found = found}
↕
//{s ≥ 0 & s < i-1 → f[s] ≠ value}
while (i < f.length() & !found) {
//{(s ≥ 0 & s < i-1 → f[s] ≠ value) & (i < f.length() & found = false)}

    if (value == f[i]) {
    //{(s ≥ 0 & s < i-1 → f[s] ≠ value) & (i < f.length() & found = false) & (value = f[i])} 
        ↓
        //{(s ≥ 0 & s < i → f[s] ≠ value)}
        ↕
        //{(s ≥ 0 & s < i-1+1 → f[s] ≠ value) & true = true}
        found = true;

        //{(s ≥ 0 & s < i-1+1 → f[s] ≠ value) & found = found} 
        }

    //{(s ≥ 0 & s < i-1+1 → f[s] ≠ value) & found = found} 
    ↕
    //{s ≥ 0 & s < i-1+1 → f[s] ≠ value}
    i = i + 1;

    //{s ≥ 0 & s < i-1 → f[s] ≠ value}
    }//end while
//{(s ≥ 0 & s < i-1 → f[s] ≠ value) & !(i < f.length() & found = false)}
↓
//Postcondition = {i = f.length() | found = true}
return found;
}//end LinearSearch
于 2020-12-22T18:32:57.387 回答