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 {
method m() {
assert 4 + (a * 5) + (2 + 3) * (a + a);
a := a + 3;
b := a - b - c + 4 * d + 20 + --25;
b := ((((a - b) - c) + 4 * d) + 20) + --25;
c := a - (b - (c + (4 * d + (20 + 25))));
assert (X ==> Y) ==> Z <==> A ==> B ==> C;
assume A && B && (C || D || E) && F;
var x;
var y := 12 + !(x.f.g).h - (!x).f + (!x.f);
var z := new C;
y := new D;
o.f := 5;
(a + b).y := new T;
reorder (2 ==(O != 3)) != O between a,b,c and x,y,z;
reorder X ==> Y below x+5;
reorder o.f above this, null;
share o;
unshare o;
acquire o;
release o;
rd acquire o;
rd release o;
downgrade o;
var tok: token<C.m>;
fork tok := o.m();
join tok;
assert rd(x) + acc(y) + acc(z, 1/4) + old(old(k)) + null.f;
x := this.f;
call m(2,3,4);
call this.m(2,3,4);
call a,b,c := o.m();
call x := m(200);
reorder o above waitlevel;
}
method p(a,b,c) returns (x,y,z)
requires 8 + 2 == 10;
ensures 8 + 5 > 10;
requires x == y+1;
ensures old(x) < x;
{
if (x == 7) {
y := y + 1; z := z + 2;
} else if (x == 8) {
y := 2;
} else {
z := 10;
}
{ // empty block
}
if (x == 9) { }
if (x == 10) { x := 10; } else { }
var n := 0;
while (n < 100) { n := n - 1; }
while (n != 0)
invariant n % 2 == 0;
invariant sqrt2 * sqrt2 == 2;
{
n := n - 2;
}
call v,x := s.M(65);
}
}
class D { }
// ----- tests specifically of implicit locals in CALL and RECEIVE statements
class ImplicitC {
var k: int;
method MyMethod() returns (x: int, y: ImplicitC)
requires acc(k)
ensures acc(y.k) && x < y.k
{
x := k - 15;
y := this;
}
method B0() {
var c := new ImplicitC;
call a, b := c.MyMethodX(); // error: method not found (so what is done with a,b?)
assert a < b.k;
}
method B1() {
var c := new ImplicitC;
call a, a := c.MyMethod(); // error: a occurs twice
assert a < b.k;
}
method D0() {
var ch := new Ch;
var c := new ImplicitC;
send ch(c.k - 15, c); // give ourselves some credit
receive a, b := chX; // error: channel not found (so what is done with a,b?)
assert a < b.k;
}
method D1() {
var ch := new Ch;
var c := new ImplicitC;
send ch(c.k - 15, c); // give ourselves some credit
receive a, a := ch; // error: a occurs twice
assert a < b.k;
}
}
channel Ch(x: int, y: ImplicitC) where acc(y.k) && x < y.k;
|
