Tu parles quand même dans un cadre très général bien loin des cas pratiques.
- de déterminer si ce programme fait la même chose qu'un autre programme
Dans le cas général.
Parce que c'est justement dans ce domaine là que les prouveurs formelles sont utilisés industriellement à grande échelle. On appelle cela les "equivalence checker". C'est un outil du domaine de l'EDA qui permet de s'assurer qu'une mer de portes générées par un synthétiseur est équivalent au code source HDL.
- et par extension de déterminer si ce programme est conforme à sa spécification
Il faut encore savoir ce qu'est une spec. Souvent, c'est super flou et pas clair. Le client veut que le produit réponde à son problème et ne plante pas, par contre, il ne sait pas forcément bien le définir. C'est plus un problème d'ingénierie logiciel que de preuves mathématiques.
[^] # Re: prouveur automatique/assistant de preuve
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
- de déterminer si ce programme fait la même chose qu'un autre programme
Dans le cas général.
Parce que c'est justement dans ce domaine là que les prouveurs formelles sont utilisés industriellement à grande échelle. On appelle cela les "equivalence checker". C'est un outil du domaine de l'EDA qui permet de s'assurer qu'une mer de portes générées par un synthétiseur est équivalent au code source HDL.
- et par extension de déterminer si ce programme est conforme à sa spécification
Il faut encore savoir ce qu'est une spec. Souvent, c'est super flou et pas clair. Le client veut que le produit réponde à son problème et ne plante pas, par contre, il ne sait pas forcément bien le définir. C'est plus un problème d'ingénierie logiciel que de preuves mathématiques.
"La première sécurité est la liberté"