Download Le Coq` Art (V8)

13.4. DÉVELOPPEMENT D’UN MODULE : LES DICTIONNAIRES
379
les spécifications ont du être modifiés, les preuves de lemmes sur les arbres de
recherche n’ont subi que quelques modifications locales.
13.4.4.1
Structure du foncteur
Le module paramétrique associé à la réalisation de dictionnaires par arbres de
recherche ressemble beaucoup à ceux que nous avons déjà vus. Nous commençons
par importer quelques champs des paramètres Key, de signature DEC_ORDER et
Val de signature DATA :
Module TDict (Key:DEC_ORDER)(Val:DATA) :
DICT with Definition key := Key.A
with Definition data := Val.data.
Definition key := Key.A.
Definition data := Val.data.
Module M := More_Dec_Orders Key.
Travail d’adaptation
Les arbres manipulés dans notre implémentation se distinguent de ceux du
chapitre 12 par le double étiquetage (clef,valeur ) des sommets internes. Toutes
les définitions de types : occ, min, maj, search_tree, . . ., prennent en compte
cette modification : par exemple le prédicat occ a pour type
“ data → key→ btree→ Prop ”, la proposition “ occ d k t ” signifiant : « il
existe un sommet de t étiqueté par la clef k et la donnée d ». Nous donnons
ci-dessous le type inductif associé aux arbres binaires, en laissant au lecteur le
soin de définir les prédicats occ et search_tree.
Inductive btree : Set :=
| leaf : btree
| bnode : key→data→btree→btree→btree.
Le travail d’adaptation se poursuit en modifiant les notions de recherche
et d’insertion. Le type du programme de recherche pour une clef k dans un
arbre t utilise sumor ; en effet, soit on retourne une valeur d associée à k dans t,
accompagnée d’une preuve que l’entrée (k, d) est bien dans t, soit une preuve
qu’aucune valeur ne se trouve associée à k.
Definition occ_dec_spec (k:key)(t:btree) :=
search_tree t → {d:data | occ d k t}+{(∀ d:data, ∼occ d k t)}.
La spécification de l’insertion tient compte d’une conséquence de la spécification
DICT : si on insère à une clef déjà présente dans l’arbre, la nouvelle entrée masque
la précédente :