blob: 0560945d5bac3c4da78d70b1ff67ee898afa9b86 (
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
|
class Program {
var x: int;
method a(a: seq<A>)
requires |a| > 2;
requires rd(a[*].f);
requires forall i in [0..|a|-1] :: a[i] != null;
requires a[0].f == 1;
ensures rd(a[*].f);
{
assert rd(a[*].f);
call b(a);
}
method b(a: seq<A>)
requires |a| > 2;
requires rd(a[*].f);
requires forall i in [0..|a|-1] :: a[i] != null;
requires a[0].f == 1;
ensures rd(a[*].f);
{
assert rd(a[*].f);
}
method c(a: seq<A>)
requires |a| > 2;
requires rd(a[*].f);
requires forall i in [0..|a|-1] :: a[i] != null;
requires a[0].f == 1;
ensures rd(a[*].f);
{
call void(a[1]);
call void(a[0]);
}
method c1(a: seq<A>) // ERROR: should fail to verify postcondition
requires |a| > 2;
requires rd(a[*].f);
requires forall i in [0..|a|-1] :: a[i] != null;
requires a[0].f == 1;
ensures rd(a[*].f);
{
call dispose(a[1]);
}
method d(a: seq<A>)
requires |a| > 2;
requires rd(a[*].f);
requires forall i in [0..|a|-1] :: a[i] != null;
requires a[0].f == 1;
ensures rd*(a[*].f);
{
call dispose(a[1]); // we don't give away all the permission, thus verification succeeds
var x: int;
call x := some_number();
call dispose(a[x]); // slighly more interesting, but still clearly ok
}
method e(a: seq<A>) // ERROR: should fail to verify postcondition
requires |a| > 2;
requires acc(a[*].f,10);
requires forall i in [0..|a|-1] :: a[i] != null;
requires a[0].f == 1;
ensures rd*(a[*].f);
{
var x: int;
call x := some_number();
call dispose2(a[x]);
}
method some_number() returns (a: int)
ensures 0 <= a && a < 3;
{
a := 1;
}
method dispose(a: A) requires rd(a.f); {}
method dispose2(a: A) requires acc(a.f,10); {}
method void(a: A) requires rd(a.f); ensures rd(a.f); {}
}
class A {
var f: int;
}
|
