01 - Logiques de programmes : quand la machine raisonne sur ses logiciels

Xavier LeroyCollège de FranceScience du logicielAnnée 2020-2021Logiques de programmes : quand la machine raisonne sur ses logicielsRésuméComment s'assurer qu'un logiciel fait ce qu'il est censé faire ? Les méthodes classiques de vérification et de validation du logiciel, reposant sur le test, les revues et les analyses, ne suffisent pas toujours. La vérification déductive permet d'aller plus loin en établissant des propriétés vraies de toutes les exécutions possibles d'un programme, via des raisonnements formels au sein d'une logique appropriée : une logique de programmes. Le premier cours a illustré cette approche par la vérification déductive d'une fonction de recherche dichotomique dans un tableau trié, un algorithme très utilisé et souvent implémenté de manière incorrecte.Ensuite, le cours a retracé l'émergence de la vérification déductive et des logiques de programmes via trois publications fondatrices. La brève communication d'Alan Turing en 1949, intitulée « Checking a large routine », introduit deux idées majeures : les assertions logiques et les ordres de terminaison, et les illustre sur la vérification d'un petit programme exprimé par un organigramme. Trop en avance sur son temps, et jamais publié formellement, ce texte précurseur tombe dans l'oubli jusqu'en 1984.L'article de Robert W. Floyd de 1967, « Assigning meanings to programs », réinvente l'approche de Turing et l'approfondit considérablement, avec une formalisation complète des conditions de vérification qui garantissent qu'un programme est correctement annoté, et l'observation, révolutionnaire pour l'époque, qu'une telle formalisation constitue une sémantique formelle du langage de programmation utilisé.Enfin, l'article de C. A. R. Hoare de 1969, intitulé « An axiomatic basis for computer programming », constitue le manifeste de la vérification déductive moderne. L'article étend les résultats de Floyd à un langage à contrôle structuré (séquences, conditionnelles, boucles) et introduit des notations toujours utilisées aujourd'hui (les « triplets de Hoare »). Mais, au-delà des contributions techniques, cet article est visionnaire tant par son approche purement axiomatique de la vérification déductive que par son analyse lucide de l'intérêt pratique de cette approche.

Om Podcasten

Écrire un petit programme informatique est facile. Concevoir et réaliser un logiciel complet qui soit fiable, pérenne et résistant aux attaques reste extraordinairement difficile. C'est le but des sciences du logiciel que de concevoir et développer les principes, les formalismes mathématiques, les techniques empiriques et les outils informatiques nécessaires pour concevoir, programmer et vérifier des logiciels fiables et sécurisés.L'enseignement de la chaire Sciences du logiciel vise à explorer cette problématique et à présenter la recherche contemporaine dans ce domaine. Le cours privilégie les approches dites « formelles », par opposition à l'empirisme souvent de mise en génie logiciel. Ces approches s'appuient sur des fondements mathématiquement rigoureux, connus ou en émergence : sémantiques formelles, logiques de programmes, systèmes déductifs, équivalences de programmes, calculs de processus… Historiquement, ces concepts ont émergé de considérations de programmation très terre-à-terre avant de se parer de rigueur mathématique. Le cours s'efforce de retracer ce cheminement des idées en partant de l'intuition du programmeur et en allant jusqu'à la mécanisation de ces approches formelles.Les premières années de cet enseignement auraient pu s'intituler « Programmer, démontrer », car ils ont exploré plusieurs modes d'interaction entre la programmation de logiciels et la démonstration d'énoncés mathématiques : programmer puis démontrer, comme dans les logiques de programmes pour la vérification déductive ; programmer pour démontrer, comme dans les logiques constructives et l'assistant à la démonstration Coq ; enfin, programmer égale démontrer, comme dans la féconde correspondance de Curry-Howard, objet de la première année du cours.La recherche de la chaire Sciences du logiciel s'effectue dans le cadre de l'équipe-projet Cambium, commune avec l'Inria. Les travaux de l'équipe visent à améliorer la fiabilité, la sûreté et la sécurité du logiciel en faisant progresser les langages de programmation et les méthodes de vérification formelle de programmes. Les principaux thèmes de recherche sont les systèmes de types et les algorithmes d'inférence de types, la vérification déductive de programmes, le parallélisme à mémoire partagée, et les modèles mémoires faiblement cohérents. L'équipe conçoit et développe deux grands logiciels de recherche qui intègrent et font passer dans la pratique bon nombre de ses résultats : OCaml, un langage de programmation fonctionnel statiquement typé et son implémentation, et CompCert, un compilateur formellement vérifié pour logiciels embarqués critiques.