Résumé
Tout comme la logique mathématique donne des lois pour raisonner sur les définitions et les énoncés mathématiques, une logique de programmes pour un langage de programmation donne des lois pour établir des propriétés vraies de toutes les exécutions possibles d'un programme écrit dans ce langage. Après des rappels sur cette approche déductive de la vérification de programmes et sur la plus ancienne de ces logiques, celle publiée par C.A.R. Hoare en 1969, ce cours a montré comment cette logique de Hoare s'applique à de nombreuses structures de contrôle, dont plusieurs formes de boucles, avec sortie prématurée mono-niveau ou multi-niveaux, mais aussi à des constructions non déterministes comme les commandes gardées de Dijkstra, et jusqu'aux coroutines asymétriques et aux threads coopératifs vus au deuxième cours. Même le branchement « goto » peut être spécifié en logique de Hoare, en prenant quelques précautions.
La seconde partie du cours a introduit la logique de séparation, une logique de programmes plus récente qui permet de raisonner plus facilement sur les pointeurs (références) vers l'état mutable ainsi que sur la bonne utilisation des ressources du système informatique. Nous avons étudié comment raisonner en logique de séparation sur les programmes impératifs et fonctionnels utilisant des opérateurs de contrôle comme « call/cc » ou les gestionnaires d'effets, en suivant les approches publiées par Timany et Birkedal en 2019 et par de Vilhena et Pottier en 2021. Autant les continuations que l'on peut lancer plusieurs fois invalident facilement les règles usuelles des logiques de programmes, autant les continuations à usage unique telles qu'utilisées dans OCaml 5 restent compatibles avec une logique de séparation classique.
