L'écriture manuelle des tests unitaires est-elle une preuve d'exemple?

Nous savons que l'écriture de tests JUnit illustre un chemin particulier à travers votre code.

Un de mes associés a commenté:

L'écriture manuelle de tests unitaires est une preuve par exemple .

Il venait de l'arrière-plan de Haskell qui a des outils comme Quickcheck et la capacité de raisonner sur le comportement du programme avec les types .

Son implication était qu'il existe de nombreuses autres combinaisons d'entrées non testées par cette méthode pour lesquelles votre code n'est pas testé.

Ma question est la suivante: les tests unitaires écrits manuellement sont - ils des preuves par exemple?

Si vous choisissez au hasard des entrées pour les tests, je suppose qu'il est possible que vous exerciez une erreur logique de preuve par exemple.

Mais de bons tests unitaires ne font jamais cela. Au lieu de cela, ils traitent des plages et des cas de bord.

Par exemple, si vous deviez écrire des tests unitaires pour une fonction de valeur absolue qui accepte un entier en entrée, vous n'auriez pas besoin de tester toutes les valeurs d'entrée possibles pour prouver que le code fonctionne. Pour obtenir un test complet, vous n'auriez besoin que de cinq valeurs: -1, 0, 1 et les valeurs max et min pour l'entier d'entrée.

Ces cinq valeurs testent chaque plage possible et chaque cas de bord de la fonction. Vous n'avez pas besoin de tester toutes les autres valeurs d'entrée possibles (c'est-à-dire chaque nombre que le type entier peut représenter) pour obtenir un niveau de confiance élevé que la fonction fonctionne pour toutes les valeurs d'entrée.

Tout test de logiciel est comme "Proof By Example", pas seulement les tests unitaires utilisant un outil comme JUnit. Et ce n'est pas une nouvelle sagesse, il y a une citation de Dijkstra de 1960, qui dit essentiellement la même chose:

"Les tests montrent la présence, pas l'absence de bugs"

(il suffit de remplacer les mots "montre" par "preuves"). Cependant, cela est également vrai pour les outils qui génèrent des données de test aléatoires. Le nombre d'entrées possibles pour une fonction du monde réel est généralement plus élevé par ordre de grandeur que le nombre de cas de test que l'on peut produire et vérifier par rapport à un résultat attendu à l'ère de l'univers, indépendamment de la méthode de génération de ces cas, donc même si l'on utilise un outil générateur pour produire beaucoup de données de test, il n'y a aucune garantie de ne pas manquer le seul cas de test qui aurait pu détecter un certain bug.

Les tests aléatoires peuvent parfois révéler un bogue qui a été ignoré par les cas de test créés manuellement. Mais en général, il est plus efficace de créer soigneusement des tests pour la fonction à tester et de s'assurer que l'on obtient un code complet et une couverture de branche avec le moins de cas de test possible. Parfois, il est possible de combiner des tests générés manuellement et aléatoirement. De plus, lors de l'utilisation de tests aléatoires, il faut veiller à obtenir des résultats reproductibles.

Les tests créés manuellement ne sont donc en aucun cas pires que les tests générés de manière aléatoire, souvent bien au contraire.

L'écriture manuelle de tests est une "preuve par l'exemple". Mais QuickCheck l'est aussi, et dans une mesure limitée, les systèmes de type. Tout ce qui n'est pas une vérification formelle directe sera limité dans ce qu'il vous dit sur votre code. Au lieu de cela, vous devez penser en termes de mérite relatif des approches.

Les tests génératifs, comme QuickCheck, sont vraiment bons pour balayer un large espace d'entrées. C'est aussi beaucoup mieux pour s'attaquer aux cas marginaux que les tests manuels: les bibliothèques de tests génératifs seront plus expérimentées que vous dans ce domaine. D'un autre côté, ils ne vous parlent que des invariants, pas des sorties spécifiques. Donc , pour valider votre programme obtient les résultats corrects, vous avez encore besoin de quelques tests manuels pour vérifier que, en fait, foo(bar) = baz.