diff options
| author |  Rustan Leino <unknown> | 2013-08-04 17:55:06 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-08-04 17:55:06 -0700 |
| commit | a1710a324a8d92935cd7bc8ecbda115b9cd09748 (patch) | |
| tree | 0da87df5c79764cc7d46da695561ea8134f60146 /Test/dafny0/Iterators.dfy | |
| parent | 8af0f2d97ab5ca1a212c7f4901c43059ccb08e36 (diff) | |
Set up call-graph to keep track of edges between functions and methods. (To be done: replace InMethodContext with a Function/Method-Height in translator.)
Diffstat (limited to 'Test/dafny0/Iterators.dfy')
| -rw-r--r-- | Test/dafny0/Iterators.dfy | 145 |
1 files changed, 145 insertions, 0 deletions
diff --git a/Test/dafny0/Iterators.dfy b/Test/dafny0/Iterators.dfy index e0c58867..f4d36762 100644 --- a/Test/dafny0/Iterators.dfy +++ b/Test/dafny0/Iterators.dfy @@ -233,3 +233,148 @@ method ClientOfNewReferences() i := i - 1;
}
}
+
+// ------ recursive iterators --------------------------------------
+
+module ITER_A {
+ iterator RecursiveIterator(n: nat, r: RecIterCaller, good: bool)
+ requires r != null;
+ decreases n+2, 0;
+ {
+ if n == 0 {
+ } else if good {
+ r.M(n - 1);
+ } else {
+ r.M(n + 1); // error: may fail to terminate
+ }
+ }
+
+ class RecIterCaller {
+ method M(n: nat)
+ decreases n+2;
+ {
+ var good;
+ var iter := new RecursiveIterator(n, this, good);
+ var more := iter.MoveNext();
+ }
+ }
+}
+module ITER_B {
+ iterator RecursiveIterator(n: nat, r: RecIterCaller, good: bool)
+ requires r != null;
+ decreases n;
+ {
+ if n == 0 {
+ } else if good {
+ r.M(n - 1);
+ } else {
+ r.M(n + 1); // error: may fail to terminate
+ }
+ }
+
+ class RecIterCaller {
+ method M(n: nat)
+ decreases n;
+ {
+ var good;
+ var iter := new RecursiveIterator(n, this, good);
+ var more := iter.MoveNext(); // error: failure to decrease variant function
+ }
+ }
+}
+module ITER_C {
+ iterator RecursiveIterator(n: nat, r: RecIterCaller, good: bool)
+ requires r != null;
+ {
+ if n == 0 {
+ } else if good {
+ r.M(n - 1);
+ } else {
+ r.M(n + 1); // error: may fail to terminate
+ }
+ }
+
+ class RecIterCaller {
+ method M(n: nat)
+ {
+ var good;
+ var iter := new RecursiveIterator(n, this, good);
+ var more := iter.MoveNext();
+ }
+ }
+}
+module ITER_D {
+ iterator RecursiveIterator(n: nat, r: RecIterCaller, good: bool)
+ requires r != null;
+ {
+ if n == 0 {
+ } else if good {
+ r.M(n - 1, {});
+ } else {
+ r.M(n + 1, {}); // error: may fail to terminate
+ }
+ }
+
+ class RecIterCaller {
+ method M(n: nat, incomparable: set<int>)
+ {
+ var good;
+ var iter := new RecursiveIterator(n, this, good);
+ var more := iter.MoveNext(); // error: failure to decrease variant function
+ }
+ }
+}
+module ITER_E {
+ class Cell {
+ var data: nat;
+ }
+ iterator RecursiveIterator(cell: Cell, n: nat, r: RecIterCaller, good: bool)
+ requires cell != null && r != null;
+ modifies cell;
+ decreases if cell.data < 2 then n else n+n-n;
+ {
+ if n == 0 {
+ } else if good {
+ r.M(n - 1);
+ } else {
+ r.M(n + 1); // error: may fail to terminate
+ }
+ }
+
+ class RecIterCaller {
+ method M(n: nat)
+ {
+ var good;
+ var cell := new Cell;
+ var iter := new RecursiveIterator(cell, n, this, good);
+ var more := iter.MoveNext(); // error: failure to decrease variant function
+ }
+ }
+}
+module ITER_F {
+ class Cell {
+ var data: nat;
+ }
+ iterator RecursiveIterator(cell: Cell, n: nat, r: RecIterCaller, good: bool)
+ requires cell != null && r != null;
+ modifies cell;
+ decreases if cell.data < 2 then n else n+n-n, 0;
+ {
+ if n == 0 {
+ } else if good {
+ r.M(n - 1);
+ } else {
+ r.M(n + 1); // error: may fail to terminate
+ }
+ }
+
+ class RecIterCaller {
+ method M(n: nat)
+ {
+ var good;
+ var cell := new Cell;
+ var iter := new RecursiveIterator(cell, n, this, good);
+ var more := iter.MoveNext();
+ }
+ }
+}
|