blob: b79d3308ce8965237c783f13bc5090c40025ff40 (
plain)
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
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
class Node<T> {
var list: seq<T>;
var footprint: set<Node<T>>;
var data: T;
var next: Node<T>;
function Valid(): bool
reads this, footprint;
{
this in this.footprint && null !in this.footprint &&
(next == null ==> list == [data]) &&
(next != null ==>
next in footprint && next.footprint <= footprint &&
this !in next.footprint &&
list == [data] + next.list &&
next.Valid())
}
method Init(d: T)
modifies this;
ensures Valid() && fresh(footprint - {this});
ensures list == [d];
{
data := d;
next := null;
list := [d];
footprint := {this};
}
method SkipHead() returns (r: Node<T>)
requires Valid();
ensures r == null ==> |list| == 1;
ensures r != null ==> r.Valid() && r.footprint <= footprint;
ensures r != null ==> r.list == list[1..];
{
r := next;
}
method Prepend(d: T) returns (r: Node<T>)
requires Valid();
ensures r != null && r.Valid() && fresh(r.footprint - old(footprint));
ensures r.list == [d] + list;
{
r := new Node<T>;
r.data := d;
r.next := this;
r.footprint := {r} + this.footprint;
r.list := [r.data] + this.list;
}
method ReverseInPlace() returns (reverse: Node<T>)
requires Valid();
modifies footprint;
ensures reverse != null && reverse.Valid();
ensures fresh(reverse.footprint - old(footprint));
ensures |reverse.list| == |old(list)|;
ensures (forall i :: 0 <= i && i < |old(list)| ==> old(list)[i] == reverse.list[|old(list)|-1-i]);
{
var current := next;
reverse := this;
reverse.next := null;
reverse.footprint := {reverse};
reverse.list := [data];
while (current != null)
invariant reverse != null && reverse.Valid();
invariant reverse.footprint <= old(footprint);
invariant current == null ==> |old(list)| == |reverse.list|;
invariant current != null ==>
current.Valid() &&
current in old(footprint) && current.footprint <= old(footprint) &&
current.footprint !! reverse.footprint &&
|old(list)| == |reverse.list| + |current.list|;
invariant current != null ==> current.list == old(list)[|reverse.list|..];
invariant
(forall i :: 0 <= i && i < |reverse.list| ==> old(list)[i] == reverse.list[|reverse.list|-1-i]);
decreases if current != null then |current.list| else -1;
{
var nx := current.next;
// ..., reverse, current, nx, ...
current.next := reverse;
current.footprint := {current} + reverse.footprint;
current.list := [current.data] + reverse.list;
reverse := current;
current := nx;
}
}
}
|
