Algorithmes, discipline de programmation et tests en MP2I : cours, méthodes et exercices corrigés

Q: Comment rédiger une preuve par invariant de boucle ?

On énonce une propriété I des variables, puis on la prouve en trois temps. Initialisation : I est vraie avant le premier tour. Conservation : si I et la condition de boucle sont vraies au début d'un tour, I est vraie à la fin. Conclusion : en sortie, la condition est fausse et I est vraie, ce qui donne la postcondition. Pour une boucle `for` sur `i`, l'invariant parle de l'état au début du tour d'indice `i`, par exemple « `s` vaut la somme de t[0..i-1] ». Un invariant prouvé mais pas exploité en sortie ne prouve rien.

Q: Quelle différence entre correction partielle et correction totale ?

Un algorithme est partiellement correct si, pour toute entrée qui vérifie sa précondition, le résultat vérifie la postcondition lorsqu'il s'arrête. Il est totalement correct s'il est partiellement correct et s'il termine sur toute entrée qui vérifie la précondition. L'invariant prouve la correction partielle, le variant la terminaison. Un sujet qui écrit « si la fonction se termine » dans une postcondition demande une correction partielle ; la terminaison se prouve à part.

Q: À quoi sert assert en C et en OCaml ?

`assert(condition)` vérifie, à l'exécution, une propriété qui doit être vraie, le plus souvent une précondition, placée avant l'opération risquée. Si elle est fausse, le programme C s'arrête avec un message qui donne la condition, le fichier et la ligne ; en OCaml, `assert` lève l'exception `Assert_failure`. La condition écrite est ce qui doit être vrai, et une assertion ne contient jamais d'effet : compilé avec l'option `-DNDEBUG`, un programme C n'exécute plus aucune assertion, et `ocamlc -noassert` les retire en OCaml.

Q: Comment construire un bon jeu de tests ?

On calcule chaque résultat attendu avant d'exécuter, et l'on écrit les tests sous forme d'assertions : un affichage n'est pas un test. On découpe le domaine des entrées en classes (sous, dans et au-dessus d'un intervalle ; tableau vide, d'une case, de plusieurs ; valeur en tête, en queue, absente) et l'on prend un représentant par classe, puis les valeurs limites : chaque borne et sa voisine. On ne teste pas une entrée hors de la précondition. Pour un tri, on vérifie l'ordre et la conservation des valeurs.

MP2I
Offert à l'essai

Algorithme et programme, paradigmes, compilation et interprétation ; entiers bornés et flottants ; terminaison par variant, correction par invariant ; complexité dans le pire cas, en moyenne et amortie ; spécification, programmation défensive et assertions, typage faible du C et fort d'OCaml, exceptions ; jeux de tests par partition et limites, graphe de flot de contrôle, couvertures et test exhaustif des conditions, en C et en OCaml.

16méthodes
33exercices corrigés
3problèmes
22pièges
37figures

Les nombres sont ceux du chapitre complet ; chaque filière voit la partie qui correspond à son programme.

Ce chapitre ouvre l'année de MP2I : il apprend à écrire un programme dont on peut répondre de la justesse, en C et en OCaml. On spécifie chaque fonction (signature, précondition, postcondition, effets), on se défend contre les entrées invalides par des assertions, on prouve qu'une boucle s'arrête par un variant et qu'elle calcule ce qu'on attend par un invariant, en distinguant correction partielle et correction totale. On compte le coût dans le pire cas, et sur des exemples simples le coût moyen et le coût amorti. On calcule juste avec des entiers bornés et des flottants. Enfin, on teste : jeux de tests construits par partition des entrées et valeurs limites, graphe de flot de contrôle, couverture des sommets, des arcs et des chemins sans cycle, test de toutes les façons d'évaluer une condition composée. Les sujets de Mines-Ponts, de CCINP et de Centrale-Supélec en filière MPI posent ces questions, reprises dans les exercices et les problèmes. Tous les programmes ont été compilés avec les options -Wall -Wextra -std=c99 ou par ocamlc, exécutés et testés.

Ce que tu sauras faire

Ce chapitre ouvre l'année. Il n'enseigne pas encore les langages, qui ont leurs chapitres : il enseigne ce qu'on fait de tout programme, dans les deux langages du programme, le C et OCaml. Écrire ce qu'une fonction doit faire, se protéger des entrées invalides, prouver qu'une boucle s'arrête et calcule le bon résultat, compter son coût, puis la soumettre à des tests bien choisis. À la fin, tu dois savoir :

distinguer un problème, un algorithme et un programme, et dire ce que fait un compilateur ;
prévoir les limites des entiers et des flottants de la machine, et comparer deux flottants correctement ;
prouver la terminaison d'une boucle par un variant, et sa correction par un invariant ;
donner la complexité dans le pire cas d'un code à boucles, et calculer un cas moyen ou un coût amorti sur un exemple simple ;
écrire la spécification d'une fonction, et la défendre par des assertions en C et en OCaml ;
écrire un jeu de tests par partition des entrées et test des limites ;
tracer le graphe de flot de contrôle d'une fonction, choisir des tests qui couvrent ses sommets ou ses arcs, et tester une condition composée de toutes les façons possibles.

L'essentiel : Algorithmes et programmes Extrait gratuit

Un extrait de la fiche « L'essentiel » du chapitre. Les démonstrations sont dans le cours détaillé.

À retenir Trois mots

Un problème : des entrées et la sortie attendue. Un algorithme : une méthode finie qui le résout, décrite sans langage. Un programme : la mise en œuvre d'un algorithme dans un langage.

Paradigmes : impératif (actions qui modifient des variables, boucles : le C), fonctionnel (valeur d'une expression, sans modification : OCaml), logique (on décrit ce qu'on veut : SQL, mentionné seulement). GOTO est hors programme.
Fichier source, fichier objet (gcc -c), exécutable (édition de liens). OCaml : ocamlc (code-octet, lancé par ocamlrun), ocamlopt (natif), boucle interactive ocaml. Un interprète exécute le source sans produire d'exécutable.
Interface (.h, .mli) : ce que le module promet. Implémentation (.c, .ml) : comment il le tient.

Une méthode du chapitre Extrait gratuit

Méthode Rédiger une preuve de correction par invariant

Quand l’utiliser

L'énoncé demande de « prouver la correction », ou de « montrer que la fonction renvoie » un résultat, pour une fonction à boucle.

Rappel de cours

Correction partielle : si la fonction s'arrête, le résultat est juste. Correction totale : correction partielle et terminaison. La preuve par invariant a trois temps : initialisation, conservation, conclusion par $\neg P \wedge I$ .

Démarche

Énoncer l'invariant $I$ en une phrase, avec les variables du code.
Initialisation : vérifier $I$ avec les valeurs d'avant la boucle.
Conservation : supposer $P$ et $I$ au début d'un tour, suivre les affectations du corps (en distinguant les cas d'un if), retrouver $I$ avec les nouvelles valeurs.
Conclusion : à la sortie, $\neg P$ et $I$ donnent la postcondition. Ajouter la terminaison (méthode 6) pour la correction totale.

Rédaction type

« Montrons que la propriété $I$ : « $a = q \times b + reste$ et $reste \geq 0$ » est un invariant. Initialisation : $q = 0$ et $reste = a \geq 0$ . Conservation : si $reste \geq b$ et $I$ , alors $(q + 1) b + (reste - b) = a$ et $reste - b \geq 0$ . Conclusion : en sortie, $reste < b$ ; avec $I$ , $a = q b + reste$ et $0 \leq reste < b$ . Avec le variant reste, la fonction est totalement correcte. »

Exemple traité

maximum (cours, section 5.5) : invariant « avant le tour d'indice $i$ , m est le maximum de $t[0..i[$ ». Initialisation : $i = 1$ et m = t[0], maximum de $t[0..1[$ . Conservation : si t[i] > m, m prend la valeur t[i], qui dépasse tout $t[0..i[$ ; sinon m dépasse déjà t[i] ; dans les deux cas, m est le maximum de $t[0..i + 1[$ . Conclusion : en sortie, $i = n$ , et m est le maximum de $t[0..n[$ . La boucle for fait $n - 1$ tours : la fonction termine.

Erreurs fréquentes

Prouver l'invariant et s'arrêter là : « une fois l'invariant prouvé, il reste à l'exploiter » (rapport d'oral du CCINP 2025, MPI).
Dire « on itère » au lieu de rédiger la récurrence sur les tours.
Oublier la terminaison quand l'énoncé demande la correction totale.

Pour s’entraîner

Exercices 8, 9, 14, 15, 16, 17, 18 et 30 ; problèmes 1 et 3.

Un exercice corrigé Extrait gratuit

Exercice Compter les occurrences ★☆☆

Langage : C.

Écrire une fonction int nb_occurrences(int t[], int n, int x) qui renvoie le nombre de cases de t[0..n-1] égales à x, avec sa spécification.
Énoncer un invariant de la boucle et prouver la correction de la fonction.
Écrire trois tests : aucune occurrence, une seule, et toutes les cases.

Indications

Méthode 7 : l'invariant d'une boucle for parle de l'état au début du tour d'indice i, donc des cases déjà lues, t[0..i-1].
Méthode 8 : initialisation, conservation, conclusion.

Analyse : comment trouver l’idée

On parcourt le tableau une fois, en augmentant un compteur à chaque case égale à x. Au début du tour d'indice i, on a lu les cases d'indice 0 à $i - 1$ : le compteur vaut le nombre d'occurrences dans cette partie.

Correction détaillée

Question 1.

/* nb_occurrences : int nb_occurrences(int t[], int n,
   int x)
   Precondition : n >= 0, t a au moins n cases.
   Valeur de retour : le nombre d'indices i < n tels
   que t[i] == x. */
int nb_occurrences(int t[], int n, int x) {
    int nb = 0;
    for (int i = 0; i < n; i = i + 1) {
        /* nb = occurrences de x dans t[0..i-1] */
        if (t[i] == x) {
            nb = nb + 1;
        }
    }
    return nb;
}

Question 2. Notons $I(i)$ : « nb est le nombre d'occurrences de x dans $t[0..i-1]$ ».

Initialisation : au premier tour, $i = 0$ ; la partie $t[0..-1]$ est vide et nb vaut 0.
Conservation : si $I(i)$ est vraie au début du tour d'indice $i$ , le tour ajoute 1 à nb exactement quand $t[i] = x$ ; à la fin du tour, nb compte les occurrences dans $t[0..i]$ : c'est $I(i+1)$ , vraie au début du tour suivant.
Conclusion : la boucle s'arrête quand $i = n$ (l'indice n'est modifié que par l'en-tête, et la borne ne change pas) ; $I(n)$ dit que nb est le nombre d'occurrences dans $t[0..n-1]$ , ce que la fonction renvoie.

La boucle fait exactement $n$ tours : la fonction termine, elle est totalement correcte, et son coût est linéaire en $n$ .

Question 3.

int main(void) {
    int t[5] = {2, 7, 2, 2, 9};
    int u[3] = {4, 4, 4};
    assert(nb_occurrences(t, 5, 5) == 0);
    assert(nb_occurrences(t, 5, 7) == 1);
    assert(nb_occurrences(u, 3, 4) == 3);
    assert(nb_occurrences(t, 0, 2) == 0);
    return 0;
}

Le quatrième test ajoute le cas limite du tableau vide ( $n = 0$ ).

Méthodes à retenir

L'invariant d'une boucle for porte sur l'état avant le corps, pour l'indice courant : « sur les cases déjà lues, $t[0..i-1]$ ». En sortie, on l'applique à $i = n$ . Voir les méthodes 7 et 8.

Dans le chapitre complet

Le cours détaillé, toute la fiche « L'essentiel », 16 méthodes, 22 pièges corrigés, la carte mentale, 33 exercices corrigés, 3 problèmes de concours, les fiches à mémoriser et l'assistant qui répond à tes questions. Ce chapitre est offert : il s’ouvre en entier avec un compte d’essai gratuit.

Ouvrir l'essai gratuit Une question ? WhatsApp

Plan du cours

Partie A. Algorithmes et programmes
- 1. Problème, algorithme, programme
- 1. Langage compilé, langage interprété
- 1. Les nombres de la machine
- 1. Terminaison
- 1. Correction partielle, correction totale, invariant
- 1. Complexité
Partie B. Discipline de programmation
- 7. Spécifier
- 1. Annoter un bloc
- 1. Programmation défensive et assertions
- 1. Ce que garantit chaque langage
- 1. Exceptions
- 1. Expliciter ses choix
Partie C. Validation et test
- 13. Jeux de tests
- 1. Partition des entrées et test des limites
- 1. Graphe de flot de contrôle
- 1. Couvertures
- 1. Test exhaustif d'une condition
- 1. Tester et prouver

Les méthodes du chapitre

Chaque méthode est une fiche : quand l'utiliser, le rappel de cours, les étapes, la rédaction attendue sur la copie, un exemple traité, les erreurs à éviter.

Écrire la spécification d'une fonction
Choisir entre précondition, assertion et valeur spéciale
Écrire une assertion juste en C et en OCaml
Prévenir un dépassement d'entier
Comparer des flottants et repérer un calcul instable
Prouver la terminaison d'une boucle par un variant
Trouver un invariant de boucle
Rédiger une preuve de correction par invariant
Annoter un code bloc par bloc et y trouver l'erreur
Évaluer la complexité d'un code à boucles
Construire un jeu de tests par partition et limites
Écrire un programme de test
Tracer le graphe de flot de contrôle d'une fonction
Choisir des tests qui couvrent les sommets, puis les arcs
Tester exhaustivement une condition composée
Trouver un contre-exemple à un code faux et le corriger

Les exercices corrigés

Chaque exercice a ses indications, sa correction rédigée et ce qu'il faut en retenir.

Application directe (13)

Que fait ce programme ?
Spécifier une fonction mystère
Entiers bornés et précondition vérifiée
Ce que le C laisse passer, ce qu'OCaml refuse
Une puissance de deux sans flottants
Des flottants qu'on ne compare pas avec ==
Des calculs qui s'arrêtent, ou pas
Compter les occurrences
Multiplier par additions
Confirmer ou réfuter une spécification
Une date valide
Le graphe de flot d'un maximum
Un affichage n'est pas un test

Entraînement (15)

Exponentiation rapide, version itérative
Le premier élément au moins égal à x
La multiplication russe
Le schéma de Horner
L'algorithme d'Euclide
Deux recherches fausses
Des tests trop pauvres
Tester un tri sans le lire
Terminaison d'un algorithme d'appariement
Couvrir les instructions ne suffit pas
Toutes les façons d'être bissextile
Analyse partitionnelle d'un code à six chiffres
Coût moyen d'une recherche
Comparer par soustraction
Annoter un second maximum

Approfondissement (5)

Trois catégories en un passage, annotées et fausses
Un producteur majoritaire en un passage
Un compteur binaire
Une écriture en base trois faussée par les flottants
Spécifier une fonction dont on ignore si elle termine

Les problèmes de concours

Des extraits de sujets réels, corrigés en entier, avec la durée conseillée et les méthodes mobilisées.

Déconnecter un réseau : correction partielle puis terminaison
Mines-Ponts 2024, filière MPI, informatique 1, section 1, questions 8, 10 et 11, complétée
Décrire une chaîne par un programme
Mines-Ponts 2023, filière MPI, informatique 2, questions 1 à 3, 7, 11 et 15 à 17
Calculer avec des flottants en C
CCINP 2023, filière MPI, oral d'informatique, exercice 8 de la sélection de sujets, questions 1 à 4 et 6, complétée

Questions fréquentes

Qu'est-ce qu'un variant de boucle ?

Un variant est une quantité qui prouve qu'une boucle s'arrête. Sa justification tient en trois points : c'est un entier ; il est positif tant que la condition de boucle est vraie ; il décroît strictement à chaque tour. Une suite d'entiers positifs strictement décroissante est finie : la boucle fait un nombre fini de tours. Dans une dichotomie entre deb et fin, le variant est fin - deb. Les rapports de jury relèvent que le caractère strict de la décroissance est souvent oublié : une quantité qui peut rester égale ne prouve rien.

Comment rédiger une preuve par invariant de boucle ?

On énonce une propriété $I$ des variables, puis on la prouve en trois temps. Initialisation : $I$ est vraie avant le premier tour. Conservation : si $I$ et la condition de boucle sont vraies au début d'un tour, $I$ est vraie à la fin. Conclusion : en sortie, la condition est fausse et $I$ est vraie, ce qui donne la postcondition. Pour une boucle for sur i, l'invariant parle de l'état au début du tour d'indice i, par exemple « s vaut la somme de $t[0..i-1]$ ». Un invariant prouvé mais pas exploité en sortie ne prouve rien.

Quelle différence entre correction partielle et correction totale ?

Un algorithme est partiellement correct si, pour toute entrée qui vérifie sa précondition, le résultat vérifie la postcondition lorsqu'il s'arrête. Il est totalement correct s'il est partiellement correct et s'il termine sur toute entrée qui vérifie la précondition. L'invariant prouve la correction partielle, le variant la terminaison. Un sujet qui écrit « si la fonction se termine » dans une postcondition demande une correction partielle ; la terminaison se prouve à part.

À quoi sert assert en C et en OCaml ?

assert(condition) vérifie, à l'exécution, une propriété qui doit être vraie, le plus souvent une précondition, placée avant l'opération risquée. Si elle est fausse, le programme C s'arrête avec un message qui donne la condition, le fichier et la ligne ; en OCaml, assert lève l'exception Assert_failure. La condition écrite est ce qui doit être vrai, et une assertion ne contient jamais d'effet : compilé avec l'option -DNDEBUG, un programme C n'exécute plus aucune assertion, et ocamlc -noassert les retire en OCaml.

Comment construire un bon jeu de tests ?

On calcule chaque résultat attendu avant d'exécuter, et l'on écrit les tests sous forme d'assertions : un affichage n'est pas un test. On découpe le domaine des entrées en classes (sous, dans et au-dessus d'un intervalle ; tableau vide, d'une case, de plusieurs ; valeur en tête, en queue, absente) et l'on prend un représentant par classe, puis les valeurs limites : chaque borne et sa voisine. On ne teste pas une entrée hors de la précondition. Pour un tri, on vérifie l'ordre et la conservation des valeurs.

Qu'est-ce que la couverture des arcs et des chemins sans cycle ?

Le graphe de flot de contrôle d'une fonction a un sommet par bloc d'instructions et par condition, et un arc par passage possible. Un jeu de tests couvre les sommets s'il exécute chaque instruction, les arcs s'il emprunte chaque branche, y compris la branche « faux » d'un if sans else. Un chemin de l'entrée à la sortie est dit sans cycle quand il parcourt chaque boucle au plus une fois ; couvrir les chemins sans cycle faisables est plus exigeant que couvrir les arcs, qui l'est plus que couvrir les sommets. Certains chemins sont infaisables : aucune entrée ne les suit. Aucune couverture ne prouve l'absence d'erreur.

Comment y accéder

Ce chapitre fait partie des chapitres offerts : il s'ouvre en entier avec un compte d'essai gratuit. Créer un compte d'essai ou se connecter. Pour l'accès complet, les tarifs ou une question, écris-nous sur WhatsApp.