Existe-t-il des systèmes de vérification formels annotés pour les langages de programmation fonctionnels purs?

ACSL (Ansi C Specification Language), est une spécification pour le code C, annotée de commentaires spéciaux, qui permet de vérifier formellement le code C.

Je ne l'ai pas étudié, mais j'imagine que les méthodes formelles utilisées dans ACSL vérificateurs seraient similaires à Hoare Logic. Pour les langages fonctionnels purs, comme Haskell, je ne peux pas imaginer quel type de formalisme serait utilisé pour la vérification formelle.

Quelqu'un at-il fait quelque chose de similaire à ACSL , mais pour un langage fonctionnel pur? Sinon, y a-t-il eu des recherches sur la vérification formelle de style annoté par spécifications pour les langages fonctionnels?

Je sais qu'il existe un typage dépendant, que de nombreuses langues (Agda, Idris, etc ...) prennent en charge, mais dans Haskell, le typage dépendant est difficile sans faire un type de sorcellerie (illisible?). Dans cet esprit, et comme Haskell a un support de bibliothèque bien meilleur qu'Agda et Idris, je pense qu'un tel système de vérification formelle fonctionnelle pourrait être utile, mais je ne sais pas si des recherches ont été faites à ce sujet ou non.

Honda et Yoshida

• Une logique de programme de composition pour les fonctions polymorphes d'ordre supérieur

(probablement) pionnier de la logique Hoare pour les langages purement fonctionnels. Ce travail est basé sur la logique de Hennessy-Milner et l'encodage de fonctions de Milner en processus, comme décrit ici:

• De la logique de processus à la logique de programme

Le travail de Régis-Gianas et al mentionné dans une autre réponse est similaire au premier travail ci-dessus de Honda / Yoshida. Cela a été étendu aux langages efficaces de style ML:

• Une logique de programme complète pour les fonctions impératives d'ordre supérieur

• Une analyse logique de l'aliasing dans les fonctions impératives d'ordre supérieur

• Raisonnement logique pour les fonctions d'ordre supérieur avec état local

• Logiques de programme pour le contrôle séquentiel d'ordre supérieur

• Logiques de programme pour une méta-programmation homogène

Les logiques mentionnées sont ce que l'on appelle l'observation complète, ce qui signifie que la sémantique opérationnelle et logique coïncident. Arthur Charguéraud a utilisé ce complément pour ses travaux sur la vérification des programmes fonctionnels de style Hoare en Coq.

$F^*$ , qui propose des constructions similaires.

Il semble y avoir une correspondance étroite entre les types de raffinement et les notations de type ACSL.

Enfin, je ne peux que suggérer de regarder de plus près Agda et Idris, car ils peuvent être compilés en Haskell, et visent à fournir à l'utilisateur un langage de programmation utilisable (en particulier Idris). Je soupçonne qu'il est possible d'intégrer les bibliothèques Haskell dans le code Idris sans trop de problèmes.

Voir aussi le travail de thèse de Yann Régis-Gianas avec François Pottier: Une logique de Hoare pour les programmes fonctionnels d'appel par valeur (MPC'08) . Ce travail a été étendu pour couvrir les effets secondaires habituels du ML par Johannes Kanig et Jean-Cristophe Filliatre en 2009: Who: A Verifier for Effectful Higher-Order Programs .

Il y a un article dans l' ICFP de cette année , les types de raffinement pour Haskell . Le document traite de la vérification de la terminaison plutôt que de la logique Hoare complète, mais j'espère que c'est un début dans cette direction.

La section de travail connexe de cet article contient des pointeurs, tels que Xu, Peyton-Jones et Claessen's statique contract checking for Haskell , et Sonnex, Drossopoulou et Eisenbach's Zeno and Vytiniotis, Peyton-Jones, Claessen et Rosen's Halo .

Notre travail sur la vérification souple des contrats est lié, à OOPSLA 2012 et ICFP 2014 , vous permet d'écrire des contrats, qui ressemblent beaucoup aux spécifications ACSL, puis de les vérifier statiquement ou de les utiliser une vérification dynamique lors de l'exécution.