Terminaison et correction

Terminaison

Prouver la terminaison d'un algorithme signifie démontrer que l'algo termine.

i) Pour les fonctions récursives

• Mettre des assert ("s'assurer que") au début, pour traiter uniquement les cas qui nous intéressent
• Trouver un variant de boucle, c'est-à-dire une variable ou somme de variables qui :
  1. Lorsque le variant vaut $0$ ou moins, la fonction ne fait aucun appel récursif
  2. Sinon, le variant décroit strictement

ii) Pour les boucles while(condition)

C'est exactement la même chose sauf la condition (1.) qui change légèrement :

• Trouver un variant de boucle, c'est-à-dire une variable ou somme de variables qui :
  1. Lorsque le variant vaut $0$ ou moins, la condition n'est plus respectée
  2. Sinon, le variant décroit strictement

iii) Pour les boucles for

Les boucles for terminent toujours.

Correction

Prouver la correction d'un algorithme signifie démontrer que l'algo renvoie bien ce qu'on veut qu'il renvoie.

Il faut toujours faire la terminaison après la correction !

i) Pour les fonctions récursives (pas besoin d'invariant de boucle ici)

On a déjà démontré la terminaison. Il suffit donc de démontrer :

1. Les cas initiaux sont corrects
2. En supposant les appels récursifs corrects, expliquer pourquoi la fonction est correcte

ii) Pour les boucles while(condition) (invariant de boucle)

• Pour ne pas t'emmêler les pinceaux, je te conseille de toujours rédiger les deux phrases suivantes :

1. On a déjà démontré la terminaison : le test condition est donc effectué $i_{max}$ fois.
2. Pour toute variable v, on note $v_i$ sa valeur lorsque le test condition est effectué pour la $i^{\text{ème}}$ fois.

• Invariant de boucle

Il faut que tu trouves un prédicat $P_i$ que tu exprimes grâce à la notation présentée au point (2.) tel que :

1. $$\forall i \in \{1, ..., i_{max}\}, P_i \text{ est vrai}$$
2. $$P_{i_{max}}\text{ correspond exactement à ce que tu veux démontrer}$$

iii) Pour les boucles for (invariant de boucle)

• Je te conseille de commencer par rédiger :

• Invariant de boucle

Notre $i_{max}$ correspond simplement au nombre d'itérations de notre boucle for. Ensuite c'est pareil !

Il faut que tu trouves un prédicat $P_i$ que tu exprimes grâce à la notation présentée ci-dessus tel que :

1. $$\forall i \in \{1, ..., i_{max}\}, P_i \text{ est vrai}$$
2. $$P_{i_{max}}\text{ correspond exactement à ce que tu veux démontrer}$$

Exercices

Exercice 1 : Terminaison (récursif)

Soit la fonction suivante :

def somme_n(n):
    assert n >= 0
    if n == 0:
        return 0
    return n + somme_n(n-1)

1. Définir un variant de récursion et montrer que la fonction termine pour tout entier $n \ge 0$.
2. Vérifier que la fonction renvoie bien la somme des $n$ premiers entiers.

Exercice 2 : Terminaison (boucle while)

Écrire une fonction qui calcule le plus grand commun diviseur (PGCD) de deux entiers a et b avec l’algorithme d’Euclide :

def pgcd(a, b):
    while b != 0:
        a, b = b, a % b
    return a

1. Identifier un variant de boucle et démontrer que la boucle termine.
2. Proposer un invariant de boucle pour montrer que l’algorithme est correct.

Exercice 3 : Terminaison (boucle for)

Écrire une fonction qui calcule la factorielle d’un entier $n \ge 0$ :

def factorielle(n):
    f = 1
    for i in range(1, n+1):
        f *= i
    return f

1. Montrer que la boucle for termine toujours.
2. Proposer un invariant de boucle et démontrer la correction de l’algorithme.

Exercice 4 : Invariant de boucle avancé

On souhaite trier une liste L de taille $n$ en utilisant le tri par insertion :

def tri_insertion(L):
    for i in range(1, len(L)):
        x = L[i]
        j = i
        while j > 0 and L[j-1] > x:
            L[j] = L[j-1]
            j -= 1
        L[j] = x

1. Définir un variant de boucle pour la boucle while.
2. Proposer un invariant de boucle pour la boucle for.
3. Montrer que l’algorithme termine et est correct.

Exercice 5 : Analyse combinée

Pour chaque fonction ou boucle ci-dessous, indiquer :

1. La terminaison (variant de boucle ou récursion).
2. L’invariant de boucle (si applicable) pour démontrer la correction.

a) Fonction qui retourne le plus petit élément d’une liste :

def minimum(L):
    min_val = L[0]
    for x in L:
        if x < min_val:
            min_val = x
    return min_val

b) Fonction récursive qui calcule la suite de Fibonacci :

def fib(n):
    if n <= 1:
        return n
    return fib(n-1) + fib(n-2)

Quelques redactions type pour la correction

Le plus dur est encore que tu aies l'intuition pour pouvoir exhiber un invariant de boucle.

Mais ça va venir avec l'entraînement.

Voici les corrections des exos 1 et 2.