Résumé
Comment montrer qu’un programme est correct (toutes ses exécutions calculent le résultat attendu) ou, a minima, qu’il est sûr (aucune exécution ne produit un « plantage » ou une faille de sécurité) ? On peut raisonner directement sur la sémantique du programme, mais c’est laborieux. Les logiques de programmes fournissent des principes de plus haut niveau pour raisonner sur les propriétés d’un programme.
Cette approche déductive apparaît dès 1949 dans une brève communication de Turing lui-même, puis est redécouverte et généralisée par Floyd en 1967, sur des programmes de type « organigramme ». Mais c’est Hoare, en 1969, qui introduit le concept de « logique de programmes » et donne les règles de base d’une telle logique pour les langages à contrôle structuré.
Dans ce quatrième cours, nous avons défini puis mécanisé en Coq une logique de Hoare pour le langage IMP. La mécanisation fait clairement apparaître les deux manières de définir les « triplets de Hoare » {P} c {Q} qui sont valides : axiomatiquement, par des règles de déduction, ou sémantiquement, en termes des exécutions du programme c. L’équivalence entre des deux définitions démontre la correction et la complétude de la logique de Hoare.
La logique de Hoare s’étend assez facilement aux programmes manipulant des tableaux, mais plus difficilement aux programmes avec pointeurs manipulant des structures de données chaînées. Une réflexion profonde sur les notions de localité, d’alias, et de ressources conduisent O’Hearn, Reynolds et Yang à inventer, de 1999 à 2001, la logique de séparation, avec ses notions d’empreinte mémoire pour chaque assertion logique et de conjonction séparante entre ces assertions. La logique de séparation est très efficace pour vérifier les structures de données chaînées sans partage. Son extension au parallélisme à mémoire partagée, la logique de séparation concurrente, est l’objet de nombreux travaux de recherche récents.
