blob: 6ad8e592184cfc82cf3411236fd98929dec9f248 (
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
|
class C
{
var value:int;
predicate inv { acc(value) }
function get():int
requires inv;
{
unfolding inv in value
}
method set(newval:int)
requires inv;
ensures inv && get()==newval;
{
unfold inv;
value:=newval;
fold inv;
}
method callmethod0()
requires inv;
ensures inv && get()==3;
{
call set(3);
}
method callmethod1()
{
call set(3); // ERROR: should fail
}
method ifc()
requires inv;
ensures inv && get()>old(get())
{
if(get()>0) { call set(get()+get()); }
else { call set(2); }
}
method loop0() returns (r:int)
requires inv && get()>0;
ensures inv && r==get();
{
r:=0;
while (r<unfolding inv in value)
invariant inv && r<=get();
{ r:=r+1; }
}
method loop1() returns (r:int)
requires inv && get()>0;
ensures inv && r==get();
{
r:=0;
while (r<get())
invariant inv && r<=unfolding inv in value;
{ r:=r+1; }
}
method uf0()
requires acc(value);
{
assert acc(value);
fold inv;
assert acc(value); // ERROR: should fail
}
method uf1()
requires acc(value);
{
assert acc(value);
fold inv;
assert acc(inv);
}
method uf2()
requires inv;
{
assert inv;
unfold inv;
assert acc(value);
}
method uf3()
requires inv;
{
assert inv;
unfold inv;
assert acc(inv); // ERROR: should fail
}
method badframing0()
requires get()==2; // ERROR: should fail
{}
method badframing1()
requires value==2; // ERROR: should fail
{}
method badframing2()
requires acc(value) && get()==2; // ERROR: should fail
{}
method badframing3()
requires inv && value==2; // ERROR: should fail
{}
}
|
