1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// 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 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>): (List<int>, List<int>)
ensures var (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 => (Nil, Nil)
case Cons(hd, tl) =>
var (lo, hi) := partition(x, tl);
if hd <= x then
(Cons(hd, lo), hi)
else
(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 (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')
*/
|
