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

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

我正在尝试使用 hoare-logic 证明以下线性搜索，但我得到了一个矛盾证明 (1) => (2)。我相信我的不变量应该是不同的。

目前我使用 {s ≥ 0 & s

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

当我试图证明 (1) 蕴涵 (2) 时，矛盾就出现了。因为它适用于 (1) {f[i] = value} 并且对于所有 s

但在 (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

解决方法

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