27-08-2013, 04:16 PM
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:
EDIT:
Arf, grillé par niahoo -.-
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:
Carmack a écrit :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 -.-