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

25

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.

Nathan BeDell
la source

Réponses:

13

Honda et Yoshida

(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:

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:

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.

Martin Berger
la source
15

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.

cody
la source
sans trop de peine - pas vraiment. Idris est strict par défaut, et Haskell est paresseux; cela pose à lui seul un problème majeur. La compatibilité avec Haskell n'a également jamais été une priorité très élevée pour la conception d'Idris.
Bartek Banachewicz
C'est suffisant. Agda vérifie la terminaison par défaut, donc les choses comme la rigueur ne sont pas un problème en théorie . Bien sûr, le temps d'exécution pourrait être radicalement différent.
cody
8

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 .

Ohad Kammar
la source
1

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.

Sam Tobin-Hochstadt
la source