Bon, désolé, j'avais préparé quelque chose de mieux écrit, et suite à un clic mal placé, j'ai tout perdu. Pour résumer:
il est possible d'écrire un programme validant la terminaison d'un autre programme spécifique dont l'ensemble des données (interne et externe) sont bornées en taille mémoire. En d'autres termes une machine de Turing qui n'a pas une bande infinie...
C'est ce que je disais plus haut, et à quoi tu répondais "euh non, pas du tout": tu peux toujours exécuter le programme et voir ce que ça donne. Si tu bornes la taille mémoire utilisable, que tu stockes tous les états complets du programme et qu'à chaque étape tu vérifies que tu ne retombes pas dans un état déjà visité, alors en un temps irréaliste et avec une mémoire irréaliste, tu peux savoir si ton programme s'est terminé ou pas pour ces données là.
C'est un résultat relativement inutile. J'ose espérer que quand on parle de "preuve de programme" on essaye d'avoir une certaine généralité. Ici, on devra réappliquer la même procédure pour chaque nouveau jeu de données, et cette procédure ne fait rien économiser par rapport à exécuter le programme sans rien prouver.
Malheureusement les résultats un peu généraux sont algorithmiquement indécidables.
La page française mentionne l'indécidabilité algorithmique du problème suivant, par exemple: « le programme calcule un résultat correct par rapport à la spécification ».
(Ce qui, encore une fois, ne veut pas dire que l'on ne peut jamais rien prouver. En restreignant les problèmes considérés, on peut se ramener à des cas gérables.)
[^] # Re: C'est trop compliqué !
Posté par Yusei (Mastodon) . En réponse au journal Des langages de haut niveau. Évalué à 2.
C'est ce que je disais plus haut, et à quoi tu répondais "euh non, pas du tout": tu peux toujours exécuter le programme et voir ce que ça donne. Si tu bornes la taille mémoire utilisable, que tu stockes tous les états complets du programme et qu'à chaque étape tu vérifies que tu ne retombes pas dans un état déjà visité, alors en un temps irréaliste et avec une mémoire irréaliste, tu peux savoir si ton programme s'est terminé ou pas pour ces données là.
C'est un résultat relativement inutile. J'ose espérer que quand on parle de "preuve de programme" on essaye d'avoir une certaine généralité. Ici, on devra réappliquer la même procédure pour chaque nouveau jeu de données, et cette procédure ne fait rien économiser par rapport à exécuter le programme sans rien prouver.
Malheureusement les résultats un peu généraux sont algorithmiquement indécidables.
Pour conclure de mon côté, je renverrais les lecteurs intéressés, s'il en reste, vers le théorème de Rice pour plus de détails:
http://en.wikipedia.org/wiki/Rice's_theorem
http://fr.wikipedia.org/wiki/Th%C3%A9or%C3%A8me_de_Rice
La page française mentionne l'indécidabilité algorithmique du problème suivant, par exemple: « le programme calcule un résultat correct par rapport à la spécification ».
(Ce qui, encore une fois, ne veut pas dire que l'on ne peut jamais rien prouver. En restreignant les problèmes considérés, on peut se ramener à des cas gérables.)