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

【问题标题】：How to resolve a contradiction using Hoare-Logic in LinearSearch如何在 LinearSearch 中使用 Hoare-Logic 解决矛盾
【发布时间】：2021-03-31 15:02:39
【问题描述】：

我正在尝试使用 Hoare-Logic 来证明以下 LinearSearch，但我得到了矛盾证明 (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

【问题讨论】：

如果你从循环中提前返回，你的不变量是正确的，但如果你使用布尔标志而不是。这个版本的线性搜索的正确不变量应该是((s >= 0 and s < i) implies f[s] != value) or (found and f[i-1] == value)。

标签： linear-search hoare-logic

【解决方案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

【讨论】：