Si tu confirmes que dans ce que tu appelles "prouver le code", on peut inclure "prouver que le programme se termine",
La preuve n'est pas forcément vraie. Prouver qu'un programme se termine ne veut pas dire démontrer qu'un programme se termine. Quand on prouve un code on peut prouver qu'il est vrai OU qu'il est faux...
Quand on prouve un programme on cherche à savoir si oui ou non il fait ce qui est marqué sur la fiche de specs. C'est cette information supplémentaire qui permet de faire la preuve.
On ne peut pas écrire un programme qui valide la terminaison ou non de tous les autres programmes car il est impossible de spécifier à priori l'ensemble de toutes les specs de tous les programmes. Par contre sur un programme donné, dont on connait par avance les specs et les états souhaitables il est possible (même programmatiquement) de voir
a) Si on ne rencontre effectivement que des états souhaitables
b) Si on termine le programme.
Avant d'arriver au b) il faut d'abord valider le a) sinon on se retrouve avec un programme dont on ne connait pas les specs et de fait on est bien en peine de démontrer si il va boucler ou non vu que son comportement n'est plus formalisé. Par contre une fois que l'on a le a) et donc un nombre d'état possible limité, prouver le b) n'est qu'une question de temps.
[^] # Re: C'est trop compliqué !
Posté par Jerome Herman . En réponse au journal Des langages de haut niveau. Évalué à 1.
La preuve n'est pas forcément vraie. Prouver qu'un programme se termine ne veut pas dire démontrer qu'un programme se termine. Quand on prouve un code on peut prouver qu'il est vrai OU qu'il est faux...
Quand on prouve un programme on cherche à savoir si oui ou non il fait ce qui est marqué sur la fiche de specs. C'est cette information supplémentaire qui permet de faire la preuve.
On ne peut pas écrire un programme qui valide la terminaison ou non de tous les autres programmes car il est impossible de spécifier à priori l'ensemble de toutes les specs de tous les programmes. Par contre sur un programme donné, dont on connait par avance les specs et les états souhaitables il est possible (même programmatiquement) de voir
a) Si on ne rencontre effectivement que des états souhaitables
b) Si on termine le programme.
Avant d'arriver au b) il faut d'abord valider le a) sinon on se retrouve avec un programme dont on ne connait pas les specs et de fait on est bien en peine de démontrer si il va boucler ou non vu que son comportement n'est plus formalisé. Par contre une fois que l'on a le a) et donc un nombre d'état possible limité, prouver le b) n'est qu'une question de temps.