diff options
author | 2014-01-08 23:57:48 -0800 | |
---|---|---|
committer | 2014-01-08 23:57:48 -0800 | |
commit | 5fcfcbe96910e4205e9777ca28405e4f48e0f120 (patch) | |
tree | bb141a9d4e0245d257badfdf5fe2a36b0167bd0b /Test | |
parent | de8338b233b3a4daec0f0cfcfeca59115e32e574 (diff) |
Dafny renditions of sorting algorithms proved in other provers (Coq, Isabelle, F*)
Diffstat (limited to 'Test')
-rw-r--r-- | Test/alltests.txt | 1 | ||||
-rw-r--r-- | Test/dafny4/Answer | 12 | ||||
-rw-r--r-- | Test/dafny4/CoqArt-InsertionSort.dfy | 192 | ||||
-rw-r--r-- | Test/dafny4/Fstar-QuickSort.dfy | 126 | ||||
-rw-r--r-- | Test/dafny4/GHC-MergeSort.dfy | 838 | ||||
-rw-r--r-- | Test/dafny4/runtest.bat | 7 |
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
|