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

Xavier Leroy

Collège de France

Science du logiciel

Année 2020-2021

Logiques de programmes : quand la machine raisonne sur ses logiciels

Ré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.