4 files changed, 206 insertions, 0 deletions
diff --git a/Chalice/refinements/Answer b/Chalice/refinements/Answer
index b513e041..6db2a988 100644
--- a/Chalice/refinements/Answer
+++ b/Chalice/refinements/Answer
@@ -29,3 +29,9 @@ Processing Pick.chalice
   26.25: Sequence index might be larger than or equal to the length of the sequence.
 
 Boogie program verifier finished with 11 verified, 1 error
+Processing TestCoupling.chalice
+  35.13: The postcondition at 35.13 might not hold. Insufficient fraction at 35.13 for A1.y.
+  62.38: Location might not be readable.
+  66.5: Location might not be writable
+
+Boogie program verifier finished with 17 verified, 3 errors
diff --git a/Chalice/refinements/Counter.chalice b/Chalice/refinements/Counter.chalice
new file mode 100644
index 00000000..c9576a13
--- /dev/null
+++ b/Chalice/refinements/Counter.chalice
@@ -0,0 +1,125 @@
+class Counter0 {
+  var x: int;
+  
+  method init() 
+    requires acc(x); 
+    ensures acc(x) && x == 0;
+  {
+    x := 0;  
+  }
+
+  method inc()
+    requires acc(x);
+    ensures acc(x) && x == old(x) + 1;
+  {
+    x := x + 1;
+  } 
+
+  method dec()
+    requires acc(x);
+    ensures acc(x) && x == old(x) - 1;
+  {    
+    x := x - 1;  
+  }
+
+  /** Interesting issues */  
+
+  /* We can expose representation here */
+  method magic1() returns (c: Cell) 
+    requires acc(x)
+    ensures acc(c.n) && x == old(x);
+  {
+    var c [acc(c.n)];
+  }
+
+  /* This should prevent us from exposing representation */
+  method magic2() returns (c: Cell)
+    requires acc(x);
+    ensures acc(x) && x == old(x) && acc(c.n);
+  {
+    var c [acc(c.n)];
+  }
+}
+
+class Counter1 refines Counter0 {
+  var y: int;
+  var z: int;  
+  replaces x by acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0;
+  
+  transforms init() 
+  {
+    replaces * by {this.y := 0; this.z := 0;}
+  }
+
+  transforms inc()
+  {    
+    replaces * by {this.y := this.y + 1;}
+  }
+
+  transforms dec() 
+  {
+    replaces * by {this.z := this.z + 1;}
+  }       
+
+  /** This violates abstraction of x -- we must hold all permissions to x to update it */
+  method magic3() 
+    requires acc(y);    
+  {
+    y := y + 1;
+  }
+
+  /** This does also -- but it also prohibits us from reading part of the state across refinement */
+  method magic4() returns (i)
+    requires acc(y);
+  {
+    i := y;
+  }
+}
+
+class Cell {var n: int}
+/*
+class Counter2 refines Counter1 {
+  var a: Cell;
+  var b: Cell;
+  replaces y, z by acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n;
+  
+  transforms init() 
+  {
+    replaces * by {
+      this.a := new Cell {n := 0};
+      this.b := new Cell {n := 0};
+    }
+  }
+
+  transforms inc() 
+  {
+    replaces * by {this.a.n := this.a.n + 1;}
+  }
+
+  transforms dec()
+  {
+    replaces * by {this.b.n := this.b.n + 1;}
+  }
+
+  transforms magic1() returns (c: Cell)
+  {
+    replaces * by {c := this.a;}
+  }
+
+  transforms magic2() returns (c: Cell)
+  {
+    replaces * by {c := this.a;}
+  }
+
+  transforms magic3()
+  {
+    replaces * by {this.a.n := this.a.n + 1;}
+  }
+
+  transforms magic4() returns (i)
+  {
+    replaces * by {i := this.a.n;}
+  }
+}
+*/
+  
diff --git a/Chalice/refinements/TestCoupling.chalice b/Chalice/refinements/TestCoupling.chalice
new file mode 100644
index 00000000..a178c9b4
--- /dev/null
+++ b/Chalice/refinements/TestCoupling.chalice
@@ -0,0 +1,74 @@
+class A0 {
+  var x: int;
+  var n: int;
+  var k: int;
+  
+  method inc()
+    requires acc(x) && acc(n);
+    ensures acc(x) && x == old(x) + 1;
+  {
+    x := x + 1;
+    n := n + 1;
+  }
+
+  method error() 
+    requires acc(x)
+    ensures acc(x)
+  {
+    x := x + 1;
+  } 
+}
+
+class A1 refines A0 {
+  var y: int;
+  var z: int;  
+  replaces x by acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0;
+  
+  refines inc()
+    ensures y == old(y) + 1
+  {
+    this.y := 1 + this.y;
+    this.n := this.n + 1;    
+  }
+
+  refines error()     
+    ensures acc(y)
+  {
+    this.y := 1 + this.y;
+  }
+}
+
+class B0 {
+  var x: int; 
+  var y: int;
+  
+  method error()
+    requires acc(x);
+    ensures acc(x);
+  {
+    x := x + 1;     
+  }
+  
+  method inc()
+    requires acc(x) && acc(y);
+    ensures acc(x) && acc(y);
+  { 
+    x := x + 1;
+  }
+}
+
+class B1 refines B0 {
+  var z: int;
+  replaces x,y by acc(z) && z == x + y;
+
+  refines error() 
+  {
+    this.z := this.z + 1;
+  }
+
+  refines inc() 
+  {
+    this.z := this.z + 1;
+  }
+}
+   
diff --git a/Chalice/refinements/test.sh b/Chalice/refinements/test.sh
index 73ede390..24dbd6e5 100644
--- a/Chalice/refinements/test.sh
+++ b/Chalice/refinements/test.sh
@@ -13,6 +13,7 @@ TESTS="
   RecFiniteDiff.chalice
   LoopFiniteDiff.chalice
   Pick.chalice
+  TestCoupling.chalice
 "
 
 # Switch to test directory