mergesort_list.mlw 2.51 KB
Newer Older
1 2 3

(* Sorting a list of integers using mergesort *)

4
module Elt
5

6 7 8 9
  use export int.Int
  use export list.Length
  use export list.Append
  use export list.Permut
10

11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70
  type elt
  predicate le elt elt
  clone relations.TotalPreOrder with type t = elt, predicate rel = le
  clone export list.Sorted      with type t = elt, predicate le  = le

end

module Merge

  use export Elt

  let rec merge (l1 l2: list elt) : list elt
    requires { sorted l1 /\ sorted l2 }
    ensures  { sorted result /\ permut result (l1 ++ l2) }
    variant  { length l1 + length l2 }
  = match l1, l2 with
    | Nil, _ -> l2
    | _, Nil -> l1
    | Cons x1 r1, Cons x2 r2 ->
       if le x1 x2 then Cons x1 (merge r1 l2) else Cons x2 (merge l1 r2)
    end

end

(* TODO: proof to be completed
module EfficientMerge

  use export Elt
  use import list.Mem
  use import list.Reverse
  use import list.RevAppend

  let rec merge_aux (acc l1 l2: list elt) : list elt
    requires { sorted (reverse acc) /\ sorted l1 /\ sorted l2 }
    requires { forall x y: elt. mem x acc -> mem y l1 -> le x y }
    requires { forall x y: elt. mem x acc -> mem y l2 -> le x y }
    ensures  { sorted result /\ permut result (acc ++ l1 ++ l2) }
    variant  { length l1 + length l2 }
  = match l1, l2 with
    | Nil, _ -> rev_append acc l2
    | _, Nil -> rev_append acc l1
    | Cons x1 r1, Cons x2 r2 ->
       if le x1 x2 then merge_aux (Cons x1 acc) r1 l2
                   else merge_aux (Cons x2 acc) l1 r2
    end

  let merge (l1 l2: list elt) : list elt
    requires { sorted l1 /\ sorted l2 }
    ensures  { sorted result /\ permut result (l1 ++ l2) }
  =
    merge_aux Nil l1 l2

end
*)

module Mergesort

  use import Merge

  let split (l0: list 'a) : (list 'a, list 'a)
71
    requires { length l0 >= 2 }
72
    ensures  { let (l1, l2) = result in
73
      1 <= length l1 /\ 1 <= length l2 /\ permut l0 (l1 ++ l2) }
74
  = let rec split_aux (l1 l2 l: list 'a) : (list 'a, list 'a)
75
      requires { length l2 = length l1 \/ length l2 = length l1 + 1 }
76
      ensures  { let r1, r2 = result in
77 78
        (length r2 = length r1 \/ length r2 = length r1 + 1) /\
        permut (r1 ++ r2) (l1 ++ (l2 ++ l)) }
79
      variant { length l }
80
    = match l with
81 82 83 84 85
      | Nil -> (l1, l2)
      | Cons x r -> split_aux l2 (Cons x l1) r
      end
    in
    split_aux Nil Nil l0
86

87
  let rec mergesort (l: list elt) : list elt
88
    ensures { sorted result /\ permut result l }
89
    variant { length l }
90
  = match l with
91 92
      | Nil | Cons _ Nil -> l
      | _ -> let l1, l2 = split l in merge (mergesort l1) (mergesort l2)
93 94
    end

95
end