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

Le deuxième cours a été consacré à l'étude approfondie des « logiques de Hoare », c'est-à-dire des logiques de programmes qui suivent l'approche introduite par C. A. R. Hoare en 1969. Nous avons défini une telle logique de programmes pour le langage IMP, un petit langage impératif à contrôle structuré que nous avions déjà étudié dans le cours 2019-2020 « Sémantiques mécanisées ». Nous avons ensuite développé diverses extensions de cette logique : règles de raisonnement dérivées ou admissibles, non-déterminisme, erreurs dynamiques, contrôle non structuré, etc.

La suite du cours a étudié les liens entre la logique de programmes et la sémantique opérationnelle du langage IMP. Nous avons défini et démontré la correction sémantique de la logique : toutes les propriétés d'un programme dérivables par les règles de la logique sont bien vérifiées par toutes les exécutions concrètes du programme. Plusieurs techniques de démonstration ont été esquissées : inductives, co-inductives, ou encore par comptage de pas (step-indexing).

La complétude est la propriété réciproque de la correction sémantique : toute propriété vraie de toutes les exécutions d'un programme peut-elle s'exprimer comme un triplet de Hoare et se dériver par règles de la logique ? Une logique complète permettrait de décider le problème de l'arrêt. La complétude absolue est donc impossible pour un langage Turing-complet. En revanche, la logique de Hoare satisfait une propriété de complétude relative montrant qu'elle est aussi expressive qu'un raisonnement direct sur les exécutions des programmes, à logique ambiante fixée.

Enfin, nous avons discuté des possibilités d'automatiser une vérification déductive à base de logique de Hoare. À condition de fournir manuellement les invariants des boucles, un calcul de plus faible précondition, ou de plus forte postcondition, permet de réduire la vérification d'un programme en logique de Hoare à la vérification d'un ensemble d'implications en logique du premier ordre, tâche qui peut être confiée à des démonstrateurs automatiques ou assistés.