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
|
// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// Rustan Leino
// 12 April 2015
// VerifyThis 2015
// Problem 3 -- Dancing Links
// The following method demonstrates that Remove and PutBack (defined below) have the desired properties
method Test(dd: DoublyLinkedList, x: Node)
requires dd != null && dd.Valid()
requires x in dd.Nodes && x != dd.Nodes[0] && x != dd.Nodes[|dd.Nodes|-1]
modifies dd, dd.Nodes
ensures dd.Valid() && dd.Nodes == old(dd.Nodes)
{
ghost var k := dd.Remove(x);
dd.PutBack(x, k);
}
// It is also possible to remove and put back any number of elements, provided these operations are
// done in a FOLI order.
method TestMany(dd: DoublyLinkedList, xs: seq<Node>)
requires dd != null && dd.Valid()
requires forall x :: x in xs ==> x in dd.Nodes && x != dd.Nodes[0] && x != dd.Nodes[|dd.Nodes|-1]
requires forall i,j :: 0 <= i < j < |xs| ==> xs[i] != xs[j]
modifies dd, dd.Nodes
ensures dd.Valid() && dd.Nodes == old(dd.Nodes)
{
if xs != [] {
var x := xs[0];
ghost var k := dd.Remove(x);
TestMany(dd, xs[1..]);
dd.PutBack(x, k);
}
}
// And here's a Main program that shows that doubly linked lists do exist (well, at least there is one :))
method Main()
{
var a0 := new Node;
var a1 := new Node;
var a2 := new Node;
var a3 := new Node;
var a4 := new Node;
var a5 := new Node;
var dd := new DoublyLinkedList([a0, a1, a2, a3, a4, a5]);
Test(dd, a3);
TestMany(dd, [a2, a4, a3]);
}
class Node {
var L: Node
var R: Node
}
class DoublyLinkedList {
ghost var Nodes: seq<Node> // sequence of nodes in the linked list
// Valid() says that the data structure is a proper doubly linked list
predicate Valid()
reads this, Nodes
{
(forall i :: 0 <= i < |Nodes| ==> Nodes[i] != null) &&
(|Nodes| > 0 ==>
Nodes[0].L == null && (forall i :: 1 <= i < |Nodes| ==> Nodes[i].L == Nodes[i-1]) &&
(forall i :: 0 <= i < |Nodes|-1 ==> Nodes[i].R == Nodes[i+1]) && Nodes[|Nodes|-1].R == null
) &&
forall i,j :: 0 <= i < j < |Nodes| ==> Nodes[i] != Nodes[j] // this is actually a consequence of the previous conditions
}
// This constructor just shows that there is a way to create a doubly linked list. It accepts
// as an argument the sequences of Nodes to construct the doubly linked list from. The constructor
// will change all the .L and .R pointers of the given nodes in order to create a properly
// formed list.
constructor (nodes: seq<Node>)
requires forall i :: 0 <= i < |nodes| ==> nodes[i] != null
requires forall i,j :: 0 <= i < j < |nodes| ==> nodes[i] != nodes[j]
modifies this, nodes
ensures Valid() && Nodes == nodes
{
if nodes != [] {
var prev, n := nodes[0], 1;
prev.L, prev.R := null, null;
while n < |nodes|
invariant 1 <= n <= |nodes|
invariant nodes[0].L == null
invariant prev == nodes[n-1] && prev.R == null
invariant forall i :: 1 <= i < n ==> nodes[i].L == nodes[i-1]
invariant forall i :: 0 <= i < n-1 ==> nodes[i].R == nodes[i+1]
{
nodes[n].L, prev.R, prev := prev, nodes[n], nodes[n];
prev.R := null;
n := n + 1;
}
}
Nodes := nodes;
}
function PopMiddle<T>(s: seq<T>, k: nat) : seq<T>
requires k < |s| {
s[..k] + s[k+1..]
}
predicate Injective<T>(s: seq<T>) {
forall j, k :: 0 <= j < k < |s| ==> s[j] != s[k]
}
lemma InjectiveAfterPop<T>(s: seq<T>, k: nat)
requires k < |s|
requires Injective(s)
ensures Injective(PopMiddle(s, k)) { }
method Remove(x: Node) returns (ghost k: int)
requires Valid()
requires x in Nodes && x != Nodes[0] && x != Nodes[|Nodes|-1] // not allowed to remove end nodes; you may think of them as a sentinel nodes
modifies this, Nodes
ensures Valid()
ensures 0 <= k < |old(Nodes)| && x == old(Nodes)[k]
ensures Nodes == old(Nodes)[..k] + old(Nodes)[k+1..] && x.L == old(x.L) && x.R == old(x.R)
{
k :| 1 <= k < |Nodes|-1 && Nodes[k] == x;
x.R.L := x.L;
x.L.R := x.R;
InjectiveAfterPop(Nodes, k);
Nodes := Nodes[..k] + Nodes[k+1..];
}
// One might consider have a precondition that says there exists a "k" with the properties given here.
// However, we want to be able to refer to "k" in the postcondition as well, so it's convenient to
// burden the client with having to pass in "k" as a ghost parameter. This, however, is really no
// extra burden on the client, because if the client would have been able to show the existence of
// such a "k", then the client can easily just use an assign-such-that statement to obtain such a
// value "k".
method PutBack(x: Node, ghost k: int)
requires Valid()
requires x != null && 1 <= k < |Nodes| && x.L == Nodes[k-1] && x.R == Nodes[k]
modifies this, Nodes, x
ensures Valid()
ensures Nodes == old(Nodes)[..k] + [x] + old(Nodes)[k..]
{
x.R.L := x;
x.L.R := x;
Nodes := Nodes[..k] + [x] + Nodes[k..];
}
}
// --------------------------------------------------------
// If it were not required to build a data structure (like the class above) that supports the
// Remove and PutBack operations, the operations can easily be verified to compose into the
// identity transformation. The following method shows that the two operations, under a suitable
// precondition, have no net effect on any .L or .R field.
method Alt(x: Node)
requires x != null && x.L != null && x.R != null
requires x.L.R == x && x.R.L == x // links are mirrored
modifies x, x.L, x.R
ensures forall y: Node :: y != null ==> y.L == old(y.L) && y.R == old(y.R)
{
// remove
x.R.L := x.L;
x.L.R := x.R;
// put back
x.R.L := x;
x.L.R := x;
}
|
