L'utilité du test unitaire

[Roworll]

Et à quoi ressemblerait ton système de preuve avec une fonction du type square() ?

[Xenos]

A un graphe je dirai, où "square()" est un noeud.
La couleur du noeud pourrait indiquer l'état de vérification de l'élément (vert = prouvé, rouge = non prouvé, orange = dépend d'éléments non prouvés). Les hypothèses seraient à éloigner du graphe (les isoler graphiquement).
Avec en plus un analyseur de code qui lirait le code utilisateur pour dire "attention, là, tu utilises square() mais tu ne respecte pas les hypothèses donc cela peut ne pas marcher", on pourrait gagner un temps fou.
Cela revient à pousser un peu plus loin les "warnings" de Eclipse.

function square($x)

{

return ($x*$x);

}

Ensuite, on "simule" cette fonction:
L'appel à square() est effectué. La machine lit $x, $x et applique *($x,$x). Elle récupère le résultat. Elle renvoie ce résultat.
L'appel à square() et la lecture de $x reposent sur le langage et sont couverts par "le langage est fiable".
*($x,$x) n'est pas applicable sur tout type de variable. En revanche, il est applicable sur tout nombre.
Donc $x doit être un nombre.
On continue: *() donne un résultat exact si et seulement si on n'a pas de débordement d'entier; dans la plupart des cas décimaux (double/float), *() sera approximative (epsilon machine).
Si je veux que square() donne le carré exact, je peux me limiter aux entiers de sorte qu'il n'y ait pas de débordement, donc +-46340.
Donc la vraie doc de square est: "square() renvoie le carré de $x, entier entre -46340 et +46340 inclus."

Il s'agit donc de dire au développeur qui utilise la fonction/méthode que celle-ci marche à coup sûr pour toute entrée dans un certain domaine donné (l'IDE peut l'aider à le visualiser automatiquement). S'il sort du domaine, bon, ben rien ne garantis que cela marchera ou foirera, mais au moins, il visualisera directement que l'appel à telle ou telle fonction/méthode est bancal et donc en cas de bug, c'est ça qui peut foirer.

[Roworll]

Et quel serait le niveau de granularité de ton truc ?
Comment le traduire en quelque chose de visualisable ?

Si j'ai une méthode qui appelle Square(), il faut aussi que je la prouve.
Si j'ai besoin de tester une classe complète qui comporte des dizaines de méthodes, comment procéder ?
Et si je veux calculer le carré de nombres décimaux, il me faut une autre fonction ?

Rien que l'assertion "le langage est fiable" est erronée. Si les langages étaient fiables, on n'aurait jamais besoin de patches ou de hotfixes. Les langages se contenteraient d'évoluer, ce qui n'est pas le cas aujourd'hui. De plus, on prend ici un simple cas mathématique mais il faut également gérer les situations qui ne se résolvent pas par le biais d'une équation (ex opération sur des tableaux, adressage mémoire, comportement d'une classe métier)

IMHO, le test unitaire est à l'heure actuelle l'un des meilleurs moyens de vérifier le comportement des briques élémentaire d'une application indépendamment les unes des autres. Il suffit de savoir comment construire des tests pertinents.

[Xenos]

La granularité adaptée me semble être la fonction (le grain élémentaire du langage).
Je ne pense pas qu'il serait visualisable dans son ensemble, humainement, mais cela me semble aussi utile que vouloir visualiser toute une base de donnée d'un bloc.
Si la fonction Square() est ajoutée, la preuve serait faite par l'outil automatisé (car oui, je redis: à la main, ça serait long ).
Si tu veux calculer un carré de décimaux, oui, il te faudra une autre fonction: soit une nouvelle, soit un upgrade de la fonction square(). Tu peux aussi simplement passer le typage de "int" vers "double", mais la fonction ne sera plus prouvée, et toutes celles qui l'utiliseront pourront voir apparaitre un bug.
Le langage évoluent, les patch et hotfix ne sont là qu'à cause de l'implémentation que l'on en fait (implémentation non prouvée justement ). Les langages sont l'objet d'études avancées dans les labos de recherche, par les bons gros matheux bien chers et rares. Toutes les situations peuvent se résoudre par équation: l'informatique, c'est des machines de Turing, des machines d'état finis. Ca s'étudie, c'est juste long. A la main, ce serait lourd, mais si c'est la machine qui le fait, c'est tout bénef'.

D'accord, je partage l'opinion que c'est pour l'instant le meilleur ratio qualité/prix pour les systèmes courants; ça n'empêche pas que j'aimerai bien pousser et réussir à ouvrir une autre voie d'étude pour le développement :p

[niahoo]

Ce que tu cherche à faire s'appelle Haskell ou dialyzer pour erlang. ça vérifie les input/output des fonctions et ça permet aussi de le faire en cas d'effets de bord.

Mais comme tu l'as dit, prouver un algorithme est différent de tester une implémentation.

Code :

function square(int x) {
    return 42
}

Donc là ton système est supposé faire comme toi, inventer des specs ou il n'y en a pas et avertir le développeur qu'ils s'est probablement trompé ... Un algorithme ce n'est pas des mathématiques, c'est plus que ça, ça témoigne d'une intention. Une machine ne peut pas deviner ce que tu veux faire. Elle peut juste faire ce que tu lui demande de faire parmi un nombre limité d'instructions.

[Xenos]

Ah, en effet... l'outil ne peut donc que assurer des valeurs acceptables, mais pas deviner l'intention derrière... hmm...

[BAK]

Je ne pense pas qu'il soit possible d'automatiser la création de preuve, tout simplement parce que l'ordi ne peut pas savoir ce que tu veut faire (et donc encore moins si tu l'as bien fait).

Ce dont tu parles maintenant n'a rien à voir avec les preuves formelles, c'est juste une vérification de type plus poussée que la plupart des IDE.
Dans mon IDE javascript, si j'essaye de passer du texte à la méthode [pre]Math.floor[/pre] par exemple, j'ai un warning qui s'affiche.
Bon, le truc est loin d'être parfait, et il fonctionne surtout à partir des tags de documentation, mais c'est déjà une grande aide qui évite pas mal d'erreurs.

Après, je dit pas qu'il n'y a rien à faire dans ce domaine, au contraire. C'est incroyable le nombre d'erreurs que l'on peut laisser dans le code et qui sont détectées par des outils d'analyse de code basique comme JSHint, et qui sont pourtant évidentes.

Pour ceux que ça intéresse, Carmack a écrit un petit article la-dessus: Static code analysis (version fr).
Sa conclusion:

It is impossible to do a true control test in software development, but I feel the success that we have had with code analysis has been clear enough that I will say plainly it is irresponsible to not use it.

EDIT:
Arf, grillé par niahoo -.-

[niahoo]

Tu peux regarder la programmation par contrat ou regarder du côté de Haskell, ça rafraîchit quand on se tape que du PHP depuis des années.

[srm]

http://fr.wikipedia.org/wiki/M%C3%A9thod...ormatique)

[Xenos]

Ok, ça marche pour moi. Merci pour les réponses, les pistes et les remarques.