blob: ae72fe6776e10202da43b5b0bddd2de58405ad87 (
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
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
|
/**
Interesting issues:
* recursive functions should either use read accesses or provide frame conditions of operating on the same state
* carrying super-abstract state might be beneficial for the proof in the concrete program
* proofs of function refinement might be needed as lemmas in places where they are used
*/
class List0 {
var rep: seq<int>;
method init()
requires acc(this.*);
ensures acc(rep);
{
rep := [0];
}
function length(): int
requires acc(rep);
{
|rep|
}
method get(i: int) returns (v: int)
requires acc(rep);
requires 0 <= i && i < length();
ensures acc(rep);
{
v := rep[i];
}
method pick() returns (v: int)
requires acc(rep);
ensures acc(rep);
{
var i: int;
assume 0 <= i && i < length();
v := rep[i];
}
}
class Node1 {
var data;
}
class List1 {
ghost var rep: seq<int>;
var l: seq<Node1>;
function inv(): bool
requires acc(rep) && acc(l) && acc(l[*].data);
{
/** valid */ (forall i in [0..|l|] :: l[i] != null) &&
/** coupling */ |l| == |rep| && (forall i in [0..|l|] :: l[i].data == rep[i])
}
method init()
requires acc(this.*);
ensures acc(rep) && acc(l) && acc(l[*].data) && inv();
{
rep := nil<int>;
l := nil<Node1>;
}
function length(): int
requires acc(rep) && acc(l) && acc(l[*].data) && inv();
{
|l|
}
method checkLength()
requires acc(rep) && acc(l) && acc(l[*].data) && inv();
{
assert length() == |rep|;
}
method get(i: int) returns (v: int)
requires acc(rep) && acc(l) && acc(l[*].data) && inv();
requires 0 <= i && i < length();
ensures acc(rep) && acc(l) && acc(l[*].data) && inv();
{
v := l[i].data;
assert v == rep[i];
}
}
class Node2 {
var data;
var next: Node2;
}
class List2 {
ghost var rep: seq<int>;
ghost var l: seq<Node2>;
var head: Node2;
var size: int;
function inv(): bool
requires acc(rep) && acc(l) && acc(l[*].data) && acc(l[*].next) && acc(head) && acc(size)
{
/** valid */ (forall i in [0..|l|] :: l[i] != null) &&
/** coupling */ |l| == |rep| && (forall i in [0..|l|] :: l[i].data == rep[i]) &&
/** new coupling */ size == |l| &&
(head == null ==> |l| == 0) &&
(head != null ==> |l| > 0 && head == l[0] && l[|l|-1].next == null) &&
(forall i in [0..|l|-1] :: l[i].next == l[i+1])
}
method init()
requires acc(this.*);
ensures acc(rep) && acc(l) && acc(l[*].data) && acc(l[*].next) && acc(head) && acc(size) && inv();
{
rep := nil<int>;
l := nil<Node2>;
head := null;
size := 0;
}
function length(): int
requires acc(rep) && acc(l) && acc(l[*].data) && acc(l[*].next) && acc(head) && acc(size) && inv();
{
size
}
method checkLength()
requires acc(rep) && acc(l) && acc(l[*].data) && acc(l[*].next) && acc(head) && acc(size) && inv();
{
assert length() == |l|;
}
method get(i: int) returns (v: int)
requires acc(rep) && acc(l) && acc(l[*].data) && acc(l[*].next) && acc(head) && acc(size) && inv();
requires 0 <= i && i < length();
ensures acc(rep) && acc(l) && acc(l[*].data) && acc(l[*].next) && acc(head) && acc(size) && inv();
{
call v := getrec(i, head, 0);
assert v == l[i].data;
}
method getrec(i: int, n: Node2, /* ghost */ j: int) returns (v: int)
requires acc(rep) && acc(l) && acc(l[*].data) && acc(l[*].next) && acc(head) && acc(size) && inv();
requires length() == |l|;
requires 0 <= i && i < length();
requires 0 <= j && j <= i;
requires l[j] == n;
ensures acc(rep) && acc(l) && acc(l[*].data) && acc(l[*].next) && acc(head) && acc(size) && inv();
// frame
ensures l == old(l);
ensures forall x in l :: x != null && x.data == old(x.data) && x.next == old(x.next);
ensures size == old(size);
ensures head == old(head);
ensures rep == old(rep);
ensures v == l[i].data;
ensures l == old(l);
{
if (i == j) {
v := n.data;
} else {
call v := getrec(i, n.next, j+1);
}
}
}
|
