Nan, je voulais dire qu'il me semble malvenu de vouloir faire les tests sans tenir compte du code source de la fonction, en dehors de toute considération du code source.
Je ne vois pas en quoi l'écriture sur un disque ou l'ouverture d'un socket ne pourrait pas être prouvée. Si les fonction utilisées dans le code courant sont prouvées, alors il suffit de prouver le code courant, ce qui est faisable.
La preuve de ton exemple est bien mathématique (en supposant que le langage lui-même soit fiable):
set() assigne à x la valeur passée en paramètre, et plus() retourne le résultat de l'opérateur + sur la valeur de x et sur l'argument y.
Ma preuve mathématique va te dire:
C'est un biais cognitif que de se dire "plus() renvoie y+x" (faut pas faire de la traduction mot-à-mot du code source).
Si je veux que "set() assigne un nombre x à this.x", alors il faut que je change ma méthode set(): elle ne respecte pas la spécification.
Si ma spécification dit "plus() doit ajouter le nombre entier y à this.x (définit comme nombre entier aussi, plus haut dans la spec)", alors mon implémentation de plus() n'est pas correcte. Si jamais set() était codée correctement, avec un typage set(int x), alors je pourrai dire "je sais que this.x est un entier quelconque", et j'affine un peu ma preuve sur plus() ("plus() renvoie le résultat de l'opérateur + appliqué à x entier et à y quelconque).
D'ailleurs, je ne comprends pas bien l'exemple car justement, les trois tests que tu as effectués sont validés, mais la fonction plus() ne réalise pas ce que la spécification lui demandait (ajouter deux entiers).
Y'a un coté cygne noir à la preuve par les tests unitaires: on ne prouve pas que la méthode marche dans l'absolu, on prouve juste qu'il y a quelques cas où ça marche.
La preuve "mathématique", formelle, ou brutale si on veut, va elle prouver que le code marche bel et bien quelque soit le cas envisageable.
L'approche par le test me semble malsaine comme dans cet exemple car les tests passent, mais "plus tard", ça va te tomber dans le coin de la figure, et c'est généralement là que démarrent les bidouillages et arrangements boiteux qui finissent par massacrer un projet (non?).
Ok, le test qui couvre 100% du possible me semble... impossible aussi XD Mais la preuve qui couvre 100% du possible, elle est possible justement (avec quelques axiomes quand même, tu type "l'ordinateur sait compter" ou "le langage est fiable").
Je ne vois pas en quoi l'écriture sur un disque ou l'ouverture d'un socket ne pourrait pas être prouvée. Si les fonction utilisées dans le code courant sont prouvées, alors il suffit de prouver le code courant, ce qui est faisable.
La preuve de ton exemple est bien mathématique (en supposant que le langage lui-même soit fiable):
set() assigne à x la valeur passée en paramètre, et plus() retourne le résultat de l'opérateur + sur la valeur de x et sur l'argument y.
Ma preuve mathématique va te dire:
Citation :Quelque soit x, set(x) assigne x à l'attribut this.x.
Queque soit y, plus(y) retourne le résultat de l'opérateur + appliqué sur x, quelconque par définition, et y, quelconque aussi.
C'est un biais cognitif que de se dire "plus() renvoie y+x" (faut pas faire de la traduction mot-à-mot du code source).
Si je veux que "set() assigne un nombre x à this.x", alors il faut que je change ma méthode set(): elle ne respecte pas la spécification.
Si ma spécification dit "plus() doit ajouter le nombre entier y à this.x (définit comme nombre entier aussi, plus haut dans la spec)", alors mon implémentation de plus() n'est pas correcte. Si jamais set() était codée correctement, avec un typage set(int x), alors je pourrai dire "je sais que this.x est un entier quelconque", et j'affine un peu ma preuve sur plus() ("plus() renvoie le résultat de l'opérateur + appliqué à x entier et à y quelconque).
D'ailleurs, je ne comprends pas bien l'exemple car justement, les trois tests que tu as effectués sont validés, mais la fonction plus() ne réalise pas ce que la spécification lui demandait (ajouter deux entiers).
Y'a un coté cygne noir à la preuve par les tests unitaires: on ne prouve pas que la méthode marche dans l'absolu, on prouve juste qu'il y a quelques cas où ça marche.
La preuve "mathématique", formelle, ou brutale si on veut, va elle prouver que le code marche bel et bien quelque soit le cas envisageable.
Citation :Mais voilà, suite à un bug identifié plus tard dans la chaine de validation, je m'aperçois que 8 * 4 ne donne pas 32 mais 3Avec une approche par la preuve formelle, tu l'aurais vu avant qu'il n'arrive, car dans ta preuve mathématique (oui, à condition de savoir faire de la vraie logique et pas de la mélasse), tu aurais vu apparaitre un "limité à l'intervalle 0..9" (typique du débordement d'entier).
L'approche par le test me semble malsaine comme dans cet exemple car les tests passent, mais "plus tard", ça va te tomber dans le coin de la figure, et c'est généralement là que démarrent les bidouillages et arrangements boiteux qui finissent par massacrer un projet (non?).
Ok, le test qui couvre 100% du possible me semble... impossible aussi XD Mais la preuve qui couvre 100% du possible, elle est possible justement (avec quelques axiomes quand même, tu type "l'ordinateur sait compter" ou "le langage est fiable").