blob: acde86abda3278a62ea2e4c30fb0d16af81a4d74 (
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
|
/* 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 add(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.add(x);
}
fold this.valid;
}
method addFirst(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) // no warning anymore... fishy!
}
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)
}
}
|
