Prouver la correction et la terminaison d’un algorithme

Un cap pour ce chapitre

Ce que vous saurez faire

Distinguer correction et terminaison.
Construire une preuve par invariant.
Utiliser un variant entier pour justifier l’arrêt.

Les bases utiles pour commencer

Commencer par une affirmation vérifiable

Une preuve nécessite une spécification : quelles entrées sont admises et quelle propriété doit satisfaire le résultat ? Pour une fonction de maximum, on impose un tableau non vide et on attend une valeur appartenant au tableau, supérieure ou égale à toutes les autres. Dire seulement « la fonction marche » ne fournit aucun objectif démontrable.

La correction partielle signifie que, si l’algorithme termine, son résultat satisfait la spécification. La terminaison établit qu’il finit effectivement. Les deux réunies permettent d’affirmer la correction totale dans les hypothèses données. Une boucle infinie ne devient pas acceptable sous prétexte qu’elle ne renvoie jamais de mauvais résultat.

Une spécification comporte aussi les effets autorisés. Une fonction qui calcule un maximum peut avoir pour contrat de ne pas modifier le tableau. Elle peut renvoyer la bonne valeur tout en violant cette exigence si elle efface les autres cases. Pour organiser la preuve, distinguez donc domaine d’entrée, résultat et modifications. Ce sont les affirmations à établir, pas des détails ajoutés après les essais.

Un invariant décrit ce qui reste vrai

Considérons une somme des n premières valeurs d’un tableau. Après k étapes, la variable s contient la somme des cases d’indices 0 à k - 1. Cette propriété est l’invariant. Avant le parcours, k = 0 et s = 0 : la somme du préfixe vide vaut zéro. Lors d’une étape, ajouter t[k] puis augmenter k étend exactement le préfixe représenté.

À la fin, k = n. L’invariant dit alors que s contient la somme de toutes les valeurs : c’est la postcondition souhaitée. Une preuve par invariant comporte donc initialisation, conservation et exploitation à la sortie, pas seulement une phrase citée sans vérification.

def somme(t):
    k, s = 0, 0
    while k < len(t):
        s = s + t[k]
        k = k + 1
    return s

Un variant mesure le chemin restant

Pour cette boucle, n - k est un entier positif tant que la condition est vraie. Il diminue d’une unité à chaque passage. Il ne peut donc pas décroître strictement indéfiniment tout en restant dans les entiers naturels. Cela prouve la terminaison. Le variant ne doit pas forcément être stocké dans une variable du programme : il peut s’agir d’une expression.

La simple phrase « la variable diminue » est insuffisante. Une suite de nombres réels positifs peut diminuer sans atteindre zéro. Il faut préciser un domaine et une borne qui rendent l’argument valable. Dans les preuves élémentaires du cours, un entier naturel strictement décroissant fournit ce cadre.

La quantité n-k n’est pas une estimation de durée en secondes. Elle sert uniquement à établir qu’il reste un nombre fini de progrès possibles. Plusieurs opérations peuvent avoir lieu avant sa diminution. À l’inverse, une variable qui diminue certains tours mais augmente à d’autres ne constitue pas directement le variant naturel strictement décroissant recherché.

Relier preuves, traces et tests

Une trace sur quelques valeurs aide à formuler l’invariant. Des tests sur un tableau vide, un seul élément et des valeurs négatives peuvent révéler une mauvaise initialisation. Mais une collection d’essais ne remplace pas le raisonnement sur toutes les entrées autorisées. Un seul contre-exemple suffit, en revanche, à réfuter une affirmation universelle.

Pour le tri par sélection, l’invariant précise le préfixe déjà placé ; pour la dichotomie, un variant compte les cases candidates. Réutiliser ces idées signifie adapter les propriétés au programme étudié. Réciter l’invariant d’un autre algorithme, même proche, peut conduire à une preuve fausse.

Exemple suivi : compter les valeurs positives

Pour un tableau t, on initialise k=0 et c=0. Tant que k < len(t), on ajoute 1 à c si t[k] > 0, puis on augmente k. L’invariant est : c compte les valeurs strictement positives parmi les k premières cases. Il vaut au départ puisque le préfixe vide ne contient aucune valeur positive.

Pour la conservation, deux cas suffisent. Si la prochaine valeur est positive, le nouveau préfixe contient exactement une valeur positive supplémentaire ; sinon le compteur ne change pas. Dans les deux cas, avancer k rétablit la propriété. À la sortie, toutes les cases sont traitées et l’invariant fournit la réponse. Le variant len(t)-k prouve séparément la terminaison. Le tableau vide donne directement zéro sans accès à une case.

Distinguer une propriété vraie d’une preuve suffisante

La propriété « le compteur est positif ou nul » est bien conservée par le programme précédent. Elle ne suffit pourtant pas à démontrer qu’il compte les valeurs positives. Un invariant doit relier l’état du programme à la spécification. Une propriété trop faible peut être vraie et inutile pour conclure.

On peut guider la recherche d’un invariant avec une trace de [-2,5,0,4] : après 0, 1, 2, 3 et 4 lectures, les compteurs valent 0, 0, 1, 1, 2. La trace suggère la relation au préfixe, mais il reste à démontrer sa conservation pour une valeur quelconque. Enfin, un contre-exemple suffit à rejeter une proposition générale : si un maximum initialisé à zéro échoue sur [-1], il n’est pas nécessaire d’accumuler cent autres essais pour établir le défaut.

À vous de faire varier les choses

Quel rôle joue cet argument ?

Classez chaque affirmation selon ce qu’elle établit réellement. Ne confondez pas un cas observé avec une preuve générale.

Lire les associations expliquées

Sur [3, -1, 5], la fonction renvoie 7. : Test particulier: Une entrée précise est testée ; les autres ne sont pas couvertes.
Au début de chaque tour, `s` est la somme des `k` premières cases. : Invariant ou étape de sa preuve: C’est une propriété conservée par les étapes.
`n - k` est un entier naturel qui diminue strictement. : Variant et terminaison: Cette mesure interdit une infinité d’itérations.
Au départ, `k` = 0 et la somme du préfixe vide vaut 0. : Invariant ou étape de sa preuve: Cela initialise l’invariant de somme.
La recherche termine immédiatement pour un tableau vide lors de mon essai. : Test particulier: L’observation concerne une entrée déterminée.
Après une comparaison sans égalité, le nombre de cases candidates diminue. : Variant et terminaison: Avec son caractère entier et sa borne, cela prouve l’arrêt de la dichotomie.
À la sortie, `k` = `n` : la propriété du préfixe devient la somme entière. : Invariant ou étape de sa preuve: C’est l’exploitation finale de l’invariant.
Ajouter t[`k`] puis avancer `k` étend correctement le préfixe résumé. : Invariant ou étape de sa preuve: Cet argument établit la conservation.
Pour toute taille `n`, au début de l’itération `k`, `c` compte exactement les valeurs positives parmi les `k` premières cases. Après le test de la case `k`, cette propriété s’étend au préfixe suivant. : Invariant ou étape de sa preuve: Il s’agit d’une relation générale et de sa conservation. Contrairement à un simple compteur non négatif, elle relie l’état au résultat attendu.
Le programme conserve `k`=0 et `s`=0 indéfiniment : la relation `s` = somme du préfixe de longueur `k` est toujours vraie, mais `n`-`k` ne diminue jamais. : Variant et terminaison: Le diagnostic concerne l’absence de progrès permettant de prouver l’arrêt. Un invariant peut rester vrai dans une boucle infinie.
Le maximum initialisé à zéro renvoie zéro sur [-1], alors que la spécification attend -1. : Test particulier: Ce test précis fournit un contre-exemple suffisant pour réfuter la correction universelle. Il n’est pas une preuve par invariant.

Indice 2

Reliez meilleur aux valeurs déjà examinées.

Comprendre la correction

Sur [2,9], conserver 2 préserve l’appartenance sans donner le maximum. La propriété utile est : meilleur est le maximum des k premières valeurs, avec k au moins 1. L’initialisation prend la première valeur et chaque comparaison étend le préfixe. La non-vacuité rend cette initialisation définie ; elle ne doit pas être oubliée dans le contrat.

Les erreurs qui méritent un détour

Appeler invariant une quantité qui doit diminuer.: Un invariant est une propriété conservée. Un variant est une mesure choisie pour prouver un progrès vers l’arrêt.
Oublier l’initialisation de la preuve.: Une propriété conservée mais fausse au départ ne permet aucune conclusion utile.

La fiche à garder

L’essentiel à retenir

Un contrat fixe ce qui doit être démontré.
L’invariant est initialisé, conservé puis exploité.
Le variant justifie la terminaison sous des hypothèses précises.

Cette notion au bac

Retrouvez ces idées dans un sujet complet, avec des indices, une correction expliquée et des ateliers.

Le prochain pas

Retrouver le catalogue de Première

Ce chapitre s’appuie sur le programme officiel de Première (PDF, nouvel onglet). Les explications et exercices sont proposés pour l’apprentissage.