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,
Non, c'est aussi parce que le programme est gros.
Tu veux vérifier que tu ne t'es pas planté dans la copie d'une équation, dans la recopie d'une constante, que tu n'as pas de cas ou tu core dump.
"le programme calcule factorielle"
Sauf que ta spec ne dira pas ça. Il dira factoriel selon l'algo bidule précis à 10^-14 en code double flottant. De toute façon, je vois mal factoriel comme étant une fonction de base de ton logiciel de preuve.
La "preuve" sera l'équivalence à x^-14 prêt entre l'équation mathématique de la spec et ton code (souvent des développements limité).
Mais pour le cas de factoriel, le test tel que définit par la DO-178B demande de couvrir les classes d'équivalences, ce qui va se réduire à tester un nombre négatif, zéro, un nombre positif, voir les nombres max et min du range spécifié, et le range+1 pour voir que cela ne plante pas. 7 tests en tout pour vérifier l'équivalence à 10^-14 prêt et pour avoir la certif de ton avion.
Si tu fais quelques milliers de test en random() en plus, c'est encore mieux (mais la certif s'en fout). Les partitions par classe d'équivalence fonctionnent en test boite blanche quand tu connais la tête du code et que tu voix bien qu'il n'y a pas de branchement. De toute façon, à l'exécution du test, tu vérifies la couverture de code.
Certe tu n'auras pas prouver l'équivalence entre spec et code mais tu auras une grande confiance, ce qui est le principale.
[^] # 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é à 1.
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,
Non, c'est aussi parce que le programme est gros.
Tu veux vérifier que tu ne t'es pas planté dans la copie d'une équation, dans la recopie d'une constante, que tu n'as pas de cas ou tu core dump.
"le programme calcule factorielle"
Sauf que ta spec ne dira pas ça. Il dira factoriel selon l'algo bidule précis à 10^-14 en code double flottant. De toute façon, je vois mal factoriel comme étant une fonction de base de ton logiciel de preuve.
La "preuve" sera l'équivalence à x^-14 prêt entre l'équation mathématique de la spec et ton code (souvent des développements limité).
Mais pour le cas de factoriel, le test tel que définit par la DO-178B demande de couvrir les classes d'équivalences, ce qui va se réduire à tester un nombre négatif, zéro, un nombre positif, voir les nombres max et min du range spécifié, et le range+1 pour voir que cela ne plante pas. 7 tests en tout pour vérifier l'équivalence à 10^-14 prêt et pour avoir la certif de ton avion.
Si tu fais quelques milliers de test en random() en plus, c'est encore mieux (mais la certif s'en fout). Les partitions par classe d'équivalence fonctionnent en test boite blanche quand tu connais la tête du code et que tu voix bien qu'il n'y a pas de branchement. De toute façon, à l'exécution du test, tu vérifies la couverture de code.
Certe tu n'auras pas prouver l'équivalence entre spec et code mais tu auras une grande confiance, ce qui est le principale.
"La première sécurité est la liberté"