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
|
// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" /vcsMaxKeepGoingSplits:5 "%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;
}
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;
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..];
}
}
|
