> Sauf que ta spec ne dira pas ça. Il dira factoriel selon l'algo bidule précis à 10^-14 en code double flottant.
> 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é).
Tu sais que factorielle est une fonction à valeurs entières ? Il n'y a même pas d'erreur sur les entiers... Alors faire des développements limités pour prouver sa validité...
> 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 ton programme ne répond pas en 3 jours pour MAX_INT, tu en déduis qu'il ne calcule pas factorielle ? Parce que, seulement 7 tests, pourquoi pas, mais si tu ne prouves pas que chaque test termine, ça ne rend pas le problème suffisamment trivial pour être décidable.
[^] # 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é à 2.
> 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é).
Tu sais que factorielle est une fonction à valeurs entières ? Il n'y a même pas d'erreur sur les entiers... Alors faire des développements limités pour prouver sa validité...
> 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 ton programme ne répond pas en 3 jours pour MAX_INT, tu en déduis qu'il ne calcule pas factorielle ? Parce que, seulement 7 tests, pourquoi pas, mais si tu ne prouves pas que chaque test termine, ça ne rend pas le problème suffisamment trivial pour être décidable.