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
Ce qui m'ennuie avec cette phrase et qu'elle induit violamment en erreur. Dénombrer exhaustivement puis évaluer tous les états d'un programme n'est pas du tout équivalent avec l'execution d'un programme sur l'ensemble des jeu de données possibles à raison d'un million d'execution par jeu. Dans le second cas rien n'indique que l'on a effectivement couvert tous les états possibles. Un état particulier peut très bien ne se produire que dans certaines conditions très précises.
Par exemple si on cumule des arrondis au delà de la limite du CPU, on peut parfaitement avoir un programme qui calcule juste sur un ordinateur et faux sur celui d'à coté.
De plus il n'est pas question d'executer ici le programme, mais de valider ses etat. Celà se fait le plus souvent de façon totalement extérieure au programme. Enfin il ne s'agit pas de valider le programme pour un seul et unique jeu de données, mais pour un ensemble de données toutes bornées.
Avec la doc du CPU et du compilateur il est souvent à peine plus complexe de valider un état pour X appartenant l'ensemble des entiers 32 bits que pour X = 5
C'est un résultat relativement inutile
Si on ne pouvait prouver que sur un seul jeu de données oui, mais comme on peut prouver sur n'importe quel jeu de données borné à partir du moment ou les variables dans les états sont elles-mêmes bornées c'est très très pratique. Comme aucun ordinateur n'a de mémoire ou de registre infini on peut démontrer au cas par cas sur n'importe quel problème. Il arrive même (approche orthogonale aux types) que l'on prouve vrai un programme qui traduit un algorihtme d'un problème indécidable par ce que l'on sait que l'on va forcément se prendre un Out of Memory ou un NaN avant de rentrer dans les cas problématiques.
Un bonne exemple de prblème indécidable qui n'empêche pas des programmes d'être prouvé est le calcul par éléments finis. Si l'utilisateur du programme sort des etats calculables, le programme lui envoie un joli message d'erreur l'invitant à revoir sa copie. Et on construit des avions parfaitement fiables avec ces trucs là...
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:
Une fois de plus le Theorème de Rice démontre que l'on ne peut pas écrire un unique programme P tel que pour tout programme source SPx on puisse avoir P(SPx) -> le programe se termine ou non ET le programme est conforme aux specs. Il ne dit absolument pas que pour un programme quelconque spécifié il est impossible d'écrire un autre programme qui le valide ou l'invalide. Et vraiment j'insiste sur le fait que si le programme (a) tourne en environnement limité il existe au moins un programme (b) qui le valide ou l'invalide (même si pour celà le programme doit tourner dans un environnement exponentiellement plus vaste que celui du programme (a))
[^] # Re: C'est trop compliqué !
Posté par Jerome Herman . En réponse au journal Des langages de haut niveau. Évalué à 1.
Ce qui m'ennuie avec cette phrase et qu'elle induit violamment en erreur. Dénombrer exhaustivement puis évaluer tous les états d'un programme n'est pas du tout équivalent avec l'execution d'un programme sur l'ensemble des jeu de données possibles à raison d'un million d'execution par jeu. Dans le second cas rien n'indique que l'on a effectivement couvert tous les états possibles. Un état particulier peut très bien ne se produire que dans certaines conditions très précises.
Par exemple si on cumule des arrondis au delà de la limite du CPU, on peut parfaitement avoir un programme qui calcule juste sur un ordinateur et faux sur celui d'à coté.
De plus il n'est pas question d'executer ici le programme, mais de valider ses etat. Celà se fait le plus souvent de façon totalement extérieure au programme. Enfin il ne s'agit pas de valider le programme pour un seul et unique jeu de données, mais pour un ensemble de données toutes bornées.
Avec la doc du CPU et du compilateur il est souvent à peine plus complexe de valider un état pour X appartenant l'ensemble des entiers 32 bits que pour X = 5
C'est un résultat relativement inutile
Si on ne pouvait prouver que sur un seul jeu de données oui, mais comme on peut prouver sur n'importe quel jeu de données borné à partir du moment ou les variables dans les états sont elles-mêmes bornées c'est très très pratique. Comme aucun ordinateur n'a de mémoire ou de registre infini on peut démontrer au cas par cas sur n'importe quel problème. Il arrive même (approche orthogonale aux types) que l'on prouve vrai un programme qui traduit un algorihtme d'un problème indécidable par ce que l'on sait que l'on va forcément se prendre un Out of Memory ou un NaN avant de rentrer dans les cas problématiques.
Un bonne exemple de prblème indécidable qui n'empêche pas des programmes d'être prouvé est le calcul par éléments finis. Si l'utilisateur du programme sort des etats calculables, le programme lui envoie un joli message d'erreur l'invitant à revoir sa copie. Et on construit des avions parfaitement fiables avec ces trucs là...
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:
Une fois de plus le Theorème de Rice démontre que l'on ne peut pas écrire un unique programme P tel que pour tout programme source SPx on puisse avoir P(SPx) -> le programe se termine ou non ET le programme est conforme aux specs. Il ne dit absolument pas que pour un programme quelconque spécifié il est impossible d'écrire un autre programme qui le valide ou l'invalide. Et vraiment j'insiste sur le fait que si le programme (a) tourne en environnement limité il existe au moins un programme (b) qui le valide ou l'invalide (même si pour celà le programme doit tourner dans un environnement exponentiellement plus vaste que celui du programme (a))