blob: af33409380e8e84d6ae36619aff6bba53eddc7a4 (
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
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
|
/* Recursive implementation and specification of a linked list. */
class Node {
var next: Node;
var value: int;
method init(v: int)
requires acc(next) && acc(value);
ensures valid && size() == 1;
{
next := null;
value := v;
fold this.valid;
}
method append(x: int)
requires valid;
ensures valid;
ensures size() == old(size())+1;
{
unfold this.valid;
if(next==null) {
var n : Node;
n := new Node;
call n.init(x);
next := n;
} else {
call next.append(x);
}
fold this.valid;
}
method prepend(x: int) returns (rt: Node)
requires valid;
ensures rt!=null && rt.valid;
ensures rt.size() == old(size()) + 1;
{
var n: Node;
n := new Node;
n.value := x;
n.next := this;
fold n.valid;
rt := n;
}
function at(i: int): int
requires valid && 0<=i && i<size();
{
unfolding valid in i==0 ? value : next.at(i-1)
}
function size(): int
requires valid;
{
unfolding this.valid in (next!=null ? 1 + next.size() : 1)
}
predicate valid {
acc(next) && acc(value) &&
(next!=null ==> next.valid)
}
}
// abstract sequence of integers
class LinkedList {
ghost var rep: seq<int>;
var first: Node;
method init()
requires acc(this.*);
ensures valid;
{
first := null;
assert coupling(rep, first);
fold valid;
}
method append(x: int)
requires valid;
ensures valid;
{
unfold valid;
rep := rep ++ [x];
fold valid;
}
method prepend(x: int)
requires valid;
ensures valid;
{
unfold valid;
rep := [x] ++ rep;
fold valid;
}
predicate valid {
acc(rep) && acc(first) && (first != null ==> first.valid)
}
function coupling(a: seq<int>, c: Node) : bool
requires c != null ==> c.valid;
{
c == null ? a == nil<int> :
(|a| > 0 && a[0] == c.value && coupling(a[1..], c.next))
}
}
|
