27-08-2013, 02:40 PM
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.
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.
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);
}
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.