Récurrence et correction de programme

Considérons l'algorithme suivant qui calcule $x^n$ :

def puissance(x, n):
    r = 1
    b = x
    e = n
    while e > 0:
        if e % 2 == 1:
            r = r * b
        b = b * b
        e = e // 2
    return r

Identifier un invariant de boucle et le démontrer.

En déduire la correction de l'algorithme.

Montrer que l'algorithme termine et donner sa complexité.