blob: 299303461dba7eeb30385c61d50d8e22f4b22d07 (
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
|
/*
Note: At the moment, there is a performance problem if permissions are scaled.
If a predicate (such as read1 below) contains a read permission, and one takes
read access to that predicate (as in method s1; rd(read1)), then this
effectively means that the fractions corresponding to the two read permissions
are multiplied. This introduces non-linear arithmetic in Boogie, which can be
very hard and unpredicable for the theorem prover. For this reason, this test is
taking a very long time to complete.
-- Stefan Heule, June 2011
*/
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); {}
}
|
