1 files changed, 81 insertions, 0 deletions
diff --git a/Test/dafny0/Reads.dfy b/Test/dafny0/Reads.dfy
index 645494cb..6dedbada 100644
--- a/Test/dafny0/Reads.dfy
+++ b/Test/dafny0/Reads.dfy
@@ -55,3 +55,84 @@ function ok5(r : R):()
   reads if r != null then {r, r.r} else {};
 {()}
 
+// Reads checking where there are circularities among the expressions
+
+class CircularChecking {
+  ghost var Repr: set<object>
+    
+  function F(): int
+    reads this, Repr
+
+  function F'(): int
+    reads Repr, this  // this is also fine
+
+  function G0(): int
+    reads this
+    requires Repr == {} && F() == 100
+
+  function G1(): int
+    reads this
+    requires F() == 100  // fine, since the next line tells us that Repr is empty
+    requires Repr == {}
+
+  function H0(cell: Cell): int
+    reads Repr  // by itself, this reads is not self-framing
+    requires this in Repr  // lo and behold!  So, reads clause is fine after all
+
+  function H1(cell: Cell): int
+    reads this, Repr
+    requires cell in Repr
+    requires cell != null && cell.data == 10
+
+  function H2(cell: Cell): int
+    reads this, Repr
+    requires cell != null && cell.data == 10  // this is okay, too, since reads checks are postponed
+    requires cell in Repr
+}
+
+class Cell { var data: int }
+
+// Test the benefits of the new reads checking for function checking
+
+function ApplyToSet<X>(S: set<X>, f: X -> X): set<X>
+  requires forall x :: x in S ==> f.reads(x) == {} && f.requires(x)
+{
+  if S == {} then {} else
+    var x :| x in S;
+    ApplyToSet(S - {x}, f) + {f(x)}
+}
+
+function ApplyToSet_AltSignature0<X>(S: set<X>, f: X -> X): set<X>
+  requires forall x :: x in S ==> f.requires(x) && f.reads(x) == {}
+
+function ApplyToSet_AltSignature1<X>(S: set<X>, f: X -> X): set<X>
+  requires forall x :: x in S ==> f.reads(x) == {}
+  requires forall x :: x in S ==> f.requires(x)
+
+function ApplyToSet_AltSignature2<X>(S: set<X>, f: X -> X): set<X>
+  requires (forall x :: x in S ==> f.reads(x) == {}) ==> forall x :: x in S ==> f.requires(x)
+  // (this precondition would not be good enough to check the body above)
+
+function FunctionInQuantifier0(): int
+  requires exists f: int -> int :: f(10) == 100  // error (x2): precondition violation and insufficient reads
+
+function FunctionInQuantifier1(): int
+  requires exists f: int -> int :: f.requires(10) && f(10) == 100  // error: insufficient reads
+
+function FunctionInQuantifier2(): int
+  requires exists f: int -> int :: f.reads(10) == {} && f.requires(10) && f(10) == 100
+  ensures FunctionInQuantifier2() == 100
+{
+  var f: int -> int :| f.reads(10) == {} && f.requires(10) && f(10) == 100;  // fine :) :)
+  f(10)
+}
+
+class DynamicFramesIdiom {
+  ghost var Repr: set<object>
+  predicate IllFormed_Valid()
+    reads Repr  // error: reads is not self framing (notice the absence of "this")
+  {
+    this in Repr  // this says that the predicate returns true if "this in Repr", but the
+                  // predicate can also be invoked in a state where its body will evaluate to false
+  }
+}