blob: 0de8a987be4a75a951f944cc621d65a4666fcf98 (
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
|
class Client {
method main(p: Problem, s: Solver) returns (r: int)
requires acc(p.f) && s != null
ensures acc(p.f)
{
// start randomized computations
var tk1: token<Solver.solve>
var tk2: token<Solver.solve>
call tk1 := s.start(p)
call tk2 := s.start(p)
// get the results
var r1: int
join r1 := tk1
var r2: int
join r2:= tk2
r := r1 > r2 ? r1 : r2
}
}
class Solver {
method solve(p: Problem, d: Data) returns (r: int)
requires rd(p.f)
requires acc(d.*)
ensures rd(p.f)
{ /* ... */ }
method start(p: Problem)
returns (tk: token<Solver.solve>)
requires rd(p.f)
ensures acc(p.f, rd-rd(tk))
ensures acc(tk.joinable) && tk.joinable;
ensures eval(tk.fork this.solve(p,_), true)
{
var d: Data := new Data
/* .. perform some set-up/initialization and prepare the data d for the solve method */
fork tk := solve(p, d)
}
}
class Problem { var f: int }
class Data { var f: int; var g: int }
|
