blob: 07dc2f7ece52977e2ce9b6d79e96070fae4d61e6 (
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
|
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| &&
(forall i :: 0 <= i && i < |current.list| ==> current.list[i] == old(list)[|reverse.list|+i]);
invariant
(forall i :: 0 <= i && i < |reverse.list| ==> old(list)[i] == reverse.list[|reverse.list|-1-i]);
decreases current, |current.list|;
{
var nx := current.next;
assert nx != null ==> (forall i :: 0 <= i && i < |nx.list| ==> current.list[1+i] == nx.list[i]); // lemma
// ..., reverse, current, nx, ...
assert current.data == current.list[0]; // lemma
current.next := reverse;
current.footprint := {current} + reverse.footprint;
current.list := [current.data] + reverse.list;
reverse := current;
current := nx;
}
}
}
|
