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

Exercice · informatique (tronc commun des prépas scientifiques), chapitre 10 — Prouver et analyser : la boîte à outils formalisée

É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.

Un blocage sur cet exercice ? Le tuteur d'Adloun guide par questions, sans donner la réponse.