VERIFICATION STATIQUE ET EXTREME PROGRAMMING

Christophe Baillon de la société SOGILIS (http://sogilis.com/) m'a transféré la publication Static Verification and Extreme Programming (www.praxis-his.com/pdfs/svandxp.pdf). L'article parle notamment de l'étonnante cohabitation entre le développement de logiciels critiques et la pratique de XP.

Christophe a bien vu de me faire connaitre cette publication. En effet, cet article m'intéresse à plusieurs égards. D'abord, je développe en équipe des applications très critiques tout en appliquant une forme adaptée de l'eXtreme-Programming. Aussi, j'ai publié un article sur la criticité et XP (Agilité et Avionique) et j'ai présenté une conférence sur ce thème aux XP Days 2008 et à l'Agile Tour Grenoble 2008 (Agilité et Avionique). Enfin, lors de ma session à Grenoble, Bruno Orsier m'a interroge sur notre éventuelle utilisation des outils de vérification statique. J'aurais mieux fait de lire l'article transmis par Christophe bien avant pour mieux répondre à Bruno!

J'écris ce billet pour réagir à certaines affirmations de l'article.

Tout d'abord, l'auteur explique qu'un outil de vérification statique est en partie assimilable à un relecteur dans la pratique du pair-programming. En effet, un tel outil saura efficacement déceler certaines erreurs mieux et plus rapidement qu'un humain. Néanmoins, cette comparaison me semble se fonder sur une vision très réductrice du binômage. En effet, en plus d'une relecture en continue, la pratique du pair-programming offre un moyen efficace d'assurer la propriété collective du code et permet d'homogéneiser la conception et le code au delà des règles de nommage et de constructions élémentaires. Aussi et surtout, la conception et le code convergent vers un bon produit grâce à la confrontion de deux points de vues (et même plus, puisque le binômes permutent).

Ensuite, l'auteur montre que la vérification formelle permet de détecter des régressions introduites lors d'un remaniement. L'exemple donné est très proche d'une utilisation de la programmation par contrat, mais non compilable. Fort heureusement, depuis la sortie de l'article, AdaCore (http://www.adacore.com/home/) nous a gratifié d'un compilateur Ada2005 incluant un sous ensemble très efficace d'une véritable programmation par contrat (pré-conditions et post-conditions compilées et exercées à l'exécution). Cette nouvelle manière d'utiliser Ada n'exige même pas d'employer un sous-ensemble du langage comme la vérification statique de SPARK l'impose. Bref, la vérification formelle est sûrement un outil puissant, mais un peu moins lorsque la programmation par contrat est pratiquée.

De plus, je pense que l'auteur a tord de suggérer d'éviter de remanier pour les cas ou cela dégraderait la couverture structurelle du code par les tests. Sur nos projets nous remanions sans retenue car l'analyse de la couverture du code par les tests est automatisée dans le build complet activé par l'intégration continue. Les branches non pertinentes sont systématiquement éliminées par les développeurs ou alors les tests sont complétés. Ces pratiques permettent au code de rester malléable.

Enfin, l'auteur regrette de ne pouvoir disposer d'un client sur site. Je pense qu'il s'arrête à une vision dogmatique d'XP. Certes, l'organisation optimale prévoit un client sur site. Sur nos projets, nous n'y arrivons pas, cependant nous travaillons systématiquement avec des représentants internes du client. Il faut savoir adapter XP à son contexte sans trahir les valeurs et les principes de la démarche.

Je remercie Christophe car il m'a donné certains augments pour défendre la pratique d'XP en milieu critique. Il m'a semblé que cet article a surtout été écrit par des vendeurs d'outils qui cherchent à promouvoir leur solution dans un milieu prometteur qui n'y porte que peu d'attention. Un logiciel critique doit s'exécuter de manière sûr. je crois que je préfère porter l'effort de vérification lors de son exécution plutôt que sur une démonstration statique.

Working software is the primary measure of progress.