03 - 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

Dans le troisième cours, nous avons étudié les structures de données et la vérification de programmes qui les manipulent. Les tableaux sont la plus ancienne des structures de données. Une extension simple de la logique de Hoare avec une règle pour l'affectation à un élément d'un tableau permet de spécifier et de vérifier de nombreux programmes utilisant des tableaux, comme par exemple les tris en place.

Les pointeurs, aussi appelés références, permettent de représenter de nombreuses structures de données : graphes, listes chaînées, arbres... Un codage des pointeurs en termes de tableaux globaux, comme proposé par R. Burstall (1972) et développé par R. Bornat (2000), se révèle efficace pour vérifier des algorithmes opérant sur des graphes, mais très lourd pour les algorithmes sur les listes et autres structures chaînées. En effet, il est difficile d'éviter les situations de partage, d'alias et d'interférence qui peuvent invalider ces structures.

C'est en cherchant à décrire et maîtriser ces phénomènes d'interférence que J. C. Reynolds, rejoint ensuite par P. O'Hearn et H. Yang, invente entre 1997 et 2001 la logique de séparation. Cette logique met en avant l'importance du raisonnement local et des règles d'encadrement associées, le besoin d'associer une empreinte mémoire à chaque assertion, et le concept de conjonction séparante entre assertions.

Nous avons illustré l'approche en développant une logique de séparation pour un petit langage fonctionnel et impératif doté de variables immuables et de pointeurs vers des cases mémoires mutables. Cette logique de séparation permet de décrire très précisément de nombreuses structures de données par des prédicats de représentation : listes simplement ou doublement chaînées, listes circulaires, arbres, etc., et de spécifier et vérifier leurs principales opérations.

Enfin, nous avons esquissé deux démonstrations de la correction sémantique de cette logique de séparation, l'une reposant sur une propriété de non-déterminisme de l'allocation mémoire ; l'autre, sur une quantification sur tous les encadrements possibles.