Correction et terminaison d'un programme

Vue d'ensemble

Un programme qui « marche sur les exemples » n'est pas un programme prouvé. Aux concours comme en khôlle, on te demande de justifier qu'une fonction fait bien ce qu'elle promet : qu'elle s'arrête (terminaison) et qu'elle renvoie le bon résultat (correction). Deux outils suffisent pour les boucles : l'invariant (une propriété conservée à chaque tour, qui prouve la correction) et le variant (une quantité entière qui décroît, qui prouve la terminaison). Cette fiche pose le vocabulaire, puis déroule une preuve complète du début à la fin.

Au programme (tronc commun, 1^re année — BO 2021) — Spécification d'une fonction (préconditions, postconditions) ; assertions ; invariant de boucle et preuve de correction ; variant de boucle et preuve de terminaison ; correction partielle et correction totale.

Prérequis

Écrire et dérouler une boucle while (condition, corps, progression)
Le motif de l'accumulateur (une variable mise à jour à chaque tour)
Manipuler les listes : indexation t[i], longueur len(t)
Raisonner par récurrence sur les entiers

🎯 Accompagnement Majorant

Tu sais coder la boucle mais tu sèches quand on te demande de la « prouver » ? C'est le réflexe qui sépare une copie moyenne d'une bonne copie. Nos mentors alumni X · Centrale · Mines t'apprennent à rédiger invariant, variant et conclusion dans le bon ordre, sur tes propres DS, jusqu'à ce que ça coule tout seul.

Trouver un mentor →

1. Spécifier une fonction : préconditions et postconditions

Définition 1.1 — Précondition et postcondition

La précondition d'une fonction est ce qu'elle suppose vrai sur ses arguments pour fonctionner (à la charge de l'appelant). La postcondition est ce qu'elle garantit sur son résultat lorsque la précondition est respectée. Spécifier une fonction, c'est écrire ce contrat avant d'écrire le code.

def racine_entiere(n):
    # Precondition  : n est un entier, n >= 0
    # Postcondition : renvoie r tel que r*r <= n < (r+1)*(r+1)
    r = 0
    while (r + 1) * (r + 1) <= n:
        r = r + 1
    return r

🔍 Décryptage ligne par ligne

# Precondition : n >= 0Ce qu'on exige de l'appelant. La fonction n'a de sens que pour un entier positif ou nul. Sur un n négatif, on ne promet rien : c'est un usage hors contrat.

# Postcondition : r*r <= n < (r+1)*(r+1)Ce qu'on promet en retour. Le résultat r est la partie entière de

n

: le plus grand entier dont le carré ne dépasse pas n.

while (r + 1) * (r + 1) <= n:On avance tant qu'on peut. On augmente r d'un cran tant que (r+1)² reste

⩽ n

. Dès que (r+1)² dépasse n, on s'arrête : r vérifie la postcondition.

📝 À quoi ça sert. La postcondition dit quoi prouver (la correction) ; la précondition dit sous quelle hypothèse. Sans spécification écrite, la phrase « prouver que le programme est correct » n'a même pas de sens : correct par rapport à quoi ?

2. Les assertions : l'instruction assert

Définition 2.1 — Assertion

L'instruction assert condition vérifie, pendant l'exécution, qu'une propriété est vraie. Si la condition est vraie, le programme continue sans rien changer ; si elle est fausse, il s'arrête aussitôt en levant une AssertionError. C'est le moyen le plus simple de faire respecter une précondition et de tester ses hypothèses.

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

print(racine_entiere(17))   # 4
# racine_entiere(-2)  leverait AssertionError

🔍 Décryptage ligne par ligne

assert n >= 0, "..."On matérialise la précondition dans le code. Si n < 0, l'exécution s'arrête net avec le message donné : on repère l'appel fautif immédiatement, au lieu d'obtenir un résultat faux plus loin.

print(racine_entiere(17))Usage conforme. 17 >= 0 est vrai : l'assertion passe silencieusement et la fonction renvoie 4 (car

4^2 = 16 \leqslant 17 &lt; 25 = 5^2

# racine_entiere(-2)Usage hors contrat. Ici l'assertion serait fausse et lèverait AssertionError : le bug est signalé à la source.

📝 assert n'est pas un if. Une assertion sert à vérifier une propriété que tu crois toujours vraie (précondition, invariant, cohérence interne). Elle documente et teste ; elle ne gère pas les cas normaux du programme. Pour réagir proprement à une saisie utilisateur, on utilise un if, pas un assert.

3. Invariant de boucle : prouver la correction

Définition 3.1 — Invariant de boucle

Un invariant d'une boucle est une propriété P qui est vraie avant d'entrer dans la boucle et qui reste vraie après chaque tour (on dit qu'elle est préservée). Bien choisi, l'invariant, combiné à la condition d'arrêt, donne directement la correction du résultat.

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

🔍 Décryptage ligne par ligne

m = t[0]Le meilleur candidat de départ. Avant tout parcours, le maximum vu se limite au premier élément.

while i < len(t):On parcourt le reste. i désigne la case qu'on s'apprête à examiner ; les cases t[0] à t[i-1] ont déjà été traitées.

if t[i] > m:
    m = t[i]

Mise à jour du record. Si l'élément courant bat le maximum courant, il devient le nouveau maximum.

Invariant de la boucle maximum

Au début de chaque tour, m est le maximum de la tranche déjà vue, c'est-à-dire $m = max (t [0], t [1], \dots, t [i - 1])$ . Initialisation : avant la boucle, i = 1 et m = t[0], donc $m = max (t [0])$ , vrai. Conservation : si m est le max de t[0..i-1], alors après avoir comparé t[i] et incrémenté i, m devient le max de t[0..i]. À la sortie i = len(t), donc m est le max de tout le tableau : le résultat est correct.

📐 Méthode — trouver le bon invariant.

Regarde ce que vaut la variable de résultat après quelques tours : c'est souvent « le résultat partiel sur la portion déjà traitée ».
Vérifie l'initialisation : l'invariant est-il vrai juste avant la boucle (portion traitée vide) ?
Vérifie la conservation : en supposant l'invariant vrai en début de tour, l'est-il encore après une exécution du corps ?
Combine l'invariant avec la condition d'arrêt : c'est ce qui donne la postcondition, donc la correction.

4. Variant : prouver la terminaison

Définition 4.1 — Variant de boucle

Un variant d'une boucle est une quantité entière qui reste positive ou nulle tant que la boucle s'exécute et qui décroît strictement à chaque tour. Un entier positif ne peut pas décroître indéfiniment : son existence prouve que la boucle termine.

Reprenons la boucle maximum. Posons $v = len(t) - i$ . Au début d'un tour, la condition i < len(t) assure $v \geqslant 1 > 0$ . Chaque tour fait i = i + 1, donc v diminue exactement de 1 : il est entier, positif et strictement décroissant. La boucle fait donc au plus len(t) - 1 tours puis s'arrête.

💡 Le réflexe. Le variant est presque toujours « la distance qui reste à parcourir » : d - g pour la dichotomie, len(t) - i pour un parcours, n - i pour une somme, la valeur elle-même pour un compte à rebours. Cherche ce qui rapproche de la sortie.

📝 Positif ET strictement décroissant. Les deux conditions sont indispensables. Une quantité qui décroît mais peut devenir négative (par exemple i qui saute la valeur d'arrêt) ne garantit rien : c'est la source la plus fréquente de boucle infinie.

5. Correction partielle et correction totale

Définition 5.1 — Correction partielle et correction totale

Une fonction est partiellement correcte si, lorsqu'elle termine, son résultat vérifie la postcondition (« si ça s'arrête, le résultat est bon »). Elle est totalement correcte si elle est partiellement correcte et qu'elle termine toujours (sous la précondition).

Le partage du travail

Ces deux notions se prouvent avec deux outils distincts :

L'invariant (+ condition d'arrêt) prouve la correction partielle.
Le variant prouve la terminaison.

D'où l'égalité à retenir : correction totale = correction partielle + terminaison, soit invariant + variant.

📝 Pourquoi distinguer. Une fonction peut être partiellement correcte sans être totalement correcte : si elle boucle à l'infini sur certaines entrées, elle ne renvoie jamais de résultat faux… mais elle ne renvoie rien. La correction partielle seule ne suffit donc jamais : il faut toujours aussi la terminaison.

6. Exemple entièrement traité : la somme 0+1+...+n

Prouvons complètement, du variant à la conclusion, la fonction qui calcule $0 + 1 + \dots + n$ par une boucle.

def somme(n):
    # Precondition  : n est un entier, n >= 0
    # Postcondition : renvoie 0 + 1 + ... + n
    s = 0
    i = 0
    while i <= n:
        s = s + i
        i = i + 1
    return s

🔍 Décryptage ligne par ligne

s = 0L'accumulateur. s stockera la somme construite au fur et à mesure. Une somme vide vaut 0.

i = 0Le compteur. i est le prochain entier à ajouter. On commence à 0.

while i <= n:On additionne jusqu'à n inclus. La condition est <= (et non <) car on veut ajouter n lui-même.

s = s + iOn ajoute i à la somme. C'est le tour qui fait grossir l'accumulateur.

i = i + 1La progression. On passe à l'entier suivant ; c'est ce qui fera décroître le variant et terminer la boucle.

Exécution pas à pas — somme(4), avec le variant n − i au moment du test
Tour	i	s avant	s après	variant n − i
1	0	0	0	4
2	1	0	1	3
3	2	1	3	2
4	3	3	6	1
5	4	6	10 ✓	0

Théorème 6.1 — Correction totale de la fonction somme ★ À savoir démontrer

Pour tout entier n tel que $n ⩾ 0$ , l'appel somme(n) termine et renvoie $0 + 1 + \dots + n = \frac{n ( n + 1 )}{2}$ .

Démonstration

On note P(i) l'invariant : $s = 0 + 1 + \dots + (i - 1)$ (la somme des entiers de 0 à i − 1, avec la convention qu'une somme vide vaut 0).

Initialisation. Avant le premier tour, i = 0 et s = 0. L'invariant P(0) affirme $s =$ (somme vide) $= 0$ , ce qui est vrai.

Conservation. Supposons P(i) vrai au début d'un tour, avec $i ⩽ n$ : $s = 0 + 1 + \dots + (i - 1)$ . Le corps exécute d'abord s = s + i, d'où $s^{'} = (0 + \dots + (i - 1)) + i = 0 + 1 + \dots + i$ , puis i = i + 1, d'où $i^{'} = i + 1$ . On a bien $s^{'} = 0 + 1 + \dots + (i^{'} - 1)$ : P(i') est vrai. L'invariant est préservé.

Terminaison. Posons le variant $v = n - i$ . Au début d'un tour, la condition i <= n donne $v ⩾ 0$ . Chaque tour fait i = i + 1, donc $v$ diminue exactement de 1 : c'est un entier positif strictement décroissant. Il ne peut décroître indéfiniment, donc la boucle s'arrête (après $n + 1$ tours).

Conclusion (correction). À la sortie, la condition i <= n est fausse ; comme i augmente de 1 en 1 et valait n au dernier tour effectué, on a exactement i = n + 1. Par l'invariant P(n+1) : $s = 0 + 1 + \dots + n = \frac{n ( n + 1 )}{2}$ . Le résultat vérifie la postcondition. La boucle terminant (variant) et le résultat étant correct (invariant), la fonction est totalement correcte. $■$

🎯 Accompagnement Majorant

« Initialisation, conservation, terminaison, conclusion » : tu récites mais tu bloques à l'écrit ? Nos mentors te font rédiger la preuve complète sur cinq boucles-types (somme, max, factorielle, dichotomie, Euclide) jusqu'à ce que le plan devienne automatique en DS.

Trouver un mentor →

7. Pièges classiques

⚠ Confondre variant et invariant. L'invariant est une propriété (vraie/fausse) qui sert la correction ; le variant est un nombre entier qui décroît et sert la terminaison. « n − i » n'est pas un invariant, « s = 0+…+(i−1) » n'est pas un variant.

⚠ Oublier le cas de sortie. Un invariant vrai ne suffit pas : il faut le combiner avec la condition d'arrêt pour conclure. Si tu ne dis pas ce que vaut la variable de contrôle à la sortie (ici i = n + 1), la preuve de correction est incomplète.

⚠ Un invariant faux (ou trop faible). Un invariant doit être vrai dès l'initialisation et préservé à chaque tour. Un « invariant » qui ne tient pas au premier tour, ou qui ne redevient vrai qu'à la toute fin, ne prouve rien. Teste-le toujours sur l'initialisation.

⚠ Un variant qui peut devenir négatif. Si la quantité choisie décroît mais « rate » la valeur d'arrêt (par exemple une condition i != n avec un pas de 2), elle peut passer sous zéro sans jamais déclencher la sortie : la boucle ne termine pas. Le variant doit rester

⩾ 0

tant que la boucle tourne.

⚠ Croire que « ça marche sur un exemple » = « c'est prouvé ». Dérouler une trace illustre, mais ne démontre pas. Seuls un invariant et un variant rédigés constituent une preuve valable aux yeux d'un correcteur.

8. Exercices d'application

Rédige-les sur papier avant d'ouvrir le corrigé, puis passe au quiz en bas de fiche.

Exo 1Invariant d'un produitFacile

On considère la fonction ci-dessous. Donne un invariant de la boucle, puis déduis-en ce que renvoie puissance(x, n).

def puissance(x, n):
    # Precondition : n >= 0
    p = 1
    k = 0
    while k < n:
        p = p * x
        k = k + 1
    return p

Voir la correction détaillée

Invariant proposé : au début de chaque tour,

p = x^{k}

Initialisation : avant la boucle k = 0 et p = 1, donc

p = x^{0}

. Vrai.

Conservation : si

p = x^{k}

, après p = p * x on a

p = x^{k + 1}

, puis k = k + 1 redonne

p = x^{k}

pour le nouveau k.

Sortie : la condition k < n devient fausse avec k = n, donc

p = x^{n}

. La fonction renvoie

x^{n}

. (Variant : n − k.)

Exo 2Le bon variantIntermédiaire

Pour la boucle d'Euclide ci-dessous, propose un variant entier positif strictement décroissant et conclus quant à la terminaison.

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

Voir la correction détaillée

Variant :

v = b

(la valeur de b), qui est un entier

⩾ 0

À chaque tour, la nouvelle valeur de b est a % b, le reste de la division par b : il est strictement inférieur à b (car

0 \leqslant a \bmod b &lt; b

). Donc v décroît strictement.

Un entier positif strictement décroissant ne peut décroître indéfiniment : b finit par valoir 0, la condition b != 0 devient fausse et la boucle termine.

Exo 3Rédiger une preuve complèteDifficile

Prouve la correction totale de la fonction suivante, censée calculer la factorielle $n! = 1 \times 2 \times \dots \times n$ (avec $0! = 1$ ). Énonce un invariant, un variant, et conclus.

def factorielle(n):
    # Precondition : n >= 0
    f = 1
    k = 1
    while k <= n:
        f = f * k
        k = k + 1
    return f

Voir la correction détaillée

Invariant : au début de chaque tour,

f = (k - 1)!

. Initialisation : k = 1, f = 1 = 0!. Vrai.

Conservation : si

f = (k - 1)!

, après f = f * k on a

f = (k - 1)! \times k = k!

, puis k = k + 1 redonne

f = (k - 1)!

pour le nouveau k.

Terminaison : variant

v = n - k + 1

. Au début d'un tour k <= n donne

v \geqslant 1 &gt; 0

; chaque tour augmente k de 1, donc v décroît de 1. Entier positif strictement décroissant : la boucle s'arrête.

Conclusion : à la sortie k = n + 1, donc par l'invariant

f = (k - 1)! = n!

. Correction partielle (invariant) + terminaison (variant) = correction totale.

Récap final — Ce qu'il faut absolument retenir

À la veille d'une khôlle ou d'un DS, parcours cette checklist : tu dois pouvoir répondre « oui, sans hésiter » à chaque question.

Sais-tu distinguer précondition (hypothèse sur les arguments) et postcondition (garantie sur le résultat) ?
Sais-tu à quoi sert assert et pourquoi ce n'est pas un if ?
Sais-tu qu'un invariant prouve la correction et un variant la terminaison ?
Sais-tu qu'un variant est un entier $⩾ 0$ qui décroît strictement à chaque tour ?
Sais-tu vérifier un invariant en trois temps (initialisation, conservation, sortie) ?
Sais-tu que correction totale = correction partielle + terminaison ?
Sais-tu rédiger une preuve complète de boucle sans oublier le cas de sortie ?
Sais-tu qu'une trace « qui marche » n'est pas une preuve ?

À savoir refaire

Correction totale de la somme 0+1+…+n — invariant $s = 0 + 1 + \dots + (i - 1)$ , variant $n - i$ , conclusion en i = n+1.

Vue d'ensemble

Prérequis

1. Spécifier une fonction : préconditions et postconditions

2. Les assertions : l'instruction assert

3. Invariant de boucle : prouver la correction

4. Variant : prouver la terminaison

5. Correction partielle et correction totale

6. Exemple entièrement traité : la somme 0+1+...+n

7. Pièges classiques

8. Exercices d'application

Récap final — Ce qu'il faut absolument retenir

À savoir refaire

Débloque la fiche complète

Quiz — Correction et terminaison

Fiches associées

Recherche par dichotomie

Variables, types et affectations

Conditions et booléens

Boucles for et while

Fonctions : paramètres et valeurs de retour

Listes et chaînes de caractères

Tu veux aller plus loin sur ce chapitre ?