Une preuve fausse n'a pas beaucoup d'intérêt.
Si, on sait qu'on peut foutre le programme à la poubelle, ou au moins le corriger pour le rendre valide.
Mais dans la plupart des cas, tu ne pourras démontrer ni l'un ni l'autre, et c'est tout le problème.
Oui mais la réponse "on sait pas" => preuve fausse. Merci de revoir votre copie messieurs les programmeurs.
Par état souhaitable, tu veux dire état dont on sait qu'il mêne au bon résultat (et à une terminaison du programme) ? Si c'est le cas, alors la détermination des états souhaitables revient à prouver le programme,
Pas tout à fait, mais c'est vrai que c'est le plus gros du boulot.
un état souhaitable est par exemple : variable d'entrée comprise entre 0 et 1, variable de sortie de type booléen contenant vrai ou faux. Après il faut encore démontrer que la variable de sortie est bien la bonne d'après les specs ie que le code de calcul est juste.
et est impossible dans le cas général par quelque chose de puissance équivalente à une machine de Turing (MT).
Dans le cas général oui.
Prouver qu'un programme termine (sur un jeu de données fixé) n'est qu'une question de temps: il suffit de l'exécuter
Euh non pas du tout. C'est pas parcequ'il s'execute une fois, qu'il le fera forcément la fois d'après même avec le même jeu de données. Tout un tas de question de concurrence et de priorité entrent en jeu. Sans même parler des problèmes liés au threads ou à l'OS sous jacent.
Prouver qu'un programme ne termine pas est une autre paire de manches.
Une fois de plus ca dépend du programme, il y a tout un tas de programmes qui ne terminent pas de façon tout à fait triviale (etats qui bouclent dans un graph par exemple)
Tu as l'air de penser qu'à partir du moment où on choisit un programme en particulier, alors il devient prouvable
A partir du moment ou on a des specs non infinies (ce qui est quand même le cas général) pour ce programme oui. Une fois de plus prouver un programme revient à répondre à deux questions :
- le programme suit-il les specs (oui/non)
- peut on assurer que le programme va se terminer (oui/non)
La réponse à la seconde question peut parfaitement être non. Des programmes comme le jeu de la vie sont de bons exemples. Les specs sont parfaitement respectées, les états des différentes fonctions sont parfaitement connus par contre dans le cas général on ne peut pas savoir si le programme va s'arréter ou non avant d'avoir vu le jeu de données initial. Si on a des specs inifinies (la grille peut avoir n'importe quelle taille, les données initiales peuvent prendre n'importe quelle valeur) on est dans la merde. Par contre si on a une grille de taille limitée par exemple il suffit de rajouter la condition "arrêt si on revient sur un des états précédents" pour être sur que le programme s'arrêtera forcément.
dans les faits il est souvent facile de rajouter des conditions jusqu'à avoir des specs finies vu que l'ordinateur sur lequel tourne le programme n'est pas inifini...
Il n'est pas possible d'écrire un programme validant la terminaison d'un autre programme quelconque
Je n'ai jamais dit celà, par contre 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...
Démonstration simple, une machine de Turing ne possédant que N états possibles. On détermine que l'etat 0 est arrêt. On a N2 transition possible d'un état à un autre (un état pouvant éventuellement boucler sur lui même, amis aucun etat ne peut une fois amener à l'état X et la fois d'après amener à l'état Y). Il y a donc au maximum N état initiaux suivi de (N-1)xN2 transition possibles soit N^4-N3 ensembles programmes+données tous parfaitement déterminés. Pour savoir si ils terminent ou non, il suffit de regarder ce quis era fait dans un temps fini (mais plutôt long quand même il faut bien l'admettre)
[^] # Re: C'est trop compliqué !
Posté par Jerome Herman . En réponse au journal Des langages de haut niveau. Évalué à 1.
Si, on sait qu'on peut foutre le programme à la poubelle, ou au moins le corriger pour le rendre valide.
Mais dans la plupart des cas, tu ne pourras démontrer ni l'un ni l'autre, et c'est tout le problème.
Oui mais la réponse "on sait pas" => preuve fausse. Merci de revoir votre copie messieurs les programmeurs.
Par état souhaitable, tu veux dire état dont on sait qu'il mêne au bon résultat (et à une terminaison du programme) ? Si c'est le cas, alors la détermination des états souhaitables revient à prouver le programme,
Pas tout à fait, mais c'est vrai que c'est le plus gros du boulot.
un état souhaitable est par exemple : variable d'entrée comprise entre 0 et 1, variable de sortie de type booléen contenant vrai ou faux. Après il faut encore démontrer que la variable de sortie est bien la bonne d'après les specs ie que le code de calcul est juste.
et est impossible dans le cas général par quelque chose de puissance équivalente à une machine de Turing (MT).
Dans le cas général oui.
Prouver qu'un programme termine (sur un jeu de données fixé) n'est qu'une question de temps: il suffit de l'exécuter
Euh non pas du tout. C'est pas parcequ'il s'execute une fois, qu'il le fera forcément la fois d'après même avec le même jeu de données. Tout un tas de question de concurrence et de priorité entrent en jeu. Sans même parler des problèmes liés au threads ou à l'OS sous jacent.
Prouver qu'un programme ne termine pas est une autre paire de manches.
Une fois de plus ca dépend du programme, il y a tout un tas de programmes qui ne terminent pas de façon tout à fait triviale (etats qui bouclent dans un graph par exemple)
Tu as l'air de penser qu'à partir du moment où on choisit un programme en particulier, alors il devient prouvable
A partir du moment ou on a des specs non infinies (ce qui est quand même le cas général) pour ce programme oui. Une fois de plus prouver un programme revient à répondre à deux questions :
- le programme suit-il les specs (oui/non)
- peut on assurer que le programme va se terminer (oui/non)
La réponse à la seconde question peut parfaitement être non. Des programmes comme le jeu de la vie sont de bons exemples. Les specs sont parfaitement respectées, les états des différentes fonctions sont parfaitement connus par contre dans le cas général on ne peut pas savoir si le programme va s'arréter ou non avant d'avoir vu le jeu de données initial. Si on a des specs inifinies (la grille peut avoir n'importe quelle taille, les données initiales peuvent prendre n'importe quelle valeur) on est dans la merde. Par contre si on a une grille de taille limitée par exemple il suffit de rajouter la condition "arrêt si on revient sur un des états précédents" pour être sur que le programme s'arrêtera forcément.
dans les faits il est souvent facile de rajouter des conditions jusqu'à avoir des specs finies vu que l'ordinateur sur lequel tourne le programme n'est pas inifini...
Il n'est pas possible d'écrire un programme validant la terminaison d'un autre programme quelconque
Je n'ai jamais dit celà, par contre 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...
Démonstration simple, une machine de Turing ne possédant que N états possibles. On détermine que l'etat 0 est arrêt. On a N2 transition possible d'un état à un autre (un état pouvant éventuellement boucler sur lui même, amis aucun etat ne peut une fois amener à l'état X et la fois d'après amener à l'état Y). Il y a donc au maximum N état initiaux suivi de (N-1)xN2 transition possibles soit N^4-N3 ensembles programmes+données tous parfaitement déterminés. Pour savoir si ils terminent ou non, il suffit de regarder ce quis era fait dans un temps fini (mais plutôt long quand même il faut bien l'admettre)