correct merge sort, now with is_sorted proof

Author: cp526

tests/cn/mergesort.c

@@ -1,6 +1,6 @@
 struct node {
   int value;
-  struct node* next;
+  struct node *next;
 };
 
 /*@
@@ -25,7 +25,7 @@ function [rec] ({list fst, list snd}) cn_split(list xs) {
       {fst: Nil {}, snd: Nil {}}
     }
     Cons {head: h1, tail: Nil {}} => {
-      {fst: Nil {}, snd: xs}
+      {fst: xs, snd: Nil {}}
     }
     Cons {head: h1, tail: Cons {head : h2, tail : tl2 }} => {
       let P = cn_split(tl2);
@@ -37,22 +37,23 @@ function [rec] ({list fst, list snd}) cn_split(list xs) {
 
 function [rec] (list) cn_merge(list xs, list ys) {
   match xs {
-      Nil {} => { 
-        ys 
-      }
-      Cons {head: x, tail: xs1} => {
-	match ys {
-	  Nil {} => { 
-            xs 
+    Nil {} => {
+      ys
+    }
+    Cons {head: x, tail: xs_} => {
+      match ys {
+        Nil {} => {
+          xs
+        }
+        Cons {head: y, tail: ys_} => {
+          if (x <= y) {
+            Cons {head: x, tail: cn_merge(xs_, ys)}
+          } else {
+            Cons {head: y, tail: cn_merge(xs, ys_)}
           }
-	  Cons { head: y, tail: ys1} => {
-	    let tail = cn_merge(xs1, ys1);
-	    (x < y) ?
-	    (Cons { head: x, tail: Cons {head: y, tail: tail}})
-	    : (Cons { head: y, tail: Cons {head: x, tail: tail}})
-	  }
-	}
+        }
       }
+    }
   }
 }
 
@@ -72,11 +73,44 @@ function [rec] (list) cn_mergesort(list xs) {
     }
   }
 }
+
+function (boolean) smaller (i32 head, list xs) {
+  match xs {
+    Nil {} => {
+      true
+    }
+    Cons {head : x, tail : _} => {
+      head <= x
+    }
+  }
+}
+
+function [rec] (boolean) is_sorted(list xs) {
+  match xs {
+    Nil {} => { 
+      true 
+    }
+    Cons {head: head, tail: tail} => { 
+      smaller (head, tail) && is_sorted(tail)
+    }
+  }
+}
+
+function (list) tl (list xs) {
+  match xs {
+    Nil {} => {
+      Nil {}
+    }
+    Cons {head : _, tail : tail} => {
+      tail
+    }
+  }
+}
 @*/
 
 struct node_pair {
-  struct node* fst;
-  struct node* snd;
+  struct node *fst;
+  struct node *snd;
 };
 
 struct node_pair split(struct node *xs)
@@ -92,7 +126,7 @@ struct node_pair split(struct node *xs)
   } else {
     struct node *cdr = xs->next;
     if (cdr == 0) {
-      struct node_pair r = {.fst = 0, .snd = xs};
+      struct node_pair r = {.fst = xs, .snd = 0};
       return r;
     } else {
       struct node_pair p = split(cdr->next);
@@ -104,7 +138,7 @@ struct node_pair split(struct node *xs)
   }
 }
 
-struct node* merge(struct node *xs, struct node *ys)
+struct node *merge(struct node *xs, struct node *ys)
 /*@ requires take Xs = List(xs); @*/
 /*@ requires take Ys = List(ys); @*/
 /*@ ensures take Zs = List(return); @*/
@@ -113,25 +147,18 @@ struct node* merge(struct node *xs, struct node *ys)
   /*@ unfold cn_merge(Xs, Ys); @*/
   if (xs == 0) {
     return ys;
+  } else if (ys == 0) {
+    return xs;
+  } else if (xs->value <= ys->value) {
+    xs->next = merge(xs->next, ys);
+    return xs;
   } else {
-    if (ys == 0) {
-      return xs;
-    } else {
-      struct node *zs = merge(xs->next, ys->next);
-      if (xs->value < ys->value) {
-	xs->next = ys;
-	ys->next = zs;
-	return xs;
-      } else {
-	ys->next = xs;
-	xs->next = zs;
-	return ys;
-      }
-    }
+    ys->next = merge(xs, ys->next);
+    return ys;
   }
 }
 
-struct node* naive_mergesort(struct node *xs)
+struct node *naive_mergesort(struct node *xs)
 /*@ requires take Xs = List(xs); @*/
 /*@ ensures take Ys = List(return); @*/
 /*@ ensures Ys == cn_mergesort(Xs); @*/
@@ -149,6 +176,9 @@ struct node* naive_mergesort(struct node *xs)
   }
 }
 
+
+
+
 int main(void)
 /*@ trusted; @*/
 {
@@ -158,3 +188,57 @@ int main(void)
 
   struct node *sorted_i1 = naive_mergesort(&i1);
 }
+
+
+
+
+
+void prove_merge_sorted(struct node *p, struct node *q)
+/*@ requires take xs_in = List(p);
+             take ys_in = List(q);
+             is_sorted(xs_in);
+             is_sorted(ys_in);
+             let merged = cn_merge(xs_in, ys_in);
+    ensures  take xs_out = List(p);
+             take ys_out = List(q);
+             xs_out == xs_in && ys_out == ys_in;
+             is_sorted(merged);
+@*/
+{
+  /* Unfold the definition of `merged`. */
+  /*@ unfold cn_merge(xs_in, ys_in); @*/
+
+  /* If either list is empty, cn_merge just picks the other, which is
+     sorted by assumption, so nothing left to do. */
+  if (p == 0 || q == 0) {
+    return;
+  } 
+  /* For non-empty lists, cn_merge picks the smaller head and merges
+     the rest. */
+  else {
+    /* If `xs_in` has the smaller head, it merges `tl(xs_in)` with
+       `ys_in`. */
+    if (p->value <= q->value) {
+      /* By induction hypothesis (IH) `cn_merge(tl(xs_in), ys_in))` is
+         sorted. To "apply" IH, expand the definition of
+         `is_sorted(xs_in)` to prove `is_sorted(tl(xs_in))`. */
+      /*@ unfold is_sorted(xs_in); @*/
+      prove_merge_sorted(p->next, q);
+      /* By definition of `cn_merge(tl(xs_in), ys_in)`, that merged
+         list starts with the minimum of either head, ... */
+      /*@ unfold cn_merge(tl(xs_in), ys_in); @*/
+      /* ... so that list with `hd(xs_in)` cons'ed on is also
+         sorted. @*/
+      /*@ unfold is_sorted(merged); @*/
+      return;
+    }
+    else {
+      /* This is symmetric to the proof above. */
+      /*@ unfold is_sorted(ys_in); @*/
+      prove_merge_sorted(p, q->next);
+      /*@ unfold cn_merge(xs_in, tl(ys_in)); @*/
+      /*@ unfold is_sorted(merged); @*/
+      return;
+    }
+  }
+}