Problème — Le tri par partition-fusion sur tableaux : coût exact et stabilité

1. Le tri.

(* Trie t par ordre croissant, en place, à l'aide d'un tampon de taille n.
   Précondition : aucune. Complexité : Theta(n log n) en temps, Theta(n) en espace.
   Le tampon est alloué UNE fois : une allocation par appel récursif ferait
   n log n allocations pour rien. *)
let tri_fusion t =
  let n = Array.length t in
  if n > 1 then begin
    let tampon = Array.make n t.(0) in
    let rec trier g d =                       (* trie t.[g .. d-1] *)
      if d - g > 1 then begin
        let m = g + (d - g) / 2 in
        trier g m; trier m d;
        let i = ref g and j = ref m and k = ref g in
        (* INVARIANT : tampon.[g .. k-1] contient, triés, les éléments déjà pris
           dans t.[g .. i-1] et t.[m .. j-1]. *)
        while !i < m && !j < d do
          if t.(!i) <= t.(!j)                 (* <= et non < : voir question 3 *)
          then begin tampon.(!k) <- t.(!i); incr i end
          else begin tampon.(!k) <- t.(!j); incr j end;
          incr k
        done;
        while !i < m do tampon.(!k) <- t.(!i); incr i; incr k done;
        while !j < d do tampon.(!k) <- t.(!j); incr j; incr k done;
        Array.blit tampon g t g (d - g)
      end
    in trier 0 n
  end

Terminaison : variant $d-g$, divisé par deux à chaque appel ; les trois boucles ont pour variant $(m-i)+(d-j)$. Correction : l'invariant écrit ci-dessus, plus le fait que les deux moitiés sont triées par hypothèse de récurrence.