Mechanized verification of the correctness and asymptotic complexity of programs : the right answer at the right time

Vérification mécanisée de la correction et complexité asymptotique de programmes Cette thèse s’intéresse à la question de démontrer rigoureusement que l’implantation d’un algorithme donné est non seulement correcte (elle renvoie bien le bon résultat dans tous les cas possibles), mais aussi possède la bonne complexité asymptotique (elle calcule toujours ce résultat en le temps attendu).Pour les chercheurs en algorithmique, caractériser la performance d’un algorithme se fait généralement en indiquant sa complexité asymptotique, notamment à l’aide de la notation “grand O” due à Landau. Nous détaillons, tout d’abord informellement, pourquoi de telles bornes de complexité asymptotiques sont également utiles en tant que spécifications formelles. La raison est que celles-ci permettent de raisonner de façon modulaire à propos du coût d’un programme : une borne en O s’abstrait de l’expression exacte du coût du programme, et par là des divers détails d’implantation. Par ailleurs, nous illustrons, à l’aide d’exemples simples, un certain nombre de difficultés liées à l’utilisation rigoureuse de la notation O, et qu’il est facile de négliger lors d’un raisonnement informel.Ces considérations sont mises en pratique en formalisant d’une part la notation O dans l’assistant de preuve Coq, et d’autre part en étendant CFML, un outil existant dédié à la vérification de programmes, afin de permettre à l’utilisateur d’élaborer des démonstrations robustes et modulaires établissant des bornes de complexité asymptotiques. Nous étendons la logique de séparation avec crédits temps—qui permet de raisonner à la fois sur des propriétés de correction et de complexité en temps—avec la notion de crédits temps négatifs. Ces derniers augmentent l’expressivité de la logique, donnent accès à des principes de raisonnement commodes et permettent d’exprimer certaines spécifications de manière plus élégante. Au niveau des spécifications, nous montrons comment des bornes de complexité asymptotique avec O s’expriment en logique de séparation avec crédits temps. Afin d’être capable d’établir de telles spécifications, nous développons une méthodologie qui permet à l’utilisateur de développer des démonstrations qui soient à la fois robustes et menées à un niveau d’abstraction satisfaisant. Celle-ci s’appuie sur deux principes clefs : d’une part, un mécanisme permettant de collecter et remettre à plus tard certaines contraintes durant une démonstration interactive, et par ailleurs, un mécanisme permettant de synthétiser semi-automatiquement une expression de coût, et ce sans perte de généralité.Nous démontrons l’utilité et l’efficacité de notre approche en nous attaquant à un certain nombre d’études de cas. Celles-ci comprennent des algorithmes dont l’analyse de complexité est relativement simple (par exemple, une recherche dichotomique, déjà hors de portée de la plupart des approches automatisées) et des structures de données (comme les “binary random access lists” d’Okasaki). Dans notre étude de cas la plus significative, nous établissons la correction et la complexité asymptotique d’un algorithme incrémental de détection de cycles publié récemment. Nous démontrons ainsi que notre méthodologie passe à l’échelle, permet de traiter des algorithmes complexes, donc l’analyse de complexité s’appuie sur des invariants fonctionnels subtils, et peut vérifier du code qu’il est au final possible d’utiliser au sein de programmes réellement utiles et utilisés.