Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/hal-00665909
Contributor : Alain Monteil <>
Submitted on : Friday, February 3, 2012 - 10:49:18 AM
Last modification on : Saturday, January 13, 2018 - 1:04:00 AM
Long-term archiving on: : Friday, May 4, 2012 - 2:25:07 AM

File

paper_1.pdf
Files produced by the author(s)

Identifiers

  • 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. ⟨hal-00665909⟩

Share