Peut-être faudrait-il préciser ce qu'on entend par "prouver", parce que pour moi, même prouver qu'un programme s'arrête, c'est balaise
C'est faire un algorithme capable de vérifier si un programme s'arrête ou non qui est balèze. Prouver qu'un programme s'arrête peut être très simple.
Par exemple le programme composé de la seule instruction exit(0); s'arrête de façon triviale. Pour les programmes plus complexes ca se résoud à coup de théorie des graphs, de validations algorithmiques et/ou de calculabilité.
Certaines méthodes sont plus faciles à prouver que d'autre. L'approche récursive par exemple est très facile à prouver. Prouver un programme revient à regarder l'ensemble des états qu'il peut traverser (éventuellement l'ensemble des états que chacune de ses fonctions peut traverser) et à vérifier pour chaque état ou pour chaque ensemble d'état que l'état suivant est bien valide.
[^] # Re: C'est trop compliqué !
Posté par Jerome Herman . En réponse au journal Des langages de haut niveau. Évalué à 1.
C'est faire un algorithme capable de vérifier si un programme s'arrête ou non qui est balèze. Prouver qu'un programme s'arrête peut être très simple.
Par exemple le programme composé de la seule instruction exit(0); s'arrête de façon triviale. Pour les programmes plus complexes ca se résoud à coup de théorie des graphs, de validations algorithmiques et/ou de calculabilité.
Certaines méthodes sont plus faciles à prouver que d'autre. L'approche récursive par exemple est très facile à prouver. Prouver un programme revient à regarder l'ensemble des états qu'il peut traverser (éventuellement l'ensemble des états que chacune de ses fonctions peut traverser) et à vérifier pour chaque état ou pour chaque ensemble d'état que l'état suivant est bien valide.