Que prouve un test qui réussit ?
Les méthodes formelles servent à prouver qu’un programme est correct pour tous les cas, alors qu’un test n’en essaie que quelques-uns. Cette leçon montre pourquoi la différence compte.
Une boutique en ligne offre la livraison dès 50 euros. Le programmeur écrit total > 50. Deux tests réussissent, avec 20 et 80 euros. Pourtant un client qui paie exactement 50 euros se voit facturer la livraison. Aucun test n’avait essayé ce cas.
À la fin de cette leçon
Remarque
Je peux dire ce qu’un test montre et ce qu’une preuve montre.
Mots-clés
| Mot | Ce que ça veut dire | Exemple |
|---|---|---|
| Test | un essai du programme sur quelques valeurs choisies | |
| Cas | une valeur d’entrée possible | un panier de 50 euros |
| Preuve | un raisonnement qui vaut pour tous les cas | |
| Contre-exemple | un cas qui montre qu’une affirmation est fausse | |
| Propriété | une règle que le programme doit toujours respecter | |
| Méthode formelle | une méthode où une machine vérifie une propriété sur tous les cas |
Les cellules que les étudiants remplissent restent vides dans cet aperçu.
Un test n’essaie que les cas choisis
Un test lance le programme sur des valeurs choisies et compare le résultat à celui qu’on attend. Si les deux sont égaux, le test réussit.
Il dit seulement que ces valeurs-là marchent. Il ne dit rien des autres. La commande compare le code (> 50) à la règle (>= 50) pour 20 puis 80 euros. Elle affiche 1 deux fois : les deux sont d’accord.
Deux tests qui réussissent
awk 'BEGIN { print (20 > 50) == (20 >= 50), (80 > 50) == (80 >= 50) }'Affichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
Essayer tous les cas trouve la faille
Ici le panier va de 0 à 100 euros : seulement 101 cas. On peut donc tous les essayer, un par un.
La commande suivante parcourt les 101 montants. Elle affiche chaque montant où le code et la règle ne sont pas d’accord.
Chercher les montants où ils diffèrent
seq 0 100 | awk '{ if (($1 > 50) != ($1 >= 50)) print "ecart pour", $1 }'Affichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
Exemple travaillé : cinq montants
| Panier (euros) | Code : total > 50 | Règle : total >= 50 | Même réponse ? |
|---|---|---|---|
| 20 | livraison payante | livraison payante | oui |
| 49 | livraison payante | livraison payante | oui |
| 50 | livraison payante | livraison offerte | non : contre-exemple |
| 51 | livraison offerte | livraison offerte | oui |
| 80 | livraison offerte | livraison offerte | oui |
Les cellules que les étudiants remplissent restent vides dans cet aperçu.
Une preuve parle de tous les cas
Une preuve porte sur tous les cas à la fois. Quand les cas sont peu nombreux, les essayer tous est déjà une preuve.
La commande compte les montants où le code se trompe, parmi les 101. Elle trouve un seul cas. Un test aurait pu l’oublier. La vérification complète, jamais.
Compter les cas où le code se trompe
seq 0 100 | awk '{ if (($1 > 50) != ($1 >= 50)) n++ } END { print n, "cas sur", NR }'Affichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
Parfois, il y a trop de cas
Un nombre sur 64 bits peut prendre 2 puissance 64 valeurs. Les essayer toutes est impossible en pratique.
La première commande affiche ce nombre de valeurs. La seconde calcule combien d’années il faudrait, à un milliard d’essais par seconde.
Le nombre de valeurs sur 64 bits
python3 -c "print(2 ** 64)"Affichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
Le temps pour toutes les essayer
python3 -c "print(2 ** 64 // 10 ** 9 // (3600 * 24 * 365))"Affichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
Erreur fréquente
Attention
Beaucoup de gens pensent que mille tests réussis prouvent qu’un programme est juste. Mille tests prouvent seulement que ces mille cas marchent. Pour une valeur jamais essayée, rien n’est dit. Une preuve, ou un contre-exemple, parle de tous les cas.
Pour aller plus loin
Changez la règle : la livraison est offerte dès 60 euros, et le code écrit > 60. Refaites la commande qui cherche les écarts.
Elle affiche un seul montant. Cherchez lequel avant de lancer la commande, puis dites pourquoi ce montant est celui où un test oublie de regarder.