blob: 1f752fda11cb4150382ba5ece0fefeb750377e94 (
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
|
class Cell {
var x: int;
// --- some predicates ---
predicate write1 { acc(x) } // full permission in a predicate
predicate write2 { acc(x,10) } // 10%
predicate read1 { rd(x) } // fractional read permission
predicate read2 { rd*(x) } // starred fractional read permission
predicate read3 { rd(x,1) } // counting permission (1 epsilon)
// --- basic tests ---
method b1()
requires write1 && write2 && read1 && read2 && read3;
ensures write1 && write2 && read1 && read2 && read3;
{
}
method b2()
requires write1;
ensures read1;
{
unfold write1;
fold read1;
}
method b3()
requires read1;
ensures read3;
{
unfold read1;
fold read3;
fold read2;
fold read3;
fold read2;
fold write1; // ERROR: should fail
}
method b4()
requires read2;
ensures read2;
{
unfold read2;
call dispose();
fold read2;
}
method b5()
requires read1;
ensures read1;
{
unfold read1;
call dispose();
fold read1; // ERROR: should fail
}
method b6()
requires acc(x);
ensures acc(x);
{
fold read1;
unfold read1;
}
method b7() // ERROR: precondition does not hold
requires acc(x);
ensures acc(x);
{
fold read2;
unfold read2;
}
method b8()
requires acc(x);
ensures acc(x);
{
fold read3;
unfold read3;
}
method b9()
requires acc(x);
ensures acc(x);
{
fold write1;
unfold write1;
}
method b10()
requires acc(x);
ensures acc(x);
{
fold write2;
unfold write2;
}
// --- helper functions ---
method void() requires rd(x); ensures rd(x); {}
method dispose() requires rd(x); {}
}
|
