On garantie que le programme est conforme aux spécifications. Il faut que les spécifications soient correctes, mais ça, aucun programme ne peut les vérifier ; c'est le boulot des humains.
Mais si dans la spécification d'une fonction il y a marqué qu'elle retourne A, alors un code qui la fait renvoyer Q est incorrect. Si dans sa spécification il y a marqué qu'elle retourne quelque chose du même type que A ou Q, alors la spécification n'est pas assez précise. Bref, dans ta specs tu aura les contraintes sur l'objet retourné, contraintes que satisferont A mais pas Q.
Par exemple, différentes spécification pour la fonction factorielle :
* fact :: int -> int alors fact = \x :: int -> -42 * x est une implémentation correcte
* fact :: uint -> uint est un peu mieux typé, mais il est toujours possible de mal l'implémenté.
* fact :: {a::uint} -> {b::uint et pour tout x entre 1 et a, x divise b} est un peu plus précis, mais toujours pas assez. Une implémentation correcte de cette spécification peut aussi bien retourner a! que a×ばつa! ou le produit des nombres premiers entre 1 et a + 42.
* fact :: {a::uint} -> {b::uint et b = produit sur uint de 1 à a} ça c'est la définition de la fonction factorielle, une implémentation sera correcte.
* fact :: {a::uint} -> {b::uint tel que b est le nombre de permutations possibles d'une liste de a objets distincs} est correcte aussi.
[^] # Re: Implémentation prouvée
Posté par Zylabon . En réponse au journal OpenSSL est mort, vive (le futur) LibreSSL. Évalué à 6. Dernière modification le 22 avril 2014 à 15:51.
On garantie que le programme est conforme aux spécifications. Il faut que les spécifications soient correctes, mais ça, aucun programme ne peut les vérifier ; c'est le boulot des humains.
Mais si dans la spécification d'une fonction il y a marqué qu'elle retourne A, alors un code qui la fait renvoyer Q est incorrect. Si dans sa spécification il y a marqué qu'elle retourne quelque chose du même type que A ou Q, alors la spécification n'est pas assez précise. Bref, dans ta specs tu aura les contraintes sur l'objet retourné, contraintes que satisferont A mais pas Q.
Par exemple, différentes spécification pour la fonction factorielle :
*
fact :: int -> intalorsfact = \x :: int -> -42 * xest une implémentation correcte*
fact :: uint -> uintest un peu mieux typé, mais il est toujours possible de mal l'implémenté.*
fact :: {a::uint} -> {b::uint et pour tout x entre 1 et a, x divise b}est un peu plus précis, mais toujours pas assez. Une implémentation correcte de cette spécification peut aussi bien retourner a! que a×ばつa! ou le produit des nombres premiers entre 1 et a + 42.*
fact :: {a::uint} -> {b::uint et b = produit sur uint de 1 à a}ça c'est la définition de la fonction factorielle, une implémentation sera correcte.*
fact :: {a::uint} -> {b::uint tel que b est le nombre de permutations possibles d'une liste de a objets distincs}est correcte aussi.Please do not feed the trolls