blob: a9859aaaf4bf374661e297965c4794c7dee6d978 (
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
|
/* 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 && (forall y:int :: contains(y) <==> y==v);
{
next := null;
value := v;
fold this.valid;
}
method add(x: int)
requires valid;
ensures valid;
ensures size() == old(size())+1;
ensures (forall y:int :: contains(y)==(old(contains(y)) || x==y));
{
unfold this.valid;
if(next==null) {
var n : Node;
n := new Node;
call n.init(x);
next := n;
// unfold next.valid; fold next.valid; // makes it work
} else {
call next.add(x);
}
fold this.valid;
}
method addother(i:int)
requires valid
ensures valid && (forall x:int :: contains(x)==(old(contains(x)) || x==i))
{
unfold valid
if(next!=null)
{
call next.addother(i)
}
else
{
next:=new Node
next.value:=i
next.next:=null
fold next.valid
}
fold 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)
}
function size(): int
requires valid;
ensures result > 0
{
unfolding this.valid in (next!=null ? 1+ next.size() : 1)
}
function contains(i:int):bool
requires valid
{
unfolding valid in i==value || (next!=null && next.contains(i))
}
predicate valid {
acc(next) && acc(value) && (next!=null ==> next.valid)
}
}
|
