Dafny renditions of sorting algorithms proved in other provers (Coq, Isabelle, F*)

6 files changed, 1176 insertions, 0 deletions

diff --git a/Test/alltests.txt b/Test/alltests.txt
index 8ecf0e25..6edb80fb 100644
--- a/Test/alltests.txt
+++ b/Test/alltests.txt
@@ -2,6 +2,7 @@ dafny0           Use    Dafny functionality tests
 dafny1           Use    Various Dafny examples

 dafny2           Use    More Dafny examples

 dafny3           Use    And more Dafny examples

+dafny4           Use    More, more, more!

 VSI-Benchmarks   Use    Solutions to Verified Software Initiative verification challenges

 vacid0           Use    Dafny attempts to VACID Edition 0 benchmarks

 vstte2012        Use    Dafny solutions for the VSTTE 2012 program verification competition

diff --git a/Test/dafny4/Answer b/Test/dafny4/Answer
new file mode 100644
index 00000000..0e983953
--- /dev/null
+++ b/Test/dafny4/Answer
@@ -0,0 +1,12 @@
+
+-------------------- CoqArt-InsertionSort.dfy --------------------

+

+Dafny program verifier finished with 36 verified, 0 errors

+
+-------------------- GHC-MergeSort.dfy --------------------

+

+Dafny program verifier finished with 85 verified, 0 errors

+
+-------------------- Fstar-QuickSort.dfy --------------------

+

+Dafny program verifier finished with 6 verified, 0 errors

diff --git a/Test/dafny4/CoqArt-InsertionSort.dfy b/Test/dafny4/CoqArt-InsertionSort.dfy
new file mode 100644
index 00000000..9ed57e98
--- /dev/null
+++ b/Test/dafny4/CoqArt-InsertionSort.dfy
@@ -0,0 +1,192 @@
+// Dafny transcription of the Coq development of insertion sort, as found in Coq'Art.

+

+datatype List<T> = Nil | Cons(head: T, tail: List)

+

+predicate sorted(l: List<int>)

+{

+  match l

+  case Nil => true

+  case Cons(x, rest) =>

+    match rest

+    case Nil => true

+    case Cons(y, _) => x <= y && sorted(rest)

+}

+

+lemma example_sort_2357()

+  ensures sorted(Cons(2, Cons(3, Cons(5, Cons(7, Nil)))));

+{

+}

+

+lemma sorted_inv(z: int, l: List<int>)

+  requires sorted(Cons(z, l));

+  ensures sorted(l);

+{

+  match l {

+    case Nil =>

+    case Cons(_, _) =>

+  }

+}

+

+// Number of occurrences of z in l

+function nb_occ(z: int, l: List<int>): nat

+{

+  match l

+  case Nil => 0

+  case Cons(z', l') =>

+    (if z == z' then 1 else 0) + nb_occ(z, l')

+}

+

+lemma example_nb_occ_0()

+  ensures nb_occ(3, Cons(3, Cons(7, Cons(3, Nil)))) == 2;

+{

+}

+

+lemma example_nb_occ_1()

+  ensures nb_occ(36725, Cons(3, Cons(7, Cons(3, Nil)))) == 0;

+{

+}

+

+// list l' is a permutation of list l

+predicate equiv(l: List<int>, l': List<int>)

+{

+  forall z :: nb_occ(z, l) == nb_occ(z, l')

+}

+

+// equiv is an equivalence

+lemma equiv_refl(l: List<int>)

+  ensures equiv(l, l);

+{

+}

+

+lemma equiv_sym(l: List<int>, l': List<int>)

+  requires equiv(l, l');

+  ensures equiv(l', l);

+{

+}

+

+lemma equiv_trans(l: List<int>, l': List<int>, l'': List<int>)

+  requires equiv(l, l') && equiv(l', l'');

+  ensures equiv(l, l'');

+{

+}

+

+lemma equiv_cons(z: int, l: List<int>, l': List<int>)

+  requires equiv(l, l');

+  ensures equiv(Cons(z, l), Cons(z, l'));

+{

+}

+

+lemma equiv_perm(a: int, b: int, l: List<int>, l': List<int>)

+  requires equiv(l, l');

+  ensures equiv(Cons(a, Cons(b, l)), Cons(b, Cons(a, l')));

+{

+  var L, L' := Cons(a, Cons(b, l)), Cons(b, Cons(a, l'));

+  forall z {

+    calc {

+      nb_occ(z, L);

+      (if z == a && z == b then 2 else if z == a || z == b then 1 else 0) + nb_occ(z, l);

+      (if z == a && z == b then 2 else if z == a || z == b then 1 else 0) + nb_occ(z, l');

+      nb_occ(z, L');

+    }

+  }

+}

+

+// insertion of z into l at the right place (assuming l is sorted)

+function method aux(z: int, l: List<int>): List<int>

+{

+  match l

+  case Nil => Cons(z, Nil)

+  case Cons(a, l') =>

+    if z <= a then Cons(z, l) else Cons(a, aux(z, l'))

+}

+

+lemma example_aux_0()

+  ensures aux(4, Cons(2, Cons(5, Nil))) == Cons(2, Cons(4, Cons(5, Nil)));

+{

+}

+

+lemma example_aux_1()

+  ensures aux(4, Cons(24, Cons(50, Nil))) == Cons(4, Cons(24, Cons(50, Nil)));

+{

+}

+

+// the aux function seems to be a good tool for sorting...

+

+lemma aux_equiv(l: List<int>, x: int)

+  ensures equiv(Cons(x, l), aux(x, l));

+{

+  match l {

+    case Nil =>

+    case Cons(_, _) =>

+  }

+}

+

+lemma aux_sorted(l: List<int>, x: int)

+  requires sorted(l);

+  ensures sorted(aux(x, l));

+{

+  match l {

+    case Nil =>

+    case Cons(_, l') =>

+      match l' {

+        case Nil =>

+        case Cons(_, _) =>

+      }

+  }

+}

+

+// the sorting function

+function sort(l: List<int>): List<int>

+  ensures var l' := sort(l); equiv(l, l') && sorted(l');

+{

+  existence_proof(l);

+  var l' :| equiv(l, l') && sorted(l'); l'

+}

+

+lemma existence_proof(l: List<int>)

+  ensures exists l' :: equiv(l, l') && sorted(l');

+{

+  match l {

+    case Nil =>

+    case Cons(x, m) =>

+      existence_proof(m);

+      var m' :| equiv(m, m') && sorted(m');

+      calc ==> {

+        equiv(m, m') && sorted(m');

+        equiv(l, Cons(x, m')) && sorted(m');

+        { aux_equiv(m', x); }

+        equiv(l, aux(x, m')) && sorted(m');

+        { aux_sorted(m', x); }

+        equiv(l, aux(x, m')) && sorted(aux(x, m'));

+      }

+  }

+}

+

+// to get a compilable function in Dafny

+function method Sort(l: List<int>): List<int>

+  ensures equiv(l, Sort(l)) && sorted(Sort(l));

+{

+  match l

+  case Nil => l

+  case Cons(x, m) =>

+    var m' := Sort(m);

+    assert equiv(l, Cons(x, m'));

+    aux_equiv(m', x);

+    aux_sorted(m', x);

+    aux(x, m')

+}

+

+predicate p_aux_equiv(l: List<int>, x: int)

+  ensures equiv(Cons(x, l), aux(x, l));

+{

+  aux_equiv(l, x);

+  true

+}

+

+predicate p_aux_sorted(l: List<int>, x: int)

+  requires sorted(l);

+  ensures sorted(aux(x, l));

+{

+  aux_sorted(l, x);

+  true

+}

diff --git a/Test/dafny4/Fstar-QuickSort.dfy b/Test/dafny4/Fstar-QuickSort.dfy
new file mode 100644
index 00000000..b9cdc0dd
--- /dev/null
+++ b/Test/dafny4/Fstar-QuickSort.dfy
@@ -0,0 +1,126 @@
+// A Dafny rendition of an F* version of QuickSort (included at the bottom of this file).

+// Unlike the F* version, Dafny also proves termination and does not use any axioms.  However,

+// Dafny needs help with a couple of lemmas in places where F* does not need them.

+// Comments below show differences between the F* and Dafny versions.

+

+datatype Pair<T, U> = P(T, U)

+

+datatype List<T> = Nil | Cons(T, List)

+

+function length(list: List): nat  // for termination proof

+{

+  match list

+  case Nil => 0

+  case Cons(_, tl) => 1 + length(tl)

+}

+

+// In(x, list) returns the number of occurrences of x in list

+function In(x: int, list: List<int>): nat

+{

+  match list

+  case Nil => 0

+  case Cons(y, tl) => (if x == y then 1 else 0) + In(x, tl)

+}

+

+predicate SortedRange(m: int, n: int, list: List<int>)

+  decreases list;  // for termination proof

+{

+  match list

+  case Nil => m <= n

+  case Cons(hd, tl) => m <= hd <= n && SortedRange(hd, n, tl)

+}

+

+function append(n0: int, n1: int, n2: int, n3: int, i: List<int>, j: List<int>): List<int>

+  requires n0 <= n1 <= n2 <= n3;

+  requires SortedRange(n0, n1, i) && SortedRange(n2, n3, j);

+  ensures SortedRange(n0, n3, append(n0, n1, n2, n3, i, j));

+  ensures forall x :: In(x, append(n0, n1, n2, n3, i, j)) == In(x, i) + In(x, j);

+  decreases i;  // for termination proof

+{

+  match i

+  case Nil => j

+  case Cons(hd, tl) => Cons(hd, append(hd, n1, n2, n3, tl, j))

+}

+

+function partition(x: int, l: List<int>): Pair<List<int>, List<int>>

+  ensures var P(lo, hi) := partition(x, l);

+    (forall y :: In(y, lo) == if y <= x then In(y, l) else 0) &&

+    (forall y :: In(y, hi) == if x < y then In(y, l) else 0) &&

+    length(l) == length(lo) + length(hi);  // for termination proof

+{

+  match l

+  case Nil => P(Nil, Nil)

+  case Cons(hd, tl) =>

+    var P(lo, hi) := partition(x, tl);

+    if hd <= x then

+      P(Cons(hd, lo), hi)

+    else

+      P(lo, Cons(hd, hi))

+}

+

+function sort(min: int, max: int, i: List<int>): List<int>

+  requires min <= max;

+  requires forall x :: In(x, i) != 0 ==> min <= x <= max;

+  ensures SortedRange(min, max, sort(min, max, i));

+  ensures forall x :: In(x, i) == In(x, sort(min, max, i));

+  decreases length(i);  // for termination proof

+{

+  match i

+  case Nil => Nil

+  case Cons(hd, tl) =>

+    assert In(hd, i) != 0;  // this proof line not needed in F*

+    var P(lo, hi) := partition(hd, tl);

+    assert forall y :: In(y, lo) <= In(y, i);  // this proof line not needed in F*

+    var i' := sort(min, hd, lo);

+    var j' := sort(hd, max, hi);

+    append(min, hd, hd, max, i', Cons(hd, j'))

+}

+

+/*

+module Sort

+

+type SortedRange : int => int => list int => E

+assume Nil_Sorted : forall (n:int) (m:int). n <= m <==> SortedRange n m [] 

+assume Cons_Sorted: forall (n:int) (m:int) (hd:int) (tl:list int). 

+               SortedRange hd m tl && (n <= hd) && (hd <= m)

+          <==> SortedRange n m (hd::tl)

+

+val append: n1:int -> n2:int{n1 <= n2} -> n3:int{n2 <= n3} -> n4:int{n3 <= n4} 

+         -> i:list int{SortedRange n1 n2 i} 

+         -> j:list int{SortedRange n3 n4 j}

+         -> k:list int{SortedRange n1 n4 k 

+                      /\ (forall x. In x k <==> In x i \/ In x j)}

+let rec append n1 n2 n3 n4 i j = match i with 

+  | [] -> 

+    (match j with

+      | [] -> j

+      | _::_ -> j)

+  | hd::tl -> hd::(append hd n2 n3 n4 tl j)

+

+val partition: x:int

+            -> l:list int

+            -> (lo:list int

+                * hi:list int{(forall y. In y lo ==> y <= x /\ In y l)

+                               /\ (forall y. In y hi ==> x < y /\ In y l)

+                               /\ (forall y. In y l ==> In y lo \/ In y hi)})

+let rec partition x l = match l with

+  | [] -> ([], [])

+  | hd::tl ->

+    let lo, hi = partition x tl in

+    if hd <= x

+    then (hd::lo, hi)

+    else (lo, hd::hi)

+

+val sort: min:int  

+       -> max:int{min <= max} 

+       -> i:list int {forall x. In x i ==> (min <= x /\ x <= max)}

+       -> j:list int{SortedRange min max j /\ (forall x. In x i <==> In x j)}

+let rec sort min max i = match i with

+  | [] -> []

+  | hd::tl ->

+    let lo,hi = partition hd tl in

+    let i' = sort min hd lo in 

+    let j' = sort hd max hi in

+    append min hd hd max i' (hd::j')

+

+*/

diff --git a/Test/dafny4/GHC-MergeSort.dfy b/Test/dafny4/GHC-MergeSort.dfy
new file mode 100644
index 00000000..1f578593
--- /dev/null
+++ b/Test/dafny4/GHC-MergeSort.dfy
@@ -0,0 +1,838 @@
+// Rustan Leino

+// 23 Dec 2013 (completed in 5 hours, but is missing the formulation and proof that the

+// sorting algorithm is stable, which the journal article below does and says is the most interesting

+// part).

+// 28 Dec 2013, added key function and stability (which took another 5 hours).

+// Inspiration to prove this algorithm comes from "Proof Pearl --- A Mechanized Proof of GHC's Mergesort"

+// by Christian Sternagel, Journal of Automation 51:357--370, 2013.

+

+// library

+

+datatype List<T> = Nil | Cons(head: T, tail: List)

+

+function length(xs: List): nat

+{

+  match xs

+  case Nil => 0

+  case Cons(_, ys) => 1 + length(ys)

+}

+

+// returns xs-backwards followed-by acc

+function method reverse(xs: List, acc: List): List

+{

+  match xs

+  case Nil => acc

+  case Cons(a, ys) => reverse(ys, Cons(a, acc))

+}

+

+function multiset_of<T>(xs: List<T>): multiset<T>

+{

+  match xs

+  case Nil => multiset{}

+  case Cons(a, ys) => multiset{a} + multiset_of(ys)

+}

+

+function MultisetUnion<T>(xs: List<List<T>>): multiset<T>

+{

+  match xs

+  case Nil => multiset{}

+  case Cons(a, ys) => multiset_of(a) + MultisetUnion(ys)

+}

+

+function append(xs: List, ys: List): List

+{

+  match xs

+  case Nil => ys

+  case Cons(a, xs') => Cons(a, append(xs', ys))

+}

+

+lemma append_associative(xs: List, ys: List, zs: List)

+  ensures append(xs, append(ys, zs)) == append(append(xs, ys), zs);

+{

+}

+

+lemma append_Nil(xs: List)

+  ensures append(xs, Nil) == xs;

+{

+}

+

+function flatten(x: List<List>): List

+{

+  match x

+  case Nil => Nil

+  case Cons(xs, y) => append(xs, flatten(y))

+}

+

+// The algorithm

+

+// Everything is parametric in G and key

+type G

+function method key(g: G): int

+

+predicate method Below(a: G, b: G)

+{

+  key(a) <= key(b)

+}

+

+function method sort(xs: List<G>): List<G>

+{

+  mergeAll(sequences(xs))

+}

+

+function method sequences(xs: List<G>): List<List<G>>

+  ensures sequences(xs) != Nil;

+  decreases xs, 0;

+{

+  match xs

+  case Nil => Cons(xs, Nil)

+  case Cons(a, ys) =>

+    match ys

+    case Nil => Cons(xs, Nil)

+    case Cons(b, zs) => if !Below(a, b) then descending(b, Cons(a, Nil), zs) else ascending(b, Cons(a, Nil), zs)

+}

+

+function method descending(a: G, xs: List<G>, ys: List<G>): List<List<G>>

+  ensures descending(a, xs, ys) != Nil;

+  decreases ys;

+{

+  if ys.Cons? && !Below(a, ys.head) then

+    descending(ys.head, Cons(a, xs), ys.tail)

+  else

+    Cons(Cons(a, xs), sequences(ys))

+}

+

+function method ascending(a: G, xs: List<G>, ys: List<G>): List<List<G>>

+  ensures ascending(a, xs, ys) != Nil;

+  decreases ys;

+{

+  if ys.Cons? && Below(a, ys.head) then

+    ascending(ys.head, Cons(a, xs), ys.tail)

+  else

+    Cons(reverse(Cons(a, xs), Nil), sequences(ys))

+}

+

+function method mergeAll(x: List<List<G>>): List<G>

+  requires x != Nil;

+  decreases length(x);

+{

+  if x.tail == Nil then

+    x.head

+  else

+    mergeAll(mergePairs(x))

+}

+

+function method mergePairs(x: List<List<G>>): List<List<G>>

+  ensures length(mergePairs(x)) <= length(x);

+  ensures x.Cons? && x.tail.Cons? ==> length(mergePairs(x)) < length(x);

+  ensures x != Nil ==> mergePairs(x) != Nil;

+{

+  if x.Cons? && x.tail.Cons? then

+    assert

+      length(Cons(merge(x.head, x.tail.head), mergePairs(x.tail.tail))) ==

+      1 + length(mergePairs(x.tail.tail));

+    Cons(merge(x.head, x.tail.head), mergePairs(x.tail.tail))

+  else

+    x

+}

+

+function method merge(xs: List<G>, ys: List<G>): List<G>

+{

+  match xs

+  case Nil => ys

+  case Cons(a, xs') =>

+    match ys

+    case Nil => xs

+    case Cons(b, ys') =>

+      if Below(a, b) then Cons(a, merge(xs', ys)) else Cons(b, merge(xs, ys'))

+}

+

+// the specification

+

+predicate sorted(xs: List<G>)

+{

+  match xs

+  case Nil => true

+  case Cons(a, ys) =>

+    (forall y :: y in multiset_of(ys) ==> Below(a, y)) &&  // using multiset_of instead of set_of, since we don't have a need for set_of elsewhere

+    sorted(ys)

+}

+

+function filter(g: G, xs: List<G>): List<G>

+{

+  match xs

+  case Nil => Nil

+  case Cons(b, ys) => if key(g) == key(b) then Cons(b, filter(g, ys)) else filter(g, ys)

+}

+

+predicate stable(xs: List<G>, ys: List<G>)

+{

+  forall g :: filter(g, xs) == filter(g, ys)  // I dropped the unnecessary antecedent "g in multiset_of(xs)" from the paper

+}

+

+lemma Correctness(xs: List<G>)

+  ensures sorted(sort(xs)) && multiset_of(sort(xs)) == multiset_of(xs) && stable(sort(xs), xs);

+{

+  calc {

+    multiset_of(sort(xs));

+    multiset_of(mergeAll(sequences(xs)));

+    { perm_mergeAll(sequences(xs)); }

+    MultisetUnion(sequences(xs));

+    { perm_sequences(xs); }

+    multiset_of(xs);

+  }

+  sorted_sort(xs);

+  forall g {

+    stable_sort(g, xs);

+  }

+}

+

+// permutation lemmas

+

+lemma perm_sequences(xs: List<G>)

+  ensures MultisetUnion(sequences(xs)) == multiset_of(xs);

+  decreases xs, 0;

+{

+  match xs {

+    case Nil =>

+    case Cons(a, ys) =>

+      match ys {

+        case Nil =>

+        case Cons(b, zs) =>

+          perm_descending(b, Cons(a, Nil), zs);

+          perm_ascending(b, Cons(a, Nil), zs);

+      }

+  }

+}

+

+lemma perm_descending(a: G, xs: List<G>, ys: List<G>)

+  ensures MultisetUnion(descending(a, xs, ys)) == multiset{a} + multiset_of(xs) + multiset_of(ys);

+  decreases ys;

+{

+  if ys.Cons? && !Below(a, ys.head) {

+    calc {

+      MultisetUnion(descending(a, xs, ys));

+      MultisetUnion(descending(ys.head, Cons(a, xs), ys.tail));

+      { perm_descending(ys.head, Cons(a, xs), ys.tail); }

+      multiset{ys.head} + multiset_of(Cons(a, xs)) + multiset_of(ys.tail);

+      multiset{a} + multiset_of(xs) + multiset_of(Cons(ys.head, ys.tail));

+    }

+  } else {

+    calc {

+      MultisetUnion(descending(a, xs, ys));

+      MultisetUnion(Cons(Cons(a, xs), sequences(ys)));

+      multiset_of(Cons(a, xs)) + MultisetUnion(sequences(ys));

+      { perm_sequences(ys); }

+      multiset_of(Cons(a, xs)) + multiset_of(ys);

+      multiset{a} + multiset_of(xs) + multiset_of(ys);

+    }

+  }

+}

+

+lemma perm_ascending(a: G, xs: List<G>, ys: List<G>)

+  ensures MultisetUnion(ascending(a, xs, ys)) == multiset{a} + multiset_of(xs) + multiset_of(ys);

+  decreases ys;

+{

+  if ys.Cons? && Below(a, ys.head) {

+    calc {

+      MultisetUnion(ascending(a, xs, ys));

+      MultisetUnion(ascending(ys.head, Cons(a, xs), ys.tail));

+      { perm_ascending(ys.head, Cons(a, xs), ys.tail); }

+      multiset{ys.head} + multiset_of(Cons(a, xs)) + multiset_of(ys.tail);

+      multiset{a} + multiset_of(xs) + multiset_of(Cons(ys.head, ys.tail));

+    }

+  } else {

+    calc {

+      MultisetUnion(ascending(a, xs, ys));

+      MultisetUnion(Cons(reverse(Cons(a, xs), Nil), sequences(ys)));

+      multiset_of(reverse(Cons(a, xs), Nil)) + MultisetUnion(sequences(ys));

+      { perm_sequences(ys); }

+      multiset_of(reverse(Cons(a, xs), Nil)) + multiset_of(ys);

+      { perm_reverse(Cons(a, xs), Nil); }

+      multiset_of(Cons(a, xs)) + multiset_of(Nil) + multiset_of(ys);

+      multiset{a} + multiset_of(xs) + multiset_of(ys);

+    }

+  }

+}

+

+lemma perm_reverse(xs: List, acc: List)

+  ensures multiset_of(reverse(xs, acc)) == multiset_of(xs) + multiset_of(acc);

+{

+}

+

+lemma perm_mergeAll(x: List<List<G>>)

+  requires x != Nil;

+  ensures multiset_of(mergeAll(x)) == MultisetUnion(x);

+  decreases length(x);

+{

+  if x == Nil {

+  } else if x.tail == Nil {

+  } else {

+    calc {

+      multiset_of(mergeAll(x));

+      multiset_of(mergeAll(mergePairs(x)));

+      { perm_mergeAll(mergePairs(x)); }

+      MultisetUnion(mergePairs(x));

+      { perm_mergePairs(x); }

+      MultisetUnion(x);

+    }

+  }

+}

+

+lemma perm_mergePairs(x: List<List<G>>)

+  ensures MultisetUnion(mergePairs(x)) == MultisetUnion(x);

+{

+  if x.Cons? && x.tail.Cons? {

+    calc {

+      MultisetUnion(mergePairs(x));

+      MultisetUnion(Cons(merge(x.head, x.tail.head), mergePairs(x.tail.tail)));

+      multiset_of(merge(x.head, x.tail.head)) + MultisetUnion(mergePairs(x.tail.tail));

+      { perm_mergePairs(x.tail.tail); }

+      multiset_of(merge(x.head, x.tail.head)) + MultisetUnion(x.tail.tail);

+      { perm_merge(x.head, x.tail.head); }

+      multiset_of(x.head) + multiset_of(x.tail.head) + MultisetUnion(x.tail.tail);

+      multiset_of(x.head) + MultisetUnion(Cons(x.tail.head, x.tail.tail));

+      multiset_of(x.head) + MultisetUnion(x.tail);

+      MultisetUnion(Cons(x.head, x.tail));

+      MultisetUnion(x);

+    }

+  }

+}

+

+lemma perm_merge(xs: List<G>, ys: List<G>)

+  ensures multiset_of(merge(xs, ys)) == multiset_of(xs) + multiset_of(ys);

+{

+  match xs {

+    case Nil =>

+    case Cons(a, xs') =>

+      match ys {

+        case Nil =>

+        case Cons(b, ys') =>

+          if Below(a, b) {

+            perm_merge(xs', ys);

+          } else {

+            perm_merge(xs, ys');

+          }

+      }

+  }

+}

+

+// sorted-ness lemmas

+

+lemma sorted_sort(xs: List<G>)

+  ensures sorted(sort(xs));

+{

+  sorted_sequences(xs);

+  sorted_mergeAll(sequences(xs));

+}

+

+predicate AllSorted(x: List<List<G>>)

+{

+  match x

+  case Nil => true

+  case Cons(xs, y) => sorted(xs) && AllSorted(y)

+}

+

+lemma sorted_sequences(xs: List<G>)

+  ensures AllSorted(sequences(xs));

+  decreases xs, 0;

+{

+  match xs {

+    case Nil =>

+    case Cons(a, ys) =>

+      match ys {

+        case Nil =>

+        case Cons(b, zs) =>

+          if !Below(a, b) {

+            sorted_descending(b, Cons(a, Nil), zs);

+          } else {

+            sorted_ascending(b, Cons(a, Nil), zs);

+          }

+      }

+  }

+}

+

+lemma sorted_descending(a: G, xs: List<G>, ys: List<G>)

+  requires (forall y :: y in multiset_of(xs) ==> Below(a, y)) && sorted(xs);

+  ensures AllSorted(descending(a, xs, ys));

+  decreases ys;

+{

+  if ys.Cons? && !Below(a, ys.head) {

+    sorted_descending(ys.head, Cons(a, xs), ys.tail);

+  } else {

+    calc {

+      AllSorted(Cons(Cons(a, xs), sequences(ys)));

+      sorted(Cons(a, xs)) && AllSorted(sequences(ys));

+      { sorted_sequences(ys); }

+      sorted(Cons(a, xs));

+      true;

+    }

+  }

+}

+

+lemma sorted_ascending(a: G, xs: List<G>, ys: List<G>)

+  requires (forall y :: y in multiset_of(xs) ==> Below(y, a)) && sorted(reverse(xs, Nil));

+  ensures AllSorted(ascending(a, xs, ys));

+  decreases ys;

+{

+  sorted_insertInMiddle(xs, a, Nil);

+  if ys.Cons? && Below(a, ys.head) {

+    sorted_ascending(ys.head, Cons(a, xs), ys.tail);

+  } else {

+    calc {

+      AllSorted(Cons(reverse(Cons(a, xs), Nil), sequences(ys)));

+      sorted(reverse(Cons(a, xs), Nil)) && AllSorted(sequences(ys));

+      { sorted_sequences(ys); }

+      sorted(reverse(Cons(a, xs), Nil));

+      true;

+    }

+  }

+}

+

+lemma sorted_reverse(xs: List<G>, ys: List<G>)

+  requires sorted(reverse(xs, ys));

+  ensures sorted(ys);

+  ensures forall a,b :: a in multiset_of(xs) && b in multiset_of(ys) ==> Below(a, b);

+{

+  match xs {

+    case Nil =>

+    case Cons(b, xs') =>

+      calc {

+        sorted(reverse(Cons(b, xs'), ys));

+        sorted(reverse(xs', Cons(b, ys)));

+      ==> { sorted_reverse(xs', Cons(b, ys)); }

+        sorted(Cons(b, ys));

+      ==>

+        sorted(ys);

+      }

+  }

+}

+

+lemma sorted_insertInMiddle(xs: List<G>, a: G, ys: List<G>)

+  requires sorted(reverse(xs, ys));

+  requires forall y :: y in multiset_of(xs) ==> Below(y, a);

+  requires forall y :: y in multiset_of(ys) ==> Below(a, y);

+  ensures sorted(reverse(xs, Cons(a, ys)));

+{

+  match xs {

+    case Nil =>

+    case Cons(b, xs') =>

+      calc {

+        sorted(reverse(Cons(b, xs'), Cons(a, ys)));

+        sorted(reverse(xs', Cons(b, Cons(a, ys))));

+      <==  { sorted_insertInMiddle(xs', b, Cons(a, ys)); }

+        // the next 3 lines are the premises of sorted_insertInMiddle

+        sorted(reverse(xs', Cons(a, ys))) &&

+        (forall y :: y in multiset_of(xs') ==> Below(y, b)) &&

+        (forall y :: y in multiset_of(Cons(a, ys)) ==> Below(b, y));

+        // the third premise holds

+        sorted(reverse(xs', Cons(a, ys))) &&

+        (forall y :: y in multiset_of(xs') ==> Below(y, b));

+        // the following sub-calculation establishes the second premise

+        calc {

+          true;

+          sorted(reverse(Cons(b, xs'), ys));

+          sorted(reverse(xs', Cons(b, ys)));

+        ==> { sorted_reverse(xs', Cons(b, ys)); }

+          forall y :: y in multiset_of(xs') ==> Below(y, b);

+        }

+        // finally, for the first premise

+        sorted(reverse(xs', Cons(a, ys)));

+      }

+      // Here is the proof of that premise

+      calc ==> {

+        true;

+        calc {

+          sorted(reverse(xs, ys));

+          { sorted_reverse(xs, ys); }

+          sorted(ys);

+          sorted(Cons(a, ys));

+        }

+        sorted(reverse(xs', Cons(b, ys))) && sorted(Cons(a, ys));

+        { sorted_replaceSuffix(xs', Cons(b, ys), Cons(a, ys)); }

+        sorted(reverse(xs', Cons(a, ys)));

+      }

+  }

+}

+

+lemma sorted_replaceSuffix(xs: List<G>, ys: List<G>, zs: List<G>)

+  requires sorted(reverse(xs, ys)) && sorted(zs);

+  requires forall a,b :: a in multiset_of(xs) && b in multiset_of(zs) ==> Below(a, b);

+  ensures sorted(reverse(xs, zs));

+{

+  match xs {

+    case Nil =>

+    case Cons(c, xs') =>

+      forall a,b | a in multiset_of(xs') && b in multiset_of(Cons(c, zs))

+        ensures Below(a, b);

+      {

+        sorted_reverse(xs', Cons(c, ys));

+      }

+      calc {

+        sorted(reverse(Cons(c, xs'), ys));

+        sorted(reverse(xs', Cons(c, ys)));

+        sorted(reverse(xs', Cons(c, ys))) && sorted(Cons(c, zs));

+      ==>  { sorted_replaceSuffix(xs', Cons(c, ys), Cons(c, zs)); }

+        sorted(reverse(xs', Cons(c, zs)));

+        sorted(reverse(Cons(c, xs'), zs));

+        sorted(reverse(xs, zs));

+      }

+  }

+}

+

+lemma sorted_mergeAll(x: List<List<G>>)

+  requires x != Nil && AllSorted(x);

+  ensures sorted(mergeAll(x));

+  decreases length(x);

+{

+  if x.tail == Nil {

+  } else {

+    sorted_mergePairs(x);

+  }

+}

+

+lemma sorted_mergePairs(x: List<List<G>>)

+  requires AllSorted(x);

+  ensures AllSorted(mergePairs(x));

+{

+  if x.Cons? && x.tail.Cons? {

+    calc {

+      AllSorted(mergePairs(x));

+      AllSorted(Cons(merge(x.head, x.tail.head), mergePairs(x.tail.tail)));

+      sorted(merge(x.head, x.tail.head)) && AllSorted(mergePairs(x.tail.tail));

+      calc ==> {

+        AllSorted(x);

+        AllSorted(x.tail);

+        AllSorted(x.tail.tail);

+        // induction hypothesis

+        AllSorted(mergePairs(x.tail.tail));

+      }

+      sorted(merge(x.head, x.tail.head));

+      calc ==> {

+        AllSorted(x);

+        sorted(x.head) && AllSorted(x.tail);

+        sorted(x.head) && sorted(x.tail.head);

+        { sorted_merge(x.head, x.tail.head); }

+        sorted(merge(x.head, x.tail.head));

+      }

+      true;

+    }

+  }

+}

+

+lemma sorted_merge(xs: List<G>, ys: List<G>)

+  requires sorted(xs) && sorted(ys);

+  ensures sorted(merge(xs, ys));

+{

+  match xs {

+    case Nil =>

+    case Cons(a, xs') =>

+      match ys {

+        case Nil =>

+        case Cons(b, ys') =>

+          sorted_smallest(a, xs');

+          sorted_smallest(b, ys');

+          if Below(a, b) {

+            forall y {

+              calc {

+                y in multiset_of(merge(xs', ys));

+                { perm_merge(xs', ys); }

+                y in multiset_of(xs') + multiset_of(ys);

+                y in multiset_of(xs') || y in multiset_of(ys);

+              ==>

+                Below(a, y) || Below(b, y);

+              ==>

+                Below(a, y);

+              }

+            }

+            assert sorted(merge(xs', ys));  // by induction hypothesis

+          } else {

+            forall y {

+              calc {

+                y in multiset_of(merge(xs, ys'));

+                { perm_merge(xs, ys'); }

+                y in multiset_of(xs) + multiset_of(ys');

+                y in multiset_of(xs) || y in multiset_of(ys');

+              ==>

+                Below(a, y) || Below(b, y);

+              ==>

+                Below(b, y);

+              }

+            }

+            assert sorted(merge(xs, ys'));  // by induction hypothesis

+          }

+      }

+  }

+}

+

+lemma sorted_smallest(a: G, xs: List<G>)

+  requires sorted(Cons(a, xs));

+  ensures forall y :: y in multiset_of(xs) ==> key(a) <= key(y);

+{

+}

+

+// -- stability lemmas

+

+lemma stable_sort(g: G, xs: List<G>)

+  ensures filter(g, sort(xs)) == filter(g, xs);

+{

+  calc {

+    filter(g, sort(xs));

+    // def. sort

+    filter(g, mergeAll(sequences(xs)));

+    { sorted_sequences(xs); stable_mergeAll(g, sequences(xs)); }

+    filter(g, flatten(sequences(xs)));

+    { stable_sequences(g, xs); }

+    filter(g, xs);

+  }

+}

+

+lemma stable_sequences(g: G, xs: List<G>)

+  ensures filter(g, flatten(sequences(xs))) == filter(g, xs);

+  decreases xs, 0;

+{

+  match xs {

+    case Nil =>

+    case Cons(a, ys) =>

+      match ys {

+        case Nil =>

+        case Cons(b, zs) =>

+          if !Below(a, b) {

+            calc {

+              filter(g, flatten(sequences(xs)));

+              filter(g, flatten(descending(b, Cons(a, Nil), zs)));

+              { stable_descending(g, b, Cons(a, Nil), zs); }

+              filter(g, append(Cons(b, Cons(a, Nil)), zs));

+              // in the next couple of steps, unfold the definition of append

+              filter(g, Cons(b, append(Cons(a, Nil), zs)));

+              filter(g, Cons(b, Cons(a, zs)));

+              { filter_Cons_notBelow(g, b, a, zs); }

+              filter(g, Cons(a, Cons(b, zs)));

+            }

+          } else {

+            calc {

+              filter(g, flatten(sequences(xs)));

+              filter(g, flatten(ascending(b, Cons(a, Nil), zs)));

+              { stable_ascending(g, b, Cons(a, Nil), zs); }

+              filter(g, append(reverse(Cons(b, Cons(a, Nil)), Nil), zs));

+              // in the next three steps, unfold the definition of reverse

+              filter(g, append(reverse(Cons(a, Nil), Cons(b, Nil)), zs));

+              filter(g, append(reverse(Nil, Cons(a, Cons(b, Nil))), zs));

+              filter(g, append(Cons(a, Cons(b, Nil)), zs));

+              // in the next couple of steps, unfold the definition of append

+              filter(g, Cons(a, append(Cons(b, Nil), zs)));

+              filter(g, Cons(a, Cons(b, zs)));

+            }

+          }

+      }

+  }

+}

+

+lemma stable_descending(g: G, a: G, xs: List<G>, ys: List<G>)

+  requires sorted(Cons(a, xs));

+  ensures filter(g, flatten(descending(a, xs, ys))) == filter(g, append(Cons(a, xs), ys));

+  decreases ys;

+{

+  if ys.Cons? && !Below(a, ys.head) {

+    calc {

+      filter(g, flatten(descending(a, xs, ys)));

+      filter(g, flatten(descending(ys.head, Cons(a, xs), ys.tail)));

+      { stable_descending(g, ys.head, Cons(a, xs), ys.tail); }

+      filter(g, append(Cons(ys.head, Cons(a, xs)), ys.tail));

+      filter(g, Cons(ys.head, append(Cons(a, xs), ys.tail)));

+      { filter_append_notBelow(g, ys.head, Cons(a, xs), ys.tail); }

+      filter(g, append(Cons(a, xs), Cons(ys.head, ys.tail)));

+      filter(g, append(Cons(a, xs), ys));

+    }

+  } else {

+    calc {

+      filter(g, flatten(descending(a, xs, ys)));

+      filter(g, flatten(Cons(Cons(a, xs), sequences(ys))));

+      filter(g, append(Cons(a, xs), flatten(sequences(ys))));

+      { filter_append(g, Cons(a, xs), flatten(sequences(ys))); }

+      append(filter(g, Cons(a, xs)), filter(g, flatten(sequences(ys))));

+      { stable_sequences(g, ys); }

+      append(filter(g, Cons(a, xs)), filter(g, ys));

+      { filter_append(g, Cons(a, xs), ys); }

+      filter(g, append(Cons(a, xs), ys));

+    }

+  }

+}

+

+lemma stable_ascending(g: G, a: G, xs: List<G>, ys: List<G>)

+  ensures filter(g, flatten(ascending(a, xs, ys))) == filter(g, append(reverse(Cons(a, xs), Nil), ys));

+  decreases ys;

+{

+  if ys.Cons? && Below(a, ys.head) {

+    calc {

+      filter(g, flatten(ascending(a, xs, ys)));

+      filter(g, flatten(ascending(ys.head, Cons(a, xs), ys.tail)));

+      { stable_ascending(g, ys.head, Cons(a, xs), ys.tail); }

+      filter(g, append(reverse(Cons(ys.head, Cons(a, xs)), Nil), ys.tail));

+      filter(g, append(reverse(Cons(a, xs), Cons(ys.head, Nil)), ys.tail));

+      { filter_append_reverse(g, ys.head, Cons(a, xs), ys.tail); }

+      filter(g, append(reverse(Cons(a, xs), Nil), Cons(ys.head, ys.tail)));

+      filter(g, append(reverse(Cons(a, xs), Nil), ys));

+    }

+  } else {

+    calc {

+      filter(g, flatten(ascending(a, xs, ys)));

+      filter(g, flatten(Cons(reverse(Cons(a, xs), Nil), sequences(ys))));

+      filter(g, append(reverse(Cons(a, xs), Nil), flatten(sequences(ys))));

+      { filter_append(g, reverse(Cons(a, xs), Nil), flatten(sequences(ys))); }

+      append(filter(g, reverse(Cons(a, xs), Nil)), filter(g, flatten(sequences(ys))));

+      { stable_sequences(g, ys); }

+      append(filter(g, reverse(Cons(a, xs), Nil)), filter(g, ys));

+      { filter_append(g, reverse(Cons(a, xs), Nil), ys); }

+      filter(g, append(reverse(Cons(a, xs), Nil), ys));

+    }

+  }

+}

+

+lemma stable_mergeAll(g: G, x: List<List<G>>)

+  requires x != Nil && AllSorted(x);

+  ensures filter(g, mergeAll(x)) == filter(g, flatten(x));

+  decreases length(x);

+{

+  if x.tail == Nil {

+    calc {

+      flatten(x);

+      append(x.head, Nil);

+      { append_Nil(x.head); }

+      x.head;

+      mergeAll(x);

+    }

+  } else {

+    calc {

+      filter(g, mergeAll(x));

+      filter(g, mergeAll(mergePairs(x)));

+      { sorted_mergePairs(x); stable_mergeAll(g, mergePairs(x)); }  // induction hypothesis

+      filter(g, flatten(mergePairs(x)));

+      { stable_mergePairs(g, x); }

+      filter(g, flatten(x));

+    }

+  }

+}

+

+lemma stable_mergePairs(g: G, x: List<List<G>>)

+  requires AllSorted(x);

+  ensures filter(g, flatten(mergePairs(x))) == filter(g, flatten(x));

+{

+  if x.Cons? && x.tail.Cons? {

+    match x { case Nil => case Cons(_, _) => }

+    calc {

+      filter(g, flatten(mergePairs(x)));

+      // def. mergePairs

+      filter(g, flatten(Cons(merge(x.head, x.tail.head), mergePairs(x.tail.tail))));

+      // def. flatten

+      filter(g, append(merge(x.head, x.tail.head), flatten(mergePairs(x.tail.tail))));

+      { filter_append(g, merge(x.head, x.tail.head), flatten(mergePairs(x.tail.tail))); }

+      append(filter(g, merge(x.head, x.tail.head)), filter(g, flatten(mergePairs(x.tail.tail))));

+      { stable_mergePairs(g, x.tail.tail); }  // induction hypothesis

+      append(filter(g, merge(x.head, x.tail.head)), filter(g, flatten(x.tail.tail)));

+      { stable_merge(g, x.head, x.tail.head); }

+      append(filter(g, append(x.head, x.tail.head)), filter(g, flatten(x.tail.tail)));

+      { filter_append(g, append(x.head, x.tail.head), flatten(x.tail.tail)); }

+      filter(g, append(append(x.head, x.tail.head), flatten(x.tail.tail)));

+      { append_associative(x.head, x.tail.head, flatten(x.tail.tail)); }

+      filter(g, append(x.head, append(x.tail.head, flatten(x.tail.tail))));

+      // def. flatten

+      filter(g, append(x.head, flatten(Cons(x.tail.head, x.tail.tail))));

+      filter(g, append(x.head, flatten(x.tail)));

+      // def. flatten

+      filter(g, flatten(Cons(x.head, x.tail)));

+      filter(g, flatten(x));

+    }

+  }

+}

+

+lemma stable_merge(g: G, xs: List<G>, ys: List<G>)

+  requires sorted(xs);

+  ensures filter(g, merge(xs, ys)) == filter(g, append(xs, ys));

+{

+  match xs {

+    case Nil =>

+    case Cons(a, xs') =>

+      match ys {

+        case Nil =>

+          append_Nil(xs);

+        case Cons(b, ys') =>

+          if Below(a, b) {

+            // proof for this case is automatic; merge does the same thing as append does

+          } else {

+            calc {

+              filter(g, merge(xs, ys));

+              filter(g, Cons(b, merge(xs, ys')));

+              { stable_merge(g, xs, ys'); }

+              filter(g, Cons(b, append(xs, ys')));

+              { filter_append_notBelow(g, b, xs, ys'); }

+              filter(g, append(xs, Cons(b, ys')));

+              filter(g, append(xs, ys));

+            }

+        }

+      }

+  }

+}

+

+lemma filter_append(g: G, xs: List<G>, ys: List<G>)

+  ensures filter(g, append(xs, ys)) == append(filter(g, xs), filter(g, ys));

+{

+}

+

+lemma filter_append_notBelow(g: G, b: G, xs: List<G>, ys: List<G>)

+  requires sorted(xs);

+  requires xs.Cons? ==> !Below(xs.head, b);

+  ensures filter(g, Cons(b, append(xs, ys))) == filter(g, append(xs, Cons(b, ys)));

+{

+}

+

+lemma filter_Cons_notBelow(g: G, b: G, a: G, ys: List<G>)

+  requires !Below(a, b);

+  ensures filter(g, Cons(b, Cons(a, ys))) == filter(g, Cons(a, Cons(b, ys)));

+{

+  filter_append_notBelow(g, b, Cons(a, Nil), ys);

+}

+

+lemma filter_append_reverse(g: G, b: G, xs: List<G>, ys: List<G>)

+  ensures filter(g, append(reverse(xs, Cons(b, Nil)), ys)) == filter(g, append(reverse(xs, Nil), Cons(b, ys)));

+{

+  match xs {

+    case Nil =>

+    case Cons(c, xs') =>

+      calc {

+        filter(g, append(reverse(xs, Cons(b, Nil)), ys));

+        filter(g, append(reverse(Cons(c, xs'), Cons(b, Nil)), ys));

+        { append_reverse(Cons(c, xs'), Cons(b, Nil)); }

+        filter(g, append(append(reverse(Cons(c, xs'), Nil), Cons(b, Nil)), ys));

+        // def. reverse

+        filter(g, append(append(reverse(xs', Cons(c, Nil)), Cons(b, Nil)), ys));

+        { append_associative(reverse(xs', Cons(c, Nil)), Cons(b, Nil), ys); }

+        filter(g, append(reverse(xs', Cons(c, Nil)), append(Cons(b, Nil), ys)));

+        // def. append

+        filter(g, append(reverse(xs', Cons(c, Nil)), Cons(b, ys)));

+        // def. reverse

+        filter(g, append(reverse(Cons(c, xs'), Nil), Cons(b, ys)));

+        filter(g, append(reverse(xs, Nil), Cons(b, ys)));

+      }

+  }

+}

+

+lemma append_reverse(xs: List, ys: List)

+  ensures reverse(xs, ys) == append(reverse(xs, Nil), ys);

+{

+  match xs {

+    case Nil =>

+    case Cons(a, xs') =>

+      calc {

+        reverse(Cons(a, xs'), ys);

+        reverse(xs', Cons(a, ys));

+        // induction hypothesis

+        append(reverse(xs', Nil), Cons(a, ys));

+        append(reverse(xs', Nil), append(Cons(a, Nil), ys));

+        { append_associative(reverse(xs', Nil), Cons(a, Nil), ys); }

+        append(append(reverse(xs', Nil), Cons(a, Nil)), ys);

+        // induction hypothesis

+        append(reverse(xs', Cons(a, Nil)), ys);

+        append(reverse(Cons(a, xs'), Nil), ys);

+      }

+  }

+}

diff --git a/Test/dafny4/runtest.bat b/Test/dafny4/runtest.bat
new file mode 100644
index 00000000..f656066a
--- /dev/null
+++ b/Test/dafny4/runtest.bat
@@ -0,0 +1,7 @@
+@echo off

+setlocal

+

+set BINARIES=..\..\Binaries

+set DAFNY_EXE=%BINARIES%\Dafny.exe

+

+%DAFNY_EXE% /compile:0 /verifySeparately /dprint:out.dfy.tmp %* CoqArt-InsertionSort.dfy GHC-MergeSort.dfy Fstar-QuickSort.dfy