このバイナリ検索アルゴリズムがホア論理を使用して正しいことをどのように証明できますか？

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

不変が暗黙の慣習a[-1] = -∞、a[n] = +∞と

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

です。

そしていずれの場合ifステートメント

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

と

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

において、割り当てはa[l] <= x < a[r]を確立します。

同時に、-1 <= l and l + 1 < r <= nは-1 < m < nを保証するので、a[m]の評価が可能です。あなたのケースで、それは `！（L + 1！= Rであるので、終了した場合

、` while`ループのl + 1 = rと不変

によって

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