Dérivation de l'algorithme de Schorr-Waite en Coq par une méthode algébrique

Résumé : Nous présentons une spécification, une dérivation et une preuve de correction totale de l'algorithme de Schorr-Waite pour un marquage en profondeur d'un graphe binaire codé par des pointeurs. Notre approche est purement algébrique et fonctionnelle, depuis une spécification simple jusqu'à un programme récursif terminal simulant le langage C. Puis, nous obtenons par des transformations élémentaires un véritable programme en C, impératif et itératif.
Type de document :
Communication dans un congrès
JFLA - Journées Francophones des Langages Applicatifs - 2012, Feb 2012, Carnac, France. 2012
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00665909
Contributeur : Alain Monteil <>
Soumis le : vendredi 3 février 2012 - 10:49:18
Dernière modification le : samedi 13 janvier 2018 - 01:04:00
Document(s) archivé(s) le : vendredi 4 mai 2012 - 02:25:07

Fichier

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

Identifiants

  • HAL Id : hal-00665909, version 1

Collections

Citation

Jean-François Dufourd. Dérivation de l'algorithme de Schorr-Waite en Coq par une méthode algébrique. JFLA - Journées Francophones des Langages Applicatifs - 2012, Feb 2012, Carnac, France. 2012. 〈hal-00665909〉

Partager

Métriques

Consultations de la notice

89

Téléchargements de fichiers

122