Peut-on tout prouver ? Peut-on tout tester ?

Prouver et analyser : la boîte à outils formalisée · niveau 3 (difficile)

Énoncé

Discuter des limites théoriques de la preuve de terminaison et du test de correction.

Preuve de terminaison : D'après le théorème d'indécidabilité de l'arrêt de Turing (1936), il n'existe aucun algorithme général capable de décider si un programme quelconque se termine sur une entrée donnée. La preuve de terminaison doit donc se faire au cas par cas.
Test de correction : Un jeu de tests est par nature de taille finie. Si le domaine d'entrée est infini, le test ne peut pas garantir la validité absolue du programme (il ne peut que mettre en évidence la présence de bogues, pas prouver leur absence). La preuve valide la logique abstraite de l'algorithme sur l'ensemble de son domaine, tandis que le test confronte le programme réel aux spécificités physiques de la machine.