Recherche dichotomique : preuve de correction

Soit $L$ une liste triée par ordre croissant et l'algorithme de recherche dichotomique suivant :

def recherche_dicho(L, x):
    g, d = 0, len(L) - 1
    while g <= d:
        m = (g + d) // 2
        if L[m] == x:
            return m
        elif L[m] < x:
            g = m + 1
        else:
            d = m - 1
    return -1

Identifier un invariant de boucle et prouver sa validité.

Identifier un variant de boucle et prouver la terminaison.

En déduire la correction totale de l'algorithme.