Annotation automatique
Par David Monniaux le lundi, août 1 2011, 20:07 - Programmation - Lien permanent
J'aurais une petite question pour ceux de mes lecteurs qui programment.
Trouveriez-vous utile d'avoir un outil qui, en lisant un programme (disons dans un langage comme C/C++/Fortran, voire C#/Java), vous fournisse pour chaque procédure des conditions raisonnables d'utilisation, par exemple garantissant l'absence de comportements arithmétiques indéfinis, la terminaison de la fonction, voire l'absence d'erreurs de pointeurs ? (du style : p!=NULL && n > 0 && i < n)
Avez-vous des suggestions sur ce que vous aimeriez en la matière ?
Commentaires
Si on le voit comme un outil de documentation des procédures alors oui c'est utile :)
Quid des faux positifs? Est ce envisageable de convertir ces commentaires en assert?
Pour la terminaison, je ne m'attends pas à des miracles....
Est-ce qu'on peut ajouter SPARK à la liste des langages dans la liste ? Ou est-ce les utilisateurs de SPARK sont exclus car déjà convertis ? ;-)
Franchement, oui, ce serait extrêmement désirable. Avec des explications sur pourquoi ces conditions, ce serait tout simplement formidable.
Iil y déjà quelques outils comme findbugs ou l'analyseur statique de clang qui font des rapports sympa, mais qui s'arrêtent aux erreurs « évidentes » et ne permettent pas d'établir de contrats pour se prémunir d'erreurs à l'utilisation.
PS : ce sont principalement C++, D et Java qui m'intéressent ;-)
Tu comptes faire un tel outil ?
Sans vouloir faire de la pub ;-) il y a tout ce qu'il faut pour faire ça pour le langage C dans l'outil Frama-C (http://frama-c.com/)...
Frama-C a les bases pour construire un tel outil, mais n'offre pas actuellement cette fonctionnalité, je suppose ? Il faut faire de l'analyse statique pour y arriver...
Genre, sous formes d'assert pour C, je suppose ? Parce que si c'est systematiquement evalue, ca va pas le faire cote perfs...
> Frama-C a les bases pour construire un tel outil,
> mais n'offre pas actuellement cette fonctionnalité,
> je suppose ?
Pour le genre de propriétés que tu dis, c'est plutôt l'inférence automatique de préconditions, (une des activités) de Yannick Moy pendant sa thèse, disponible depuis des lustres dans Jessie à condition d'avoir Apron. http://hal.inria.fr/inria-00534331/...
Maintenant, puisque Natacha mentionne SPARK, les dépendances fonctionnelles ("derives" en Spark), c'est super, les programmeurs comprennent ce que ça veut dire, ça peut même faire partie des spécifications qu'ils ont å vérifier, ... Bref, une version de ces dépendances fonctionnelles est calculée automatiquement en Frama-C à partir des résultats de l'analyse de valeurs, avec l'option -deps.
@David : Je ne suis pas sure de comprendre ce que tu entends par :
> Il faut faire de l'analyse statique pour y arriver...
car à mon sens, Frama-C fait (entre autres) de l'analyse statique justement... Mais les "conditions raisonnables d'utilisation" dont tu parles sont générées localement au niveau des instructions douteuses. Il reste à utiliser le greffon WP si on veut les remonter sous forme de préconditions de fonction.
@Anne: Le WP ça fonctionne bien tant que tu n'as pas de boucle, mais si tu as une boucle il faut remonter ça à travers l'invariant...
de plus, à ma connaissance, pour l'instant, il n'y a qu'un calcul d'invariants intervalles, non ?
@lagon:
Je n'ai pas l'impression qu'il n'y ait qu'un calcul d'invariant d'intervalles dans http://hal.inria.fr/inria-00534331/... . Mais je n'y connais rien. Tu as regardé ?
Les invariants calculés pendant que les dépendances fonctionnelles sont inférées, je m'y connais un peu mieux et ce ne sont pas des intervalles non plus.
En fait, le probleme des pre-cond/post-cond, c'est que c'est tres rarement simple de savoir si on doit juste les documenter, ou les mettre dans le code.
Ca peut se decider au cas par cas manuellement, bien sur, mais des que le code devient un peu gros, c'est plus du tout simple.
Si on doit mettre des verifications dans chaque fonction, par exemple, ca peut conduire a des perversions, comme ecrire deliberement des fonctions un peu trop longues pour limiter le cout a l'execution...