Dafny: beefed up allocation axioms for boxes stored in fields

1 files changed, 27 insertions, 0 deletions

diff --git a/Test/dafny2/TreeFill.dfy b/Test/dafny2/TreeFill.dfy
new file mode 100644
index 00000000..f7e2cc89
--- /dev/null
+++ b/Test/dafny2/TreeFill.dfy
@@ -0,0 +1,27 @@
+datatype Tree<T> = Null | Node(Tree, T, Tree);

+

+function Contains<T>(t: Tree, v: T): bool

+{

+  match t

+  case Null => false

+  case Node(left, x, right) => x == v || Contains(left, v) || Contains(right, v)

+}

+

+method Fill<T>(t: Tree, a: array<T>, start: int) returns (end: int)

+  requires a != null && 0 <= start <= a.Length;

+  modifies a;

+  ensures start <= end <= a.Length;

+  ensures forall i :: 0 <= i < start ==> a[i] == old(a[i]);

+  ensures forall i :: start <= i < end ==> Contains(t, a[i]);

+{

+  match (t) {

+    case Null =>

+      end := start;

+    case Node(left, x, right) =>

+      end := Fill(left, a, start);

+      if (end < a.Length) {

+        a[end] := x;

+        end := Fill(right, a, end + 1);

+      }

+  }

+}