Quelles sont les techniques formelles courantes pour prouver que le code fonctionnel est correct?

10

Je veux fournir des preuves pour des parties d'un programme Haskell que j'écris dans le cadre de ma thèse. Jusqu'à présent cependant, je n'ai pas réussi à trouver un bon ouvrage de référence.

Le livre d'introduction de Graham Hutton, Programming in Haskell ( Google Books ) - que j'ai lu tout en apprenant Haskell - aborde quelques techniques de raisonnement sur des programmes tels que

  • raisonnement équationnel
  • en utilisant des motifs qui ne se chevauchent pas
  • liste d'induction

dans le chapitre 13, mais ce n'est pas très en profondeur.

Y a-t-il des livres ou des articles que vous pouvez recommander qui fournissent un aperçu plus détaillé des techniques de vérification formelles pour Haskell, ou un autre code fonctionnel?

reference-request proof-techniques functional-programming books software-verification FK82
la source

Réponses:

5

L'une des méthodes de facto pour prouver les résultats de la programmation fonctionnelle est via le groupe de Richard Bird.

En particulier, vous demandez une approche approfondie ou au moins plus complète du raisonnement équationnel et de l'induction de liste, ce qui est fourni dans les conférences sur la programmation fonctionnelle constructive .

Plus généralement, le texte «Algèbre de programmation», de Bird et de Moor, traite également de la justesse des algorithmes fonctionnels tels que l'optimisation et les problèmes de programmation dynamique.

Si vous rencontrez d'autres ressources utiles pour ce problème, veuillez les mentionner et nous pourrons peut-être transformer ce post en wiki.

Musa Al-hassy
la source
Je vous remercie! Bien sûr, si je trouve plus de ressources, je veillerai à les ajouter à mon message.
FK82
6

Vous pouvez commencer par

Les sujets incluent les concepts de base de la logique, la démonstration assistée par ordinateur, l'assistant de preuve Coq, la programmation fonctionnelle, la sémantique opérationnelle, la logique Hoare et les systèmes de type statique. L'exposition est destinée à un large éventail de lecteurs, des étudiants de premier cycle avancés aux doctorants et aux chercheurs. Aucun fond spécifique dans la logique ou les langages de programmation n'est supposé, bien qu'un degré de maturité mathématique soit utile.

Vous pouvez ignorer (ou survoler) les parties théoriques du langage de programmation et apprendre uniquement à gérer les preuves formelles à partir de la préface jusqu'à IndPrinciples. Le livre est vraiment bien écrit et éclairant.

Ensuite, vous voudrez peut-être continuer

Dans ce volume, vous apprendrez comment spécifier et vérifier (prouver l'exactitude de) les algorithmes de tri, les arbres de recherche binaires, les arbres de recherche binaires équilibrés et les files d'attente prioritaires. Avant d'utiliser ce livre, vous devez avoir une certaine compréhension de ces algorithmes et structures de données, disponibles dans n'importe quel manuel d'algorithmes standard de premier cycle. Vous devez comprendre tout le contenu du Software Foundations Volume 1 (Logic Foundations)

Un avertissement: VFA est toujours en version bêta!

Anton Trunov
la source
(Votre deuxième lien vous dirige vers le mauvais endroit.) En outre, il existe une programmation fonctionnelle vérifiée dans Agda ; qui utilise Agda, formellement un langage de programmation mais utilise unicode et est donc plus proche de la notation mathématique.
Musa Al-hassy
Corrigé, merci. Oui, j'ai lu VFPiA, mais ce n'est pas à mon goût.
Anton Trunov
Merci pour votre réponse! Je pense qu'il y a une idée fausse. Je ne cherche pas des techniques fonctionnelles pour prouver des algorithmes (comme un assistant de preuve), mais des techniques pour prouver le code fonctionnel (par exemple pour prouver une implémentation fonctionnelle d'un algorithme donné correcte) @ La réponse de MusaAl-hassy est très proche de ma réponse souhaitée. Au cas où je l'aurais manqué et que les livres que vous avez cités couvrent également cet aspect, pourriez-vous ajouter les chapitres pertinents?
FK82
@ FK82 Voici un Theorem app_assoc : ∀ l1 l2 l3 : natlist, (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3)extrait du chapitre Listes . Cet exemple ressemble-t-il à la chose qui vous intéresse? Ils commencent par la programmation fonctionnelle dans Coq, puis passent au raisonnement sur les propriétés des programmes fonctionnels. Les chapitres de la Préface à IndPrinciples couvrent les deux, et je dirais que la programmation et le raisonnement y sont intimement liés.
Anton Trunov
1
@ FK82 (1) Je suis totalement d'accord avec ce commentaire. (2) Vous voudrez peut-être consulter le livre «Penser fonctionnellement avec Haskell» (2015) de R. Bird. Le livre contient des tonnes d'exemples de raisonnement sur Haskell. (3) De plus, "Pearls of Functional Algorithm Design" (2010) du même auteur peut vous être utile.
Anton Trunov
5

Il s'avère qu'une excellente source de techniques de preuve et d'exemples pour prouver les choses sur les langages fonctionnels purs sont les assistants de preuve qui incluent généralement dans leur langage de spécification un langage fonctionnel pur sur lequel il est possible de raisonner équationnellement.

On pourrait vouloir consulter un livre comme Certified Programing with Dependent Types pour une introduction approfondie à ce type de raisonnement dans un assistant de preuve spécifique, à savoir Coq.

cody
la source
Merci! En fait, je recherche spécifiquement des techniques à Haskell . Mon message a été modifié pour inclure tout le code fonctionnel, mais c'est bien au-dessus de mes intentions.
FK82
1
Je ne connais pas les systèmes conçus pour vérifier spécifiquement Haskell, mais je voudrais noter que 1) Le noyau fonctionnel de Coq (et Agda) est essentiellement indiscernable de celui de Haskell (sauf pour la restriction des fonctions totales ) et 2) Programmes vérifiés dans Coq et Agda peuvent être extraites vers Haskell (bien que je pense que l'extraction vers Haskell est mieux prise en charge dans Agda, où Coq est plus centrée sur Ocaml)
cody
Bon à savoir! Cela impliquerait cependant que je réécris mon programme (ou les parties pertinentes) en Coq ou Agda. Je ne pense pas que ce soit raisonnable dans mon cas.
FK82
Il existe quelques "frontaux" très expérimentaux qui tentent de convertir Haskell en Isabelle ou de prouver directement des équivalences en utilisant Isabelle, mais je ne détiendrais pas trop de stock dans leur maturité. Je pense que réécrire le code serait finalement moins de travail.
cody
4

Je suggère d'utiliser les logiques du programme. Ils gèrent bien mieux les effets que les systèmes de frappe.

Il existe de nombreuses logiques de programme pour les langages fonctionnels. Cela devient intéressant avec des effets. Voir par exemple le raisonnement logique pour les fonctions d'ordre supérieur avec l'état local .

Le travail d'Arthur Charguéraud intègre l'approche logique du programme avec les assistants de preuve, voir par exemple cette page de présentation .

Martin Berger
la source