blob: e79cded926d23a99f8dd3b172fa3d7afce7e6606 (
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
|
/* Example taken from ESOP submission */
class T {
var k: int;
var l: int;
method run()
requires acc(k);
ensures acc(k) && k == old(k) + 1;
{
k := k + 1;
}
}
class Program {
method main() {
var x := new T;
x.k := 17;
x.l := 20;
fork tok := x.run();
x.l := 10;
join tok;
assert x.k == 18 && x.l == 10;
}
method justJoin(tok: token<T.run>, x: T) returns (rt: int)
requires x!=null && tok!=null && acc(tok.joinable) && tok.joinable && eval(tok.fork x.run(), acc(x.k));
ensures rt == old(eval(tok.fork x.run(), x.k)) + 1;
{
join tok;
rt := x.k;
}
}
/* example using asynchronous method calls */
class C {
var x: int;
method m(v: int) returns (rt: int)
ensures rt == v + 1;
{
rt := v + 1;
}
}
class Program2 {
method main1(){
var c := new C;
var tok: token<C.m>;
fork tok := c.m(5);
// do some computation
var x : int;
join x := tok;
assert x == 6;
}
method main2(){
var c := new C;
var tok: token<C.m>;
fork tok := c.m(5);
// do some computation
call foo(tok, c);
}
method foo(tok: token<C.m>, o: C)
requires tok!=null && acc(tok.joinable) && tok.joinable && eval(tok.fork o.m(5), true);
{
var x: int;
join x := tok;
assert x == 6;
}
}
|
