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 : Alors, il est nécessaire et suffisant que les propriétés suivantes soient vraies à chaque itération de la boucle while :

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 :

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 : De plus, nous ferons les hypothèses suivantes :

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

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

Première boucle

Deuxième boucle

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

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))

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')))))
  1. Considérons d'abord lire(f1')<lire(f2')
  2. 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')))
  1. Considérons le cas reste_elmt(f1')
  2. 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'))))

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))
  1. 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')
  2. 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