Annoter et prouver totalement

Prouver et analyser : la boîte à outils formalisée · niveau 1 (application)

Énoncé

Annoter et prouver totalement la fonction suivante :

def somme_impairs(n: int) -> int:
    s, k = 0, 0
    while k < n:
        s = s + 2 * k + 1
        k = k + 1
    return s

Précondition : $n \geq 0$ .
Postcondition : Renvoie $n^{2}$ .
Invariant $I$ : $s = k^{2}$ .
Initialisation : Avant la boucle, $s = 0$ et $k = 0$ . On a bien $0 = 0^{2}$ , l'invariant est initialisé.
Conservation : Supposons $I$ vrai et $k < n$ au début d'un tour. Après le tour, la nouvelle valeur $s^{'}$ vaut $s + 2 k + 1 = k^{2} + 2 k + 1 = (k + 1)^{2}$ et la nouvelle valeur $k^{'}$ vaut $k + 1$ . On a bien $s^{'} = (k^{'})^{2}$ . L'invariant est conservé.
Conclusion : En sortie de boucle, $k \geq n$ (par négation de la condition) et $k \leq n$ (puisque $k$ commence à 0 et progresse de 1 à chaque étape). Donc $k = n$ . L'invariant donne alors $s = n^{2}$ . La postcondition est démontrée.
Variant $v$ : $v = n - k$ . C'est un entier. Tant que la boucle tourne, $k < n ⟹ v > 0$ . À chaque tour, $k$ augmente de 1 donc $v$ diminue strictement de 1. La terminaison est prouvée. L'algorithme est totalement correct et calcule le carré de $n$ par somme d'impairs.