diff options
| author |  Rustan Leino <unknown> | 2014-01-08 23:57:48 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-01-08 23:57:48 -0800 |
| commit | 5fcfcbe96910e4205e9777ca28405e4f48e0f120 (patch) | |
| tree | bb141a9d4e0245d257badfdf5fe2a36b0167bd0b /Test/dafny4/Fstar-QuickSort.dfy | |
| parent | de8338b233b3a4daec0f0cfcfeca59115e32e574 (diff) | |
Dafny renditions of sorting algorithms proved in other provers (Coq, Isabelle, F*)
Diffstat (limited to 'Test/dafny4/Fstar-QuickSort.dfy')
| -rw-r--r-- | Test/dafny4/Fstar-QuickSort.dfy | 126 |
1 files changed, 126 insertions, 0 deletions
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')
+
+*/
|