J'ai pas de recette pour faire en sorte qu'à partir d'une spécification on puisse trouver le code qui marche bien: y'a besoin d'un code source pour prouver que ce code source est valide quelque soit les entrées qu'on voulait lui passer.
Mais si je prends le javascript, par exemple:
Après, faut prouver que ce code marche (pas facile en javascript, surtout sans typage). Je peux considérer que le langage est fiable, aka que appendChild fait bien ce que la documentation me dit.
Elle me dit que parentNode/childNode doit être un element DOM, donc, il faut soit que cette hypothèse reste et figure dans ma documentation de "addToDOM()", soit prendre en compte dans l'implémentation le cas où ces entrées ne sont pas du bon type.
La documentation ne précise pas de limite sur la quantité d'enfants d'un noeud parent (c'est une lacune à mon sens), donc là... C'est un "?" qui va trainer. Soit faut se le rattapper dans le code, soit faut étoffer la documentation originale, soit il faut fixer une limite "arbitraire", et tester tous les cas. Idem pour le nombre total de noeuds dans la page.
j'ai modifié le code, je refait ma preuve: si je suppose que isDOMNode() a déjà été prouvée (elle renvoie "true" si et seulement si je lui passe un DOMNode) alors il me faut encore prouver la validité du throw. S'il est prouvé comme "fiable", alors addToDOM() est fiable.
Oui, c'est clair que c'est assez "lourd", mais je le redis: c'est un investissement car je sais que cette fonction marchera toujours (tant que les hypothèses sur le langage n'auront pas été modifiées en tous cas).
Note que la méthode peut avoir d'autres "entrées" que celles explicites:
Mais si je prends le javascript, par exemple:
function addToDOM(parentNode, childNode)
{
parentNode.appendChild(childNode);
}
Après, faut prouver que ce code marche (pas facile en javascript, surtout sans typage). Je peux considérer que le langage est fiable, aka que appendChild fait bien ce que la documentation me dit.
Elle me dit que parentNode/childNode doit être un element DOM, donc, il faut soit que cette hypothèse reste et figure dans ma documentation de "addToDOM()", soit prendre en compte dans l'implémentation le cas où ces entrées ne sont pas du bon type.
La documentation ne précise pas de limite sur la quantité d'enfants d'un noeud parent (c'est une lacune à mon sens), donc là... C'est un "?" qui va trainer. Soit faut se le rattapper dans le code, soit faut étoffer la documentation originale, soit il faut fixer une limite "arbitraire", et tester tous les cas. Idem pour le nombre total de noeuds dans la page.
/*
* Ajoute childNode à parentNode si les deux sont des DOM Nodes
*/
function addToDOM(parentNode, childNode)
{
parentNode.appendChild(childNode);
}
ou
/*
* ajoute childNode à parentNode si possible, renvoie une exception si non.
*/
function addToDOM(parentNode, childNode)
{
if (!isDOMNode(parentNode))
throw new IsNotNodeException(parentNode);
if (!isDOMNode(childNode))
throw new IsNotNodeException(childNode);
parentNode.appendChild(childNode);
}
j'ai modifié le code, je refait ma preuve: si je suppose que isDOMNode() a déjà été prouvée (elle renvoie "true" si et seulement si je lui passe un DOMNode) alors il me faut encore prouver la validité du throw. S'il est prouvé comme "fiable", alors addToDOM() est fiable.
Oui, c'est clair que c'est assez "lourd", mais je le redis: c'est un investissement car je sais que cette fonction marchera toujours (tant que les hypothèses sur le langage n'auront pas été modifiées en tous cas).
Note que la méthode peut avoir d'autres "entrées" que celles explicites:
Code PHP :
<?php
class
{
private $value=0;
public function increment($x)
{
if (!is_int($x))
throw new NotAnIntegerException($x);
$this->value += $x;
}
}
$this->value est à considérer comme une "entrée" de "increment()". Je devrais donc plutôt parler "d'états" que "d'entrées" d'ailleurs.
Je ne sais pas s'il y a des outils pour ce genre de preuve d'ailleurs, il faudra que je cherche.
Pour le binôme, on inverse "testeur" et "implémenteur" pour éviter justement de se faire chier :p
La difficulté réside dans le fait que, si a() utilise b(), on ne peut pas prouver a() sans avoir déjà prouvé b()...