Résumé
Le dernier cours de l'année a étudié les logiques de programmes pour les fonctions, incluant les fonctions d'ordre supérieur et les fonctions comme valeurs de première classe. Les procédures récursives sont l'une des premières extensions de la logique de Hoare. Les règles de raisonnement sont à la fois élégantes dans leur traitement de la récursion et compliquées par de nombreuses restrictions sur l'utilisation et la modification des variables.
Une logique de séparation pour un langage à variables immuables et cases mémoire mutables permet non seulement une formulation plus claire des règles pour les procédures et les fonctions du premier ordre, mais aussi une extension à l'ordre supérieur. Dans cette extension, les triplets de Hoare font partie des assertions de la logique, et peuvent donc être utilisés en préconditions de fonctions d'ordre supérieur, pour spécifier les arguments de type « fonction », ainsi que dans les prédicats de représentation, pour spécifier les méthodes d'un objet tout en cachant son état interne. La correction sémantique de la règle pour les fonctions récursives pose des problèmes de circularité, qui se résolvent soit par une extension de la technique de comptage de pas, soit par l'utilisation d'une logique modale comprenant la modalité ⊳ (lire: « plus tard »).
De nouvelles manières de présenter et d'utiliser les logiques de programmes s'ouvrent à nous dans les logiques d'ordre supérieur et à types dépendants. Le système CFML représente un programme fonctionnel et impératif par sa formule caractéristique : un prédicat d'ordre supérieur qui décrit de manière compositionnelle toutes les préconditions et postconditions valides du programme. Cette représentation est particulièrement adaptée à la vérification interactive ainsi qu'à la spécification des fonctions d'ordre supérieur. Utilisant des types dépendants, les monades de Hoare et de Dijkstra ajoutent aux monades usuelles des préconditions et des postconditions (monades de Hoare) ou un calcul de plus faible précondition (monades de Dijkstra). Le langage F* s'appuie sur une hiérarchie de monades de Dijkstra et sur un typeur qui produit des conditions de vérification pour fournir un excellent environnement de programmation fonctionnelle et impérative vérifiée.
