diff options
| author |  rustanleino <unknown> | 2009-10-15 17:34:31 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-10-15 17:34:31 +0000 |
| commit | 4de49bb033ecde8d4fa6fa3327c20ce2ac001387 (patch) | |
| tree | 1efd7db3e19c39162825405984715f39e8035d61 | |
| parent | 1f63aa9d54161eaeba72c339c649a7db96bca006 (diff) | |
Sieve of Eratosthenes, written in Chalice.
| -rw-r--r-- | Chalice/examples/Sieve.chalice | 64 | ||||
| -rw-r--r-- | Chalice/src/Chalice.cs | 7 |
2 files changed, 71 insertions, 0 deletions
diff --git a/Chalice/examples/Sieve.chalice b/Chalice/examples/Sieve.chalice new file mode 100644 index 00000000..402b7e43 --- /dev/null +++ b/Chalice/examples/Sieve.chalice @@ -0,0 +1,64 @@ +channel NumberStream(x: int) where 2 <= x && credit(this);
+
+class Sieve {
+ method Counter(n: NumberStream) // sends the plurals along n
+ requires rd(n.mu) && credit(n,-1);
+ {
+ var i := 2;
+ while (true)
+ invariant rd(n.mu);
+ invariant 2 <= i;
+ {
+ send n(i);
+ i := i + 1;
+ if (i == 120) {
+ var done := new ChaliceSystem; call done.Done();
+ }
+ }
+ }
+
+ method Filter(prime: int, r: NumberStream, s: NumberStream)
+ requires 2 <= prime;
+ requires rd(r.mu) && maxlock << r.mu;
+ requires rd(s.mu) && s.mu << r.mu && credit(s,-1);
+ {
+ while (true)
+ invariant rd(r.mu) && maxlock << r.mu;
+ invariant credit(r);
+ invariant rd(s.mu);
+ {
+ var x: int;
+ receive x := r;
+ if (x % prime != 0) { // suppress multiples of prime
+ send s(x);
+ }
+ }
+ }
+
+ method Start()
+ {
+ var ch := new NumberStream;
+ fork Counter(ch);
+ var p: int;
+ receive p := ch;
+ while (p < 100)
+ invariant 2 <= p;
+ invariant rd(ch.mu) && maxlock << ch.mu;
+ {
+ // print p--it's a prime!
+ var cp := new ChalicePrint; call cp.Int(p);
+
+ var n := new NumberStream between maxlock and ch;
+ fork Filter(p, ch, n);
+ ch := n;
+ receive p := ch;
+ }
+ }
+}
+
+external class ChalicePrint {
+ method Int(x: int) { }
+}
+external class ChaliceSystem {
+ method Done() { }
+}
diff --git a/Chalice/src/Chalice.cs b/Chalice/src/Chalice.cs index 4865db69..60e2afa9 100644 --- a/Chalice/src/Chalice.cs +++ b/Chalice/src/Chalice.cs @@ -96,4 +96,11 @@ namespace Chalice System.Console.WriteLine(x);
}
}
+
+ public class ChaliceSystem {
+ public void Done() {
+ ChannelBuffer<int> buffer = new ChannelBuffer<int>();
+ buffer.Remove();
+ }
+ }
}
|