blob: d7223d04a5f580a048ee5b2075bcbd22c1ab5f08 (
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
|
channel NumberStream(x: int) where 2 <= x ==> credit(this);
class Sieve {
method Counter(n: NumberStream, to: int) // sends the plurals along n
requires rd(n.mu) && credit(n,-1) && 0 <= to;
{
var i := 2;
while (i < to)
invariant rd(n.mu);
invariant 2 <= i;
invariant credit(n, -1)
{
send n(i);
i := i + 1;
}
send n(-1);
}
method Filter(prime: int, r: NumberStream, s: NumberStream)
requires 2 <= prime;
requires rd(r.mu) && waitlevel << r.mu;
requires rd(s.mu) && s.mu << r.mu && credit(r) && credit(s, -1);
{
receive x := r;
while (2 <= x)
invariant rd(r.mu) && rd(s.mu) && s << r && waitlevel << r.mu;
invariant 2<= x ==> credit(r);
invariant credit(s, -1);
{
if (x % prime != 0) { // suppress multiples of prime
send s(x);
}
receive x := r;
}
send s(-1);
}
method Start()
{
var ch := new NumberStream;
fork Counter(ch, 101);
var p: int;
receive p := ch;
while (2 <= p)
invariant ch != null;
invariant 2 <= p ==> credit(ch, 1);
invariant rd*(ch.mu) && waitlevel << ch.mu;
{
// print p--it's a prime!
var cp := new ChalicePrint; call cp.Int(p);
var n := new NumberStream between waitlevel and ch;
fork Filter(p, ch, n);
ch := n;
receive p := ch;
}
}
}
external class ChalicePrint {
method Int(x: int) { }
}
|
