>>et par extension de déterminer si ce programme est conforme à sa spécification
>Il faut encore savoir ce qu'est une spec
D'après le théorème de Kleene, il n'existe pas d'algorithme capable de prouver qu'un algorithme vérifie une propriété non triviale.
Il n'y a pas à tortiller, si la "spec" est "le programme termine sur l'entrée 16 en temps 64", c'est trivial, si c'est "le programme calcule factorielle", c'est indécidable. Les specs que tu veux vérifier, c'est parce qu'elles sont non triviales, donc quoi qu'il arrive, tu auras des cas où ton programme se gourrera ou juste ne répondra pas, même si la spec est parfaitement claire.
> Dans le cas général.
Il y a heureusement des cas où un humain ou un programme est capable de prouver qu'un programme vérifie une propriété, mais ce sont juste des cas particuliers ;)
[^] # Re: prouveur automatique/assistant de preuve
Posté par 태 (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 5.
>Il faut encore savoir ce qu'est une spec
D'après le théorème de Kleene, il n'existe pas d'algorithme capable de prouver qu'un algorithme vérifie une propriété non triviale.
Il n'y a pas à tortiller, si la "spec" est "le programme termine sur l'entrée 16 en temps 64", c'est trivial, si c'est "le programme calcule factorielle", c'est indécidable. Les specs que tu veux vérifier, c'est parce qu'elles sont non triviales, donc quoi qu'il arrive, tu auras des cas où ton programme se gourrera ou juste ne répondra pas, même si la spec est parfaitement claire.
> Dans le cas général.
Il y a heureusement des cas où un humain ou un programme est capable de prouver qu'un programme vérifie une propriété, mais ce sont juste des cas particuliers ;)