completed proof of mergesort_queue

examples/mergesort_queue.mlw

 
+(** {1 Sorting a queue using mergesort}
+
+    Author: Jean-Christophe Filliâtre (CNRS) *)
+
 module MergesortQueue
 
   use import int.Int
+  use import list.Mem
   use import list.Length
   use import list.Append
   use import list.Permut
@@ -9,19 +14,18 @@ module MergesortQueue
 
   type elt
   predicate le elt elt
-
-  axiom total_preorder1:
-    forall x y: elt. le x y \/ le y x
-  axiom total_preorder2:
-    forall x y z: elt. le x y -> le y z -> le x z
-
-  clone import list.Sorted with type t = elt, predicate le = le
+  clone relations.TotalPreOrder with type t = elt, predicate rel = le
+  clone export list.Sorted      with type t = elt, predicate le  = le
 
   let merge (q1: t elt) (q2: t elt) (q: t elt)
-    requires { q.elts = Nil (* /\ sorted q1.elts /\ sorted q2.elts *) }
-    ensures { permut q.elts (old q1.elts ++ old q2.elts) }
+    requires { q.elts = Nil /\ sorted q1.elts /\ sorted q2.elts }
+    ensures  { sorted q.elts }
+    ensures  { permut q.elts (old q1.elts ++ old q2.elts) }
   = 'L:
     while length q1 > 0 || length q2 > 0 do
+      invariant { sorted q1.elts /\ sorted q2.elts /\ sorted q.elts }
+      invariant { forall x y: elt. mem x q.elts -> mem y q1.elts -> le x y }
+      invariant { forall x y: elt. mem x q.elts -> mem y q2.elts -> le x y }
       invariant { permut (q.elts ++ q1.elts ++ q2.elts)
                          (at q1.elts 'L ++ at q2.elts 'L) }
       variant { length q1 + length q2 }
@@ -38,26 +42,27 @@ module MergesortQueue
           push (safe_pop q2) q
     done
 
-(*
-  let rec mergesort (q: t elt)
-    requires { }
-    ensures { (* sorted q.elts /\ *) permut q.elts (old q.elts) }
+  let rec mergesort (q: t elt) : unit
+    ensures { sorted q.elts /\ permut q.elts (old q.elts) }
+    variant { length q }
   = 'L:
     if length q > 1 then begin
       let q1 = create () : t elt in
       let q2 = create () : t elt in
       while not (is_empty q) do
         invariant { permut (q1.elts ++ q2.elts ++ q.elts) (at q.elts 'L) }
-        variant { length q.elts }
-        let x = pop q in push x q1;
-        if not (is_empty q) then let x = pop q in push x q2
+        invariant { length q1 = length q2 \/
+                    length q = 0 /\ length q1 = length q2 +1 }
+        variant   { length q }
+        let x = safe_pop q in push x q1;
+        if not (is_empty q) then let x = safe_pop q in push x q2
       done;
       assert { q.elts = Nil };
       assert { permut (q1.elts ++ q2.elts) (at q.elts 'L) };
       mergesort q1;
       mergesort q2;
       merge q1 q2 q
-    end
-*)
+    end else
+      assert { q.elts = Nil \/ exists x: elt. q.elts = Cons x Nil }
 
 end