Correction et Terminaison

def f(n):
    """Postcondition : renvoie n!"""
    while True:                # ne termine JAMAIS
        pass
    return 0
# partiellement correcte (vacuement), mais pas totalement correcte

def g(n):
    """Postcondition : renvoie n!"""
    return 0                   # termine toujours
# termine, mais n'est pas partiellement correcte pour n >= 2

def somme(t):
    s, i = 0, 0
    while i < len(t):
        s += t[i]; i += 1
    return s
# variant : len(t) - i.  Entier >= 0 tant que i < len(t), decroit de 1 par tour.

def division(a, b):
    q, r = 0, a
    while r >= b:
        r -= b; q += 1
    return q, r
# variant : r.  Entier >= 0 (car r >= b > 0 a l'entree), decroit de b >= 1.

def euclide(a, b):
    while b != 0:
        a, b = b, a % b
    return a
# variant : b.  Entier >= 0, et a % b < b : decroissance stricte.

def maximum(t):
    """Precondition  : t est une liste non vide.
    Postcondition : renvoie max(t)."""
    m = t[0]
    i = 1
    while i < len(t):
        if t[i] > m:
            m = t[i]
        i += 1
    return m

Terminaison. Variant \(V = \mathrm{len}(t) - i\). C'est un entier, positif tant que \(i < \mathrm{len}(t)\), et il decroit de 1 a chaque tour. La boucle effectue donc exactement \(\mathrm{len}(t) - 1\) iterations.

Invariant. \(P_i\) : « \(m = \max(t[0], \dots, t[i-1])\) ».

• Initialisation : \(i = 1\) et \(m = t[0] = \max(t[0])\). \(P_1\) est vraie.
• Conservation : supposons \(P_i\) vraie, c'est-a-dire \(m = \max(t[0..i-1])\). Apres le corps de boucle, la nouvelle valeur de \(m\) est \(\max(m, t[i]) = \max(\max(t[0..i-1]), t[i]) = \max(t[0..i])\), et \(i\) devient \(i+1\) : \(P_{i+1}\) est vraie.
• Exploitation : a la sortie, \(i = \mathrm{len}(t)\) et \(P_i\) donne \(m = \max(t[0..\mathrm{len}(t)-1]) = \max(t)\). C'est la postcondition.

L'algorithme est donc totalement correct, en \(\Theta(n)\).

def puissance(x, n):
    """Precondition  : n entier >= 0.
    Postcondition : renvoie x**n."""
    resultat, base, k = 1, x, n
    while k > 0:
        if k % 2 == 1:
            resultat *= base
        base *= base
        k //= 2
    return resultat

Terminaison. Variant \(V = k\). Entier positif, et \(k \ge 1\) implique \(\lfloor k/2 \rfloor \le k/2 < k\) : decroissance stricte.

Invariant. \(P\) : « \(\texttt{resultat} \times \texttt{base}^{k} = x^n\) ».

• Initialisation : \(1 \times x^n = x^n\). Vrai.
• Conservation : notons \(r, b, k\) les valeurs avant le tour et \(r', b', k'\) apres.
  • Si \(k\) est pair : \(r' = r\), \(b' = b^2\), \(k' = k/2\), d'ou \(r'b'^{k'} = r\,(b^2)^{k/2} = r\,b^{k} = x^n\).
  • Si \(k\) est impair : \(r' = rb\), \(b' = b^2\), \(k' = (k-1)/2\), d'ou \(r'b'^{k'} = rb\,(b^2)^{(k-1)/2} = r\,b^{1 + k - 1} = r\,b^k = x^n\).
  L'invariant est preserve dans les deux cas.
• Exploitation : a la sortie \(k = 0\), donc \(P\) donne \(\texttt{resultat} \times \texttt{base}^0 = \texttt{resultat} = x^n\).

Complexite. Le variant est divise par au moins 2 a chaque tour, donc le nombre d'iterations est \(\lfloor\log_2 n\rfloor + 1 = \Theta(\log n)\).

def tri_insertion(t):
    """Postcondition : t est triee et est une permutation de sa valeur initiale."""
    for i in range(1, len(t)):
        x, j = t[i], i - 1
        while j >= 0 and t[j] > x:
            t[j+1] = t[j]
            j -= 1
        t[j+1] = x

Invariant de la boucle externe : « \(t[0..i-1]\) est triee et contient exactement les elements initialement en positions \(0\) a \(i-1\) ».

Invariant de la boucle interne : « \(t[j+2..i]\) est triee, tous ses elements sont \(> x\), et \(t[0..j] \cup t[j+2..i] \cup \{x\}\) est l'ensemble initial \(t[0..i]\) ».

Variant de la boucle interne : \(j+1\), entier positif decroissant de 1.

La preuve complete est detaillee dans la fiche d'exercices du chapitre 12.

def pgcd(a, b):
    """Precondition  : a >= 0, b >= 0, (a, b) != (0, 0).
    Postcondition : renvoie pgcd(a, b)."""
    if b == 0:
        return a
    return pgcd(b, a % b)

Terminaison. Variant : \(b\). C'est un entier naturel, et lorsque \(b \ne 0\), l'appel porte sur \((b, a \bmod b)\) dont le second argument verifie \(a \bmod b < b\). Le variant decroit strictement, la suite d'entiers naturels est finie : on atteint necessairement \(b = 0\).

Correction. Par recurrence forte sur \(b\).

• Base \(b = 0\) : la fonction renvoie \(a\), et \(\operatorname{pgcd}(a, 0) = a\) pour \(a > 0\). Correct.
• Heredite : soit \(b \ge 1\), supposons le resultat vrai pour tout \(b' < b\). Comme \(a \bmod b < b\), l'hypothese de recurrence s'applique a l'appel pgcd(b, a % b), qui renvoie donc \(\operatorname{pgcd}(b, a \bmod b)\). Or, en ecrivant \(a = bq + r\) avec \(r = a \bmod b\) : tout diviseur commun de \(a\) et \(b\) divise \(r = a - bq\), et tout diviseur commun de \(b\) et \(r\) divise \(a = bq + r\). Les deux couples ont donc les memes diviseurs communs, donc le meme pgcd. La fonction renvoie bien \(\operatorname{pgcd}(a,b)\).