Wie kann ich beweisen, dass dieser binäre Suchalgorithmus korrekt ist, indem er die Logik verwendet?

Question

Dies ist der Algorithmus:

// 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 

ich einige der Forschung getan haben und verengte die invariante bis if x is in a[0 .. n-1] then a[l] <= x < a[r].

Ich habe keine Ahnung, wie man von dort aber weiterkommt. Die Voraussetzung scheint zu groß zu sein, so dass ich Probleme habe, diese P -> I zu zeigen.

Jede Hilfe wird sehr geschätzt. Dies sind die logischen Regeln, die verwendet werden können, um die Korrektheit des Algorithmus zu beweisen:

Answer 1

Die Invariante ist

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

mit der impliziten Konvention a[-1] = -∞, a[n] = +∞.

Dann in der Anweisung if

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

und

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

In jedem Fall stellt die Zuordnung a[l] <= x < a[r].

Gleichzeitig stellt -1 <= l and l + 1 < r <= n-1 < m < n sicher, so dass die Auswertung von a[m] möglich ist.

Nach Beendigung l + 1 = r und durch den unveränderlichen

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