如何在 LinearSearch 中使用 Hoare-Logic 解决矛盾

Question

我正在尝试使用 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

矛盾是：证明

(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

Answer 1

谢谢@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

如何在 LinearSearch 中使用 Hoare-Logic 解决矛盾

How to resolve a contradiction using Hoare-Logic in LinearSearch

linear-search

hoare-logic