algorithm - 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ます。

どんな助けでも大歓迎です。これらは、アルゴリズムの正しさを証明するために使用できる論理規則です。