Forum per gli studenti

Salve a tutti, sto provando a dimostrare la correttezza della versione iterativa della ricerca binaria, però non sono convinto di quello che ho scritto per cui volevo avere un confronto.

In primis lo pseudocodice:
Algoritmo binarySearchIt(A, x)
Input: {(A, x) : A = array ordinato di n interi distinti, x intero}
Output: {i intero positivo dove i = indice dove si trova x oppure -1}
low <- 0
high <- A.length - 1
while (low <= high) do {
    mid <- (low + high) / 2
    if (x == A[mid]) then {
        return mid
    } else if (x < A[mid]) then {
        high <- mid - 1
    } else if (x > A[mid]) then {
        low <- mid + 1
    }
}
return -1

INVARIANTE: alla fine di una generica iterazione, low e high rimangono sempre rispettivamente il lower bound e l'upper bound della sottosequenza dove potrebbe trovarsi x

(Ho pensato ad altri invarianti come mid, che è l'indice che sta sempre al centro della sequenza, oppure che alla fine dell'iterazione tutti gli A[mid] precedenti non corrispondono ad x, ma non sono riuscito a giustificarli per cui ho lasciato solo l'invariante sopra)

Dimostrazione correttezza
1) all'inizio del ciclo la sottosequenza S[low : high] corrisponde alla sequenza di input perché low = 0 e high = n - 1.
2) supponiamo che alla fine della generica iterazione i valga l'invariante.
- se x = A[mid] allora si restituisce mid terminando il ciclo (si è trovato x)
- se x < A[mid] si aggiorna l'upper bound a mid-1 (x non si può trovare dopo A[mid])
- altrimenti si aggiorna il lower bound a mid+1 (x non si può trovare prima di A[mid])
low e high rimangono sempre rispettivamente il lower bound e l'upper bound della sottosequenza dove potrebbe trovarsi x
3) alla fine del ciclo, se si è trovato x si capisce subito che l'invariante è valido. Altrimenti alla fine del ciclo avremo low > high. Se il lower bound è maggiore dell'upper bound significa che non è stato possibile trovare x nella sequenza. L'invariante è comunque rispettato.

Grazie mille in anticipo dell'aiuto.