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
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
|
// RUN: %dafny /compile:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// VSComp 2010, problem 5, double-ended queue.
// Rustan Leino, 18 August 2010.
//
// This program employs the standard Valid()/Repr idiom used in the dynamic-frames
// style of specifications, see for example the comment in Problem3-FindZero.dfy.
// Within that idiom, the specification is straightforward (if verbose), and there
// are no particular wrinkles or annoyances in getting the verifier to prove the
// correctness.
class AmortizedQueue<T(0)> {
// The front of the queue.
var front: LinkedList<T>
// The rear of the queue (stored in reversed order).
var rear: LinkedList<T>
ghost var Repr: set<object>
ghost var List: seq<T>
predicate Valid()
reads this, Repr
{
this in Repr &&
front in Repr && front.Repr <= Repr && front.Valid() &&
rear in Repr && rear.Repr <= Repr && rear.Valid() &&
|rear.List| <= |front.List| &&
List == front.List + rear.ReverseSeq(rear.List)
}
constructor Init()
ensures Valid() && List == []
{
front := new LinkedList<T>.Init();
rear := new LinkedList<T>.Init();
new;
Repr := {this} + front.Repr + rear.Repr;
List := [];
}
constructor InitFromPieces(f: LinkedList<T>, r: LinkedList<T>)
requires f.Valid() && r.Valid()
ensures Valid() && List == f.List + r.ReverseSeq(r.List)
{
if (r.length <= f.length) {
front := f;
rear := r;
} else {
var rr := r.Reverse();
var ff := f.Concat(rr);
front := ff;
rear := new LinkedList<T>.Init();
}
new;
Repr := {this} + front.Repr + rear.Repr;
List := front.List + rear.ReverseSeq(rear.List);
}
method Front() returns (t: T)
requires Valid() && List != []
ensures t == List[0]
{
t := front.head;
}
method Tail() returns (r: AmortizedQueue<T>)
requires Valid() && List != []
ensures r.Valid() && r.List == List[1..]
{
r := new AmortizedQueue<T>.InitFromPieces(front.tail, rear);
}
method Enqueue(item: T) returns (r: AmortizedQueue<T>)
requires Valid()
ensures r.Valid() && r.List == List + [item]
{
var rr := rear.Cons(item);
r := new AmortizedQueue<T>.InitFromPieces(front, rr);
}
}
class LinkedList<T(0)> {
var head: T
var tail: LinkedList?<T>
var length: int
ghost var List: seq<T>
ghost var Repr: set<LinkedList<T>>
predicate Valid()
reads this, Repr
{
this in Repr &&
0 <= length && length == |List| &&
(length == 0 ==> List == [] && tail == null) &&
(length != 0 ==>
tail != null && tail in Repr &&
tail.Repr <= Repr && this !in tail.Repr &&
tail.Valid() &&
List == [head] + tail.List &&
length == tail.length + 1)
}
constructor Init()
ensures Valid() && List == []
{
tail := null;
length := 0;
List := [];
Repr := {this};
}
constructor ()
{
}
method Cons(d: T) returns (r: LinkedList<T>)
requires Valid()
ensures r.Valid() && r.List == [d] + List
{
r := new LinkedList<T>();
r.head := d;
r.tail := this;
r.length := length + 1;
r.List := [d] + List;
r.Repr := {r} + Repr;
}
method Concat(end: LinkedList<T>) returns (r: LinkedList<T>)
requires Valid() && end.Valid()
ensures r.Valid() && r.List == List + end.List
decreases Repr;
{
if (length == 0) {
r := end;
} else {
var c := tail.Concat(end);
r := c.Cons(head);
}
}
method Reverse() returns (r: LinkedList<T>)
requires Valid()
ensures r.Valid() && |List| == |r.List|
ensures (forall k :: 0 <= k && k < |List| ==> List[k] == r.List[|List|-1-k])
ensures r.List == ReverseSeq(List)
decreases Repr
{
if (length == 0) {
r := this;
} else {
r := tail.Reverse();
var e := new LinkedList<T>.Init();
e := e.Cons(head);
r := r.Concat(e);
}
}
static function ReverseSeq(s: seq<T>): seq<T>
{
if s == [] then [] else
ReverseSeq(s[1..]) + [s[0]]
}
}
|
