Écrire une fonction racine entiere(n) renvoyant ⌊√n⌋ sans utiliser…

def racine_entiere(n):
    """Partie entiere de la racine carree de n.

    Precondition  : n est un entier >= 0.
    Postcondition : r*r <= n < (r+1)*(r+1).
    """
    assert n >= 0, "n doit etre positif ou nul"
    r = 0
    while (r + 1) * (r + 1) <= n:
        r = r + 1
    assert r * r <= n < (r + 1) * (r + 1)
    return r

Pourquoi la postcondition est la bonne. Elle ne mentionne ni racine carrée ni flottant : elle est écrite entièrement avec des entiers et des multiplications. C'est ce qui la rend vérifiable sans risque — l'avertissement du cours sur les postconditions flottantes ne s'applique pas ici. Et elle caractérise $r$ de façon unique : deux entiers distincts ne peuvent pas vérifier tous deux cet encadrement.

Invariant et terminaison. L'invariant est r * r <= n : il est vrai au départ ($0\le n$) et le corps ne s'exécute que si $(r+1{)}^2\le n$, ce qui le préserve. Le variant est $n-r^2$, entier positif qui décroît strictement : la boucle s'arrête.

La vérification.

for n in range(0, 10001):
    r = racine_entiere(n)
    assert r * r <= n < (r + 1) * (r + 1)

Les $10001$ cas passent. Contrôles : $\text{racine\_entiere}(0)=0$, $\text{racine\_entiere}(2)=1$, et $\text{racine\_entiere}(2026)=45$ puisque $45^2=2025\le 2026<2116=46^2$.

Pourquoi éviter math.sqrt : sur de grands entiers, la racine flottante peut tomber juste en dessous d'un entier exact, et int(math.sqrt(n)) rend alors $r-1$. La version entière n'a pas ce défaut, parce qu'elle ne quitte jamais $\mathbb{N}$.