blob: ffe9aac14d3eade9b03ff91bf9dcfcc0b3962f0d (
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
|
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) } // abstract read permission
predicate read2 { rd*(x) } // starred read permission
predicate read3 { rd(x,1) } // counting permission (1 epsilon)
// --- permission scaling ---
method s1()
requires rd(read1);
{
unfold rd(read1);
assert(rd*(x));
assert(rd(x)); // ERROR: should fail
}
method s2() // INCOMPLETNESS: postcondition should hold, but fails at the moment
requires rd(read1);
ensures rd(read1);
{
unfold rd(read1);
fold rd(read1);
}
method s3()
requires acc(x);
ensures rd(read1);
{
fold rd(read1);
assert(rd*(x));
assert(acc(x)); // ERROR: should fail
}
method s4() // ERROR: postcondition does not hold
requires acc(x);
ensures read1;
{
fold rd(read1);
}
method s5()
requires rd(read2);
{
unfold rd(read2);
assert(rd*(x));
assert(rd(x)); // ERROR: should fail
}
method s6()
requires acc(x);
ensures rd(read2);
{
fold rd(read2);
assert(rd*(x));
assert(acc(x)); // ERROR: should fail
}
method s7() // ERROR: postcondition does not hold
requires acc(x);
ensures read2;
{
fold rd(read2);
}
// --- helper functions ---
method void() requires rd(x); ensures rd(x); {}
method dispose() requires rd(x); {}
}
|
