Chalice: New permission model that provides more abstraction and more flexibility. Details of the model can be found in the paper 'Fractional Permissions without the Fractions', FTfJP 2011 (see http://www.pm.inf.ethz.ch/publications/).

This changeset also fixes several bugs not directly related to the permissions model and improves the error handling. The following features have been added or enhanced:
- Error handling: If exceptions (e.g. about not supported features) are encountered, a user-friendly message is displayed
- Sequence axioms: There is an additional axiom for singleton lists, which is helpful in some cases
- Prelude: Chalice's prelude has been split into sections (e.g. one for permission-related stuff, one for sequence axioms, and so on), which are included on demand (less superfluous axioms, etc.)
Currently not working - but planned to be updated as well - are the following features:
- Stepwise refinements
- autoFold
- read locks
There is a performance issue with permission scaling (i.e., taking non-full versions of predicates that contain read-permissions). Details can be found in the following file: Chalice/tests/permission-model/scaling.chalice.

A list of fixed bugs (see http://boogie.codeplex.com/workitem/<workitem number> for details on the individual bugs)
- workitem 10200: Issue with the axiom of framing functions
- workitem 10197: The translation of old(waitlevel) resultet in Boogie error
- workitem 10196: Quantification over empty sequences
- workitem 10195: Contradiction when descending sequences are used
- workitem 10192: Invalid translation of old-construct in certain cases
- workitem 10190: Stack overflow when parsing large comment blocks
- workitem 10147: Duplicated method parameters and return values are not detected

1 files changed, 63 insertions, 0 deletions

diff --git a/Chalice/tests/examples/Sieve.chalice b/Chalice/tests/examples/Sieve.chalice
new file mode 100644
index 00000000..d7223d04
--- /dev/null
+++ b/Chalice/tests/examples/Sieve.chalice
@@ -0,0 +1,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) { }

+}