3 files changed, 152 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index deb4a2fc..8e4c2f12 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1370,8 +1370,14 @@ Predicates.dfy[B](17,15): Related location: This is the postcondition that might
 Predicates.dfy(28,9): Related location: Related location
 Execution trace:
     (0,0): anon0
+Predicates.dfy(85,18): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Predicates.dfy(89,16): Error: assertion violation
+Execution trace:
+    (0,0): anon0
 
-Dafny program verifier finished with 9 verified, 1 error
+Dafny program verifier finished with 26 verified, 3 errors
 
 -------------------- SmallTests.dfy --------------------
 SmallTests.dfy(30,11): Error: index out of range
diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy
index 76666ef0..2583ef19 100644
--- a/Test/dafny0/Predicates.dfy
+++ b/Test/dafny0/Predicates.dfy
@@ -29,3 +29,77 @@ module B refines A {
     }
   }
 }
+
+// ------------------------------------------------
+
+module Loose {
+  class MyNumber {
+    var N: int;
+    ghost var Repr: set<object>;
+    predicate Valid
+      reads this, Repr;
+    {
+      this in Repr && null !in Repr &&
+      0 <= N
+    }
+    constructor Init()
+      modifies this;
+      ensures Valid && fresh(Repr - {this});
+    {
+      N, Repr := 0, {this};
+    }
+    method Inc()
+      requires Valid;
+      modifies Repr;
+      ensures old(N) < N;
+      ensures Valid && fresh(Repr - old(Repr));
+    {
+      N := N + 2;
+    }
+    method Get() returns (n: int)
+      requires Valid;
+      ensures n == N;
+    {
+      n := N;
+    }
+  }
+}
+
+module Tight refines Loose {
+  class MyNumber {
+    predicate Valid
+    {
+      N % 2 == 0
+    }
+    constructor Init()
+      ensures N == 0;
+    method Inc()
+      ensures N == old(N) + 2;
+  }
+}
+
+module UnawareClient imports Loose {
+  class Client {
+    method Main() {
+      var n := new MyNumber.Init();
+      assert n.N == 0;  // error: this is not known
+      n.Inc();
+      n.Inc();
+      var k := n.Get();
+      assert k == 4;  // error: this is not known
+    }
+  }
+}
+
+module AwareClient imports Tight {
+  class Client {
+    method Main() {
+      var n := new MyNumber.Init();
+      assert n.N == 0;
+      n.Inc();
+      n.Inc();
+      var k := n.Get();
+      assert k == 4;
+    }
+  }
+}
diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy
index e46fba0d..fb379c33 100644
--- a/Test/dafny0/Refinement.dfy
+++ b/Test/dafny0/Refinement.dfy
@@ -31,3 +31,74 @@ module B refines A {
                           // inherited method body
   }
 }
+
+// ------------------------------------------------
+/*  SOON
+module Abstract {
+  class MyNumber {
+    var N: int;
+    ghost var Repr: set<object>;
+    predicate Valid
+      reads this, Repr;
+    {
+      this in Repr && null !in Repr
+    }
+    constructor Init()
+      modifies this;
+      ensures N == 0;
+      ensures Valid && fresh(Repr - {this});
+    {
+      N, Repr := 0, {this};
+    }
+    method Inc()
+      requires Valid;
+      modifies Repr;
+      ensures N == old(N) + 1;
+      ensures Valid && fresh(Repr - old(Repr));
+    {
+      N := N + 1;
+    }
+    method Get() returns (n: int)
+      requires Valid;
+      ensures n == N;
+    {
+      n := N;
+    }
+  }
+}
+
+module Concrete refines Abstract {
+  class MyNumber {
+    var a: int;
+    var b: int;
+    predicate Valid
+    {
+      N == a - b
+    }
+    constructor Init()
+    {
+      a := b;
+    }
+    method Inc()
+    {
+      if (*) { a := a + 1; } else { b := b - 1; }
+    }
+    method Get() returns (n: int)
+    {
+      n := a - b;
+    }
+  }
+}
+
+module Client imports Concrete {
+  class TheClient {
+    method Main() {
+      var n := new MyNumber.Init();
+      n.Inc();
+      n.Inc();
+      var k := n.Get();
+      assert k == 2;
+    }
+  }
+}
+*/