Une preuve formelle de l'algorithme de Tarjan-1972 pour trouver les composantes fortement connexes dans un graphe

Ran Chen 1, 2 Jean-Jacques Lévy 3
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
3 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique, Inria de Paris
Résumé : Nous présentons une preuve formelle de l'algorithme de Tarjan (1972) pour trouver les composantes fortement connexes dans un graphe. Cet algorithme exécute une seule passe sur le graphe le parcourant en profondeur d'abord. Notre programme est icí ecrit dans un style de programmation fonctionnelle dans le langage Why3-ML. La preuve utilise des lemmes et des assertions exprimés dans la logique de Why3. La majorité d'entre eux sont prouvés automatiquementàautomatiquementà l'exception de 5 assertions ou lemmes prouvés manuellement en Coq. Une preuve d'une version impérative de ce programme ne figure pas dans notre article, mais nous indiquons comment y parvenir par raffinements successifs. Un point important de notre article est que nos preuves sont intuitives et lisibles par un humain.
Type de document :
Communication dans un congrès
JFLA 2017 - Vingt-huitièmes Journées Francophones des Langages Applicatifs, Jan 2017, Gourette, France. Vingt-huitièmes Journées Francophones des Langages Applicatifs
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01422215
Contributeur : Jean-Jacques Levy <>
Soumis le : samedi 24 décembre 2016 - 10:01:38
Dernière modification le : jeudi 11 janvier 2018 - 06:28:03
Document(s) archivé(s) le : mardi 21 mars 2017 - 09:45:35

Fichier

16jfla.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01422215, version 1

Citation

Ran Chen, Jean-Jacques Lévy. Une preuve formelle de l'algorithme de Tarjan-1972 pour trouver les composantes fortement connexes dans un graphe. JFLA 2017 - Vingt-huitièmes Journées Francophones des Langages Applicatifs, Jan 2017, Gourette, France. Vingt-huitièmes Journées Francophones des Langages Applicatifs. 〈hal-01422215〉

Partager

Métriques

Consultations de la notice

189

Téléchargements de fichiers

45