如何使用hoare逻辑证明这个二进制搜索算法是正确的？

Question

这是算法:

// Precondition: n > 0

l = -1;
r = n;

while (l+1 != r) {
    m = (l+r)/2;

    // I && m == (l+r)/2

    if (a[m] <= x) {
        l = m;
    } else {
        r = m;
    }
}
// Postcondition: -1 <= l < n

我做了一些研究,并将不变量缩小到了if x is in a[0 .. n-1] then a[l] <= x < a[r].

我不知道如何从那里进步.前提似乎过于宽泛,所以我很难显示出来P -> I.

非常感谢任何帮助.这些是可用于证明算法正确性的逻辑规则:

Answer 1

不变量是

\n\n

-1 <= l and l + 1 < r <= n and a[l] <= x < a[r]\n

\n\n

与隐式约定a[-1] = -\xe2\x88\x9e, a[n] = +\xe2\x88\x9e.

\n\n

然后在if声明中

\n\n

a[l] <= x < a[r] and a[m] <= x implies a[m] <= x < a[r]\n

\n\n

和

\n\n

a[l] <= x < a[r] and x < a[m] implies a[l] <= x < a[m].\n

\n\n

无论哪种情况，赋值都成立a[l] <= x < a[r]。

\n\n

同时，-1 <= l and l + 1 < r <= n确保-1 < m < n，从而使 的评估a[m]成为可能。

\n\n

终止时，l + 1 = r并且由不变量

\n\n

-1 <= l < n and a[l] <= x < a[l + 1].\n

\n