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
|
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 maxlock;
}
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 { }
|