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
128
129
130
131
132
133
134
135
136
137
138
139
140
|
// RUN: %dafny /compile:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// Note: We used integers instead of a generic Comparable type, because
// Dafny has no way of saying that the Comparable type's AtMost function
// is total and transitive.
// Note: We couldn't get things to work out if we used the Get method.
// Instead, we used .contents.
// Note: Due to infelicities of the Dafny sequence treatment, we
// needed to supply two lemmas, do a complicated assignment of
// pperm, had to write invariants over p and perm rather than pperm and we couldn't use
// "x in p".
class Queue<T> {
var contents: seq<T>;
method Init()
modifies this;
ensures |contents| == 0;
method Enqueue(x: T)
modifies this;
ensures contents == old(contents) + [x];
method Dequeue() returns (x: T)
requires 0 < |contents|;
modifies this;
ensures contents == old(contents)[1..] && x == old(contents)[0];
function method Head(): T
requires 0 < |contents|;
reads this;
{ contents[0] }
function method Get(i: int): T
requires 0 <= i < |contents|;
reads this;
{ contents[i] }
}
class Comparable {
function AtMost(c: Comparable): bool
reads this, c;
}
class Benchmark3 {
method Sort(q: Queue<int>) returns (r: Queue<int>)
requires q != null;
modifies q;
ensures r != null && fresh(r);
ensures |r.contents| == |old(q.contents)|;
ensures forall i, j :: 0 <= i < j < |r.contents| ==> r.Get(i) <= r.Get(j);
// the final Queue is a permutation of the input Queue
ensures multiset(r.contents) == multiset(old(q.contents));
{
r := new Queue<int>.Init();
while |q.contents| != 0
invariant |r.contents| + |q.contents| == |old(q.contents)|;
invariant forall i, j :: 0 <= i < j < |r.contents| ==> r.contents[i] <= r.contents[j];
invariant forall i, j ::
0 <= i < |r.contents| &&
0 <= j < |q.contents|
==> r.contents[i] <= q.contents[j];
// the current array is that permutation of the input array
invariant multiset(r.contents + q.contents) == multiset(old(q.contents));
{
ghost var qc := q.contents;
var m,k := RemoveMin(q);
assert qc == qc[..k] + [m] + qc[k+1..];
r.Enqueue(m);
}
}
method RemoveMin(q: Queue<int>) returns (m: int, k: int) //m is the min, k is m's index in q
requires q != null && |q.contents| != 0;
modifies q;
ensures |old(q.contents)| == |q.contents| + 1;
ensures 0 <= k < |old(q.contents)| && old(q.contents[k]) == m;
ensures forall i :: 0 <= i < |q.contents| ==> m <= q.contents[i];
ensures q.contents == old(q.contents)[k+1..] + old(q.contents)[..k];
{
var n := |q.contents|;
k := 0;
m := q.Head();
var j := 0;
while j < n
invariant j <= n;
invariant 0 <= k < n && old(q.contents)[k] == m;
invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j]; //i.e. rotated
invariant forall i :: 0 <= i < j ==> m <= old(q.contents)[i]; //m is min so far
{
ghost var qc0 := q.contents;
var x := q.Dequeue();
q.Enqueue(x);
RotationLemma(old(q.contents), j, qc0, q.contents);
if x < m { k := j; m := x; }
j := j+1;
}
j := 0;
while j < k
invariant j <= k;
invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j];
{
ghost var qc0 := q.contents;
var x := q.Dequeue();
q.Enqueue(x);
RotationLemma(old(q.contents), j, qc0, q.contents);
j := j+1;
}
assert j == k;
assert q.contents == old(q.contents)[k..] + old(q.contents)[..k];
m := q.Dequeue();
}
lemma RotationLemma(O: seq, j: nat, A: seq, C: seq)
requires j < |O|;
requires A == O[j..] + O[..j];
requires C == A[1..] + [O[j]];
ensures C == O[j+1..] + O[..j+1];
{
calc {
A;
O[j..] + O[..j];
O[j..j+1] + O[j+1..] + O[..j];
O[j..j+1] + (O[j+1..] + O[..j]);
}
calc {
C;
A[1..] + [A[0]];
{ assert A[0] == O[j] && A[1..] == O[j+1..] + O[..j]; }
O[j+1..] + O[..j] + [O[j]];
{ assert [O[j]] == O[j..j+1]; }
O[j+1..] + O[..j] + O[j..j+1];
O[j+1..] + (O[..j] + O[j..j+1]);
O[j+1..] + O[..j+1];
}
}
}
|
