Formalisation d'une bibliothèque d'ensembles finis en Coq

Cette page présente une formalisation dans l'assistant de preuve Coq d'une bibliothèque d'ensemble finis. Elle contient en fait trois codages différents des ensembles finis : à l'aide de listes triées, d'arbres rouges et noirs et d'AVLs. Cette formalisation fait un grand usage des modules et des foncteurs, une nouveauté de Coq 7.4, et en démontre la puissance en tant qu'outil de preuve autant qu'en tant qu'outil de programmation.

Transparents en Français : Active DVI et PostScript (exposé du 3 juillet 2003)
Rapport de recherche LRI : Functors for Proofs and Programs (PostScript file). Sera présenté à ESOP 2004

Code Ocaml de départ

• Arbres rouges et noirs: rbset.mli / rbset.ml / rbset.ps
• AVL de la bibliothèque standard d'Ocaml : set.mli / set.ml

Code Ocaml obtenu par extraction

• Arbres rouges et noirs: rbt.mli / rbt.ml
• AVL: avl.mli / avl.ml

Sources Coq

• Naviguer dans les fichiers Coq:
  • Index global
  • Table des matières
  • FSetInterface : signatures de type ordonné (OrderedType) et d'ensembles finis (S et Sdep)
  • FSetBridge foncteurs passerelles entre les interfaces dépendantes et non-dépendantes
  • FSetProperties propriétés additionnelles
  • FSetList : codage par des listées triées
  • FSetRBT : codage par des arbres rouges et noirs
  • FSetAVL : codage par des AVLs
  • FSet charge toute la bibliothèque
• Récupérer les sources: FSets.tar.gz / FSets for Coq V8.0
• Fichier Postscript