Correction et terminaison de la fusion de 2 fichiers

Analyse de l'algorithme

Le but de cet algorithme est de réaliser la fusion triée de deux fichiers préalablements triés. Il fonctionne suivant deux phases : la première consiste en la recopie des éléments de f1 et de f2 dans f, et dans le bon ordre. Elle se termine dès que l'un des deux fichiers est vide. La seconde phase débute alors. Elle consiste en la recopie des éléments du fichier non vide dans f.

Pour que l'algorithme soit correct, il est nécessaire que les fichiers f1 et f2 soient triés. Dans ce cas, il doit garantir que le résultat f est trié et qu'il contient tous les éléments de f1 et de f2.

Analyse de la première phase

Tant qu'il reste des éléments dans f1 et dans f2, on sélectionne le plus petit des éléments pointés dans les deux fichiers, puis on l'inscrit en fin de f. Par hypothèse, f1 et f2 sont triés, donc lorsque nous écrivons un élément dans f, nous savons alors :

qu'il est au moins égal à tous les éléments de f (initialement vide)
et qu'il est au plus égal à tous les éléments de f1 et f2

Alors, il est nécessaire et suffisant que les propriétés suivantes soient vraies à chaque itération de la boucle while :

les fichiers f1 et f2 sont triés
le fichier f est trié
le dernier élément de f est inférieur ou égal au premier élément de f1 et à celui de f2
l'union des éléments de f1, f2 et f est égale à l'union des éléments des fichiers initiaux

Cette phase termine car les fichiers sont finis bornés. Sachant qu'à chaque itération de la boucle la taille de f1 ou celle de f2 décroît strictement, nous pouvons affirmer que la somme de leurs tailles décroît strictement à chaque itération. Il faudra par ailleurs prouver que celle-ci est à valeurs dans N.

Analyse de la seconde phase

Lorsque la première phase se termine, l'un des fichiers f1 ou f2 est vide, donc une seule des deux boucles sera exécutée lors de cette phase. Supposons que ce soit f1 qui est vide (l'autre cas est symétrique), alors la dernière boucle est exécutée.

D'après nos déductions sur la première phase, nous savons que :

f1 est vide et que f2 est trié (et éventuellement vide)
f est trié
le dernier élément de f est au plus égal à l'élément pointé dans f2
l'union des éléments de f2 et de f est égale à l'union des éléments des fichiers initiaux

Alors, il faut et il suffit que ces propriétés restent vraies pendant l'itération de la boucle pour que l'algorithme soit correct.

Cette phase termine nécessairement car les fichiers sont finis bornés. Sachant que la taille de f2 décroît strictement à chaque itération de la boucle, et que le nombre d'éléments d'un fichiers est un entier naturel, on tient une mesure de convergence.

Formalisation de l'analyse

Hypothèses sur les fichiers

Pour la preuve de cet algorithme, nous devons pouvoir exprimer certaines propriétés des fichiers :

Nous ajoutons un prédicat trie(f) qui vaut vrai lorsque f est trié et faux sinon. À la place de ce prédicat, nous aurions pu écrire une formule de la logique du 1er ordre, mais cela alourdirait la preuve.
Nous ajoutons une opération dernier : fichier -> elmt qui renvoie le dernier élément d'un fichier non vide. Ceci nous permet d'exprimer que le dernier élément de f est au plus égal aux éléments pointés de f1 et f2.
Nous ajoutons une opération elmts : fichier -> {elmt} qui renvoie le multi-ensemble constitué des éléments du fichier. Ceci nous permet de prouver qu'aucun élément de f1 et f2 n'est perdu et qu'aucun élément indésirable est ajouté à f.
L'opération d'union sur les {elmt} sera notée +
Nous ajoutons une opération nb_elmts : fichier -> Nat qui renvoie le nombre d'éléments que contient un fichier. Ceci nous permet de prouver la terminaison des boucles.

De plus, nous ferons les hypothèses suivantes :

le fichier vide est un fichier contenant le seul élément EOF qui est de plus pointé par le curseur.
la fonction avancer(f) renvoie un fichier identique à f amputé de son premier élément. Son effet sur un fichier vide est non spécifié.

Algorithme instrumenté pour la preuve

Nous ajoutons quelques variables dans le code pour pouvoir réaliser notre preuve :

f := fichier_vide; f1' := f1; f2' := f2;
while (reste_elmt(f1') /\ reste_elmt(f2')) do
  if (lire(f1') < lire(f2')) then
    f := ecrire(f,lire(f1'));
    f1' := avancer(f1')
  else
    f := ecrire(f,lire(f2'));
    f2' := avancer(f2')
  endif
endwhile;
while (reste_elmt(f1')) do
  f := ecrire(f,lire(f1'));
  f1' := avancer(f1')
endwhile;
while (reste_elmt(f2')) do
  f := ecrire(f,lire(f2'));
  f2' := avancer(f2')
endwhile

Puisque avancer est une opération destructrice pour les fichiers, nous réalisons au préalable une copie de f1 dans f1' et de f2 dans f2' afin de pouvoir désigner les fichiers initiaux tout au long de l'exécution de l'algorithme (y compris à la fin de celle-ci).

Pré-conditions, post-conditions, invariants et mesures

POST-CONDITION : à la fin de l'exécution de l'algorithme, f doit être trié, et il doit contenir exactement les éléments de f1 et f2.
```
trie(f) /\ (elmts(f)=elmts(f1)+elmts(f2))
  
```
PRÉ-CONDITION : on suppose que les fichiers f1 et f2 passés en paramètre sont triés.
```
trie(f1) /\ trie(f2)
  
```

Nous exprimons maintenant pour chaque boucle les conditions nécessaires et suffisantes exprimées informellement ci-dessus.

Première boucle

INVARIANT : les fichiers sont triés, le dernier élément de f est au plus égal aux premiers éléments de f1' et f2', et l'union des éléments de f1', f2' et f est égale à l'union des éléments de f1 et f2.
```
trie(f1') /\ trie(f2') /\ trie(f)
/\ (dernier(f)<=lire(f1')) /\ (dernier(f)<=lire(f2'))
/\ (elmts(f1)+elmts(f2)=elmts(f)+elmts(f1')+elmts(f2'))
    
```
MESURE : la somme des nombres d'éléments de f1' et f2' décroît strictement et est à valeurs dans N par définition de nb_elmts.
```
nb_elmts(f1')+nb_elmts(f2')
    
```

Deuxième boucle

INVARIANT : f1' et f sont triés, le dernier élément de f est au plus égal au premier élément de f1', et l'union des éléments de f1' et f est égale à l'union des éléments de f1 et f2.
```
trie(f1') /\ trie(f)
/\ (dernier(f)<=lire(f1'))
/\ (elmts(f1)+elmts(f2)=elmts(f)+elmts(f1'))
  
```
MESURE : le nombre d'éléments de f1' décroît strictement et est à valeurs dans N par définition de nb_elmts.
```
nb_elmts(f1')
  
```

Troisième boucle

Ce cas est symétrique au précédent : il suffit de substituer f2' à f1' dans les formules.

Preuve de terminaison et de correction

On spécifie dans le while-program la pré-condition et la post-condition mentionnées précédemment, ainsi que les invariants et les mesures des boucles.

Obligations de preuve

TAD et axiomes

Les obligations de preuve énoncent des propriétés des opérations du TAD fichier. Le but de définir un TAD est justement, au delà de la définition du type, de donner des informations de correction et de complexité des opérations.

Le type lui même est défini par un certain nombre de constructeurs, ici fichier_vide et ecrire. Par exemple, le fichier contenant a b c s'écrit ecrire(ecrire(ecrire(fichier_vide,a),b),c).

Lors de la spécification des opérations sur les fichiers, nous devons définir des axiomes qui en définissent une sémantique de ces opérations. Par exemple, pour l'opération elmts, nous avons les axiomes suivants :

elmts(fichier_vide)={}
elmts(ecrire(f,e))={e}+elmts(f)

Les axiomes postulent donc des théorèmes sur les opérations, pour tous les fichiers obtenus à partir des constructeurs du TAD. Nous pouvons donc définir lire et avancer, nos deux opérations de base sur les fichiers :

lire(fichier_vide)=EOF
lire(ecrire(fichier_vide,e))=e
lire(ecrire(f,e))=lire(f)

avancer(ecrire(fichier_vide,e))=fichier_vide
avancer(ecrire(f,e))=ecrire(avancer(f),e)

Dans la suite, nous définirons les axiomes des opérations suivant les besoins de l'obligation de preuve, dans la limite des théorèmes que l'on peut honnêtement postuler.

Problème de preuve

Lorsque nous lançons le calcul de preuve sur notre while-program, nous nous trouvons confrontés à l'obligation de preuve suivante :

        trie(f1')/\trie(f)/\(dernier(f)<=lire(f1'))
        /\(elmts(f1)+elmts(f2)=elmts(f)+elmts(f1'))
        /\!((reste_elmt(f1')))
	------------------- implies -------------------
	trie(f2')/\trie(f)/\(dernier(f)<=lire(f2'))
        /\(elmts(f1)+elmts(f2)=elmts(f)+elmts(f2'))
        /\wfs(nb_elmts(f2'))

Elle exprime que la post-condition de la deuxième boucle while doit impliquer la pré-condition de la dernière boucle while (c'est la seconde obligation de preuve générée par la deuxième boucle while).

Nous ne sommes pas en mesure de prouver cette obligation, pourquoi ? Cela vient du fait que seule l'une des deux dernière boucles sera exécutée, et nous ne savons pas a priori laquelle. Or, tout ce que nous pouvons déduire d'une boucle while est un invariant, qui ne ne dépend donc pas du fait que la boucle est exécutée ou non, ni même combien de fois.

L'invariant de la seconde boucle énonce des vérités liées à son fonctionnement et à la conservation de l'information apportée par la première boucle. Mais il perd aussi d'autres informations, par exemple trie(f2') qui n'est plus utile ici. Imaginons cependant que cette deuxième boucle ne soit pas exécutée, mais que la troisième boucle le soit. Tout ce que nous savons au début de la troisième boucle est l'invariant de la seconde boucle et la négation de son test.

Afin d'avoir suffisament d'informations pour faire la preuve, il faudrait donc inclure dans l'invariant de la seconde boucle ce que nous déduisons en sortie de la première boucle. Ainsi, cette information serait véhiculée jusqu'à la troisième boucle. Cependant, cette solution est pénible : elle oblige à inscrire un invariant non intuitif pour la seconde boucle.

Afin de savoir laquelle des deux dernières boucles est exécutée (s'il y a lieu), il est préférable de rajouter un test dans le while-program, pour la preuve. Notons que cela ne remet pas en cause la correction de l'algorithme, mais seulement notre capacité à le prouver tel quel. Nous modifions donc le while-program de la façon suivante :

...
if (reste_elmt(f1')) then
  while (reste_elmt(f1')) do
  ...
  endwhile
else
  while (reste_elmt(f2')) do
  ...
  endwhile
endif

Le while-program complet est disponible ici. Nous obtenons le calcul de preuve suivant.

Preuve de la pré-condition

	trie(f1)/\trie(f2)
[0]	------------------- implies -------------------
	trie(f1)/\trie(f2)/\trie(fichier_vide)
        /\(dernier(fichier_vide)<=lire(f1))
        /\(dernier(fichier_vide)<=lire(f2))
        /\(elmts(f1)+elmts(f2)=elmts(fichier_vide)+elmts(f1)+elmts(f2))
        /\wfs(nb_elmts(f1)+nb_elmts(f2))

Notons premièrement que trie(f1)/\trie(f2)->trie(f1)/\trie(f2).

On peut bien entendu postuler que trie(fichier_vide) est vraie. Les axiomes pour trie sont donc :

trie(fichier_vide)=vrai
trie(ecrire(fichier_vide,e))=vrai
trie(ecrire(ecrire(f,e),e'))=(e<=e') /\ trie(ecrire(f,e))

L'opération dernier n'est usuellement pas définie pour le fichier vide. Si nous choisissons que dernier(fichier_vide) n'est pas définie, alors, nous devons modifier l'invariant de la première boucle afin d'imposer dernier(f)<=lire(f1') uniquement lorsque f n'est pas vide. Ici, nous choisissons plutôt de simplifier la preuve en considérant que l'opération dernier(fichier_vide) renvoie un élément inférieur à tous les autres (ex : moins l'infini). Par conséquent, dernier(fichier_vide)<=lire(f1) et dernier(fichier_vide)<=lire(f2) sont toujours vraies.
Nous avons défini précédemment que elmts(fichier_vide)={}. Donc, elmts(f1)+elmts(f2)=elmts(fichier_vide)+elmts(f1)+elmts(f2) est vraie.
Enfin, nous devons définir une interprétation du prédicat wfs. Ici, nous choisissons qu'il s'interprète comme Nat, le prédicat d'appartenance à l'ensemble des entiers naturels. Par définition, l'opération nb_elmts renvoie une valeur entière naturelle, donc wfs(nb_elmts(f1)+nb_elmts(f2)) est vraie.

Preuve de l'invariance pour la première boucle

	trie(f1')/\trie(f2')/\trie(f)
        /\(dernier(f)<=lire(f1'))
        /\(dernier(f)<=lire(f2'))
        /\(elmts(f1)+elmts(f2)=elmts(f)+elmts(f1')+elmts(f2'))
        /\(reste_elmt(f1')/\reste_elmt(f2'))
        /\(nb_elmts(f1')+nb_elmts(f2')=val3)
        /\(wfs(nb_elmts(f1')+nb_elmts(f2')))
[5]	------------------- implies -------------------
	((lire(f1')<lire(f2'))->
           trie(avancer(f1'))/\trie(f2')/\trie(ecrire(f,lire(f1')))
           /\(dernier(ecrire(f,lire(f1')))<=lire(avancer(f1')))
           /\(dernier(ecrire(f,lire(f1')))<=lire(f2'))
           /\(elmts(f1)+elmts(f2)=elmts(ecrire(f,lire(f1')))
                                  +elmts(avancer(f1'))+elmts(f2'))
           /\(nb_elmts(avancer(f1'))+nb_elmts(f2')<val3)
           /\(wfs(nb_elmts(avancer(f1'))+nb_elmts(f2'))))
        /\(!(lire(f1')<lire(f2'))->
           trie(f1')/\trie(avancer(f2'))/\trie(ecrire(f,lire(f2')))
           /\(dernier(ecrire(f,lire(f2')))<=lire(f1'))
           /\(dernier(ecrire(f,lire(f2')))<=lire(avancer(f2')))
           /\(elmts(f1)+elmts(f2)=elmts(ecrire(f,lire(f2')))+elmts(f1')
                                  +elmts(avancer(f2')))
           /\(nb_elmts(f1')+nb_elmts(avancer(f2'))<val3)
           /\(wfs(nb_elmts(f1')+nb_elmts(avancer(f2')))))

Considérons d'abord lire(f1')<lire(f2')
- Si reste_elmt(f1')/\trie(f1') alors, trie(avancer(f1')) (reste_elmt(f1') est important car sinon, avancer(f1') n'est pas définie)
- Bien entendu trie(f2')->trie(f2')
- Si trie(f)/\(dernier(f)<=lire(f1')) alors, trie(ecrire(f,lire(f1'))). En effet, les axiomes de trie sont :
```
trie(fichier_vide)=vrai
trie(ecrire(f,e))=trie(f)/\(dernier(f)<=e)
    
```
- Nous avons trie(f1'), et par les axiomes de dernier ci-dessous, dernier(ecrire(f,lire(f1'))) vaut lire(f1'). Par conséquent, dernier(ecrire(f,lire(f1')))<=lire(avancer(f1')).
```
dernier(fichier_vide)=-inf
dernier(ecrire(f,e))=e
    
```
- Nous avons lire(f1')<lire(f2'), donc dernier(ecrire(f,lire(f1')))<=lire(f2') par les axiomes de dernier.
- Par les axiomes de elmts, nous avons elmts(ecrire(f,lire(f1')))+elmts(avancer(f1'))= elmts(f)+elmts(f1'). Alors, sous l'hypothèse elmts(f1)+elmts(f2)=elmts(f)+elmts(f1')+elmts(f2'), nous obtenons : elmts(f1)+elmts(f2)= elmts(ecrire(f,lire(f1')))+elmts(avancer(f1'))+elmts(f2')
- Nous avons nb_elmts(f1')+nb_elmts(f2')=val3, et par les axiomes de nb_elmts :
```
nb_elmts(fichier_vide)=0
nb_elmts(ecrire(f,e))=nb_elmts(f)+1
nb_elmts(avancer(f))=nb_elmts(f)-1
    
```
  Alors, nb_elmts(avancer(f1'))+nb_elmts(f2')= nb_elmts(f1')-1+nb_elmts(f2'), ce qui donne nb_elmts(avancer(f1'))+nb_elmts(f2')<val3
- Enfin, puisque rester_elmt(f1'), nb_elmts(avancer(f1'))>=0. De plus, par définition de nb_elmts, celle-ci est à valeurs entières naturelles, donc wfs(nb_elmts(avancer(f1'))+nb_elmts(f2'))
Le cas !(lire(f1')<lire(f2')) est symétrique

Preuve de la post-condition pour la première boucle

        trie(f1')/\trie(f2')/\trie(f)/\(dernier(f)<=lire(f1'))
        /\(dernier(f)<=lire(f2'))
        /\(elmts(f1)+elmts(f2)=elmts(f)+elmts(f1')+elmts(f2'))
        /\!((reste_elmt(f1')/\reste_elmt(f2')))
[6]	------------------- implies -------------------
	((reste_elmt(f1'))->
             trie(f1')/\trie(f)/\(dernier(f)<=lire(f1'))
             /\(elmts(f1)+elmts(f2)=elmts(f)+elmts(f1'))
             /\wfs(nb_elmts(f1')))
        /\(!(reste_elmt(f1'))->
             trie(f2')/\trie(f)/\(dernier(f)<=lire(f2'))
             /\(elmts(f1)+elmts(f2)=elmts(f)+elmts(f2'))
             /\wfs(nb_elmts(f2')))

Considérons le cas reste_elmt(f1')
- Notons que !((reste_elmt(f1')/\reste_elmt(f2'))) et reste_elmt(f1') donne !(reste_elmnt(f2')). Par les axiomes de elmts, nous avons alors elmts(f2')={}. Alors, sachant que elmts(f1)+elmts(f2)=elmts(f)+elmts(f1')+elmts(f2')), nous déduisons elmts(f1)+elmts(f2)=elmts(f)+elmts(f1')
- wfs(nb_elmts(f1')) est vraie par la définition de nb_elmts qui est à valeurs entières naturelles
- Les autres sous-formules se déduisent aisément
Le cas !(reste_elmt(f1')) est symétrique

Preuve d'invariance pour la seconde boucle

	trie(f1')/\trie(f)/\(dernier(f)<=lire(f1'))
        /\(elmts(f1)+elmts(f2)=elmts(f)+elmts(f1'))
        /\(reste_elmt(f1'))/\(nb_elmts(f1')=val1)/\(wfs(nb_elmts(f1')))
[1]	------------------- implies -------------------
	trie(avancer(f1'))/\trie(ecrire(f,lire(f1')))
        /\(dernier(ecrire(f,lire(f1')))<=lire(avancer(f1')))
        /\(elmts(f1)+elmts(f2)=elmts(ecrire(f,lire(f1')))
                               +elmts(avancer(f1')))
        /\(nb_elmts(avancer(f1'))<val1)/\(wfs(nb_elmts(avancer(f1'))))

Nous avons trie(f1') et reste_elmts(f1')m donc trie(avancer(f1')) est vraie
Par trie(f) et dernier(f)<=lire(f1') nous avons trie(ecrire(f,lire(f1')))
dernier(ecrire(f,lire(f1')))<=lire(avancer(f1')) se déduit de trie(f1') d'une part et reste_elmt(f1') d'autre part
elmts(f1)+elmts(f2)=elmts(ecrire(f,lire(f1'))) +elmts(avancer(f1')) vient des axiomes comme expliqué pour la preuve de [5]
les autres sous-formules sont aisées à prouver

Post-condition pour la seconde boucle

        trie(f1')/\trie(f)/\(dernier(f)<=lire(f1'))
        /\(elmts(f1)+elmts(f2)=elmts(f)+elmts(f1'))/\!((reste_elmt(f1')))
[2]	------------------- implies -------------------
	trie(f)/\(elmts(f)=elmts(f1)+elmts(f2))

Par définition des axiomes de elmts, puisque !(reste_elmt(f1')), nous avons elmts(f1')={}. Alors nous déduisons elmts(f)=elmts(f1)+elmts(f2) sachant elmts(f1)+elmts(f2)=elmts(f)+elmts(f1')
Les autres sous-formules se déduisent aisément

Cas de la troisième boucle

La dernière boucle est symétrique à la précédente : il suffit d'inverser les rôles de f1' et de f2'.

herbrete@enseirb.fr

Last modified: Tue Dec 13 17:21:18 CET 2005