Boogie:

* Look for Z3 versions up to 2.15 (but did not implement a better algorithm for it).
* Added prover-path output as part of /trace flag (that probably isn't the best command-line option for it).

Dafny:
* Split off some tests from Test/dafny0 into Test/dafny1.
* Added Test/dafny1/UltraFilter.dfy.

16 files changed, 2084 insertions, 0 deletions

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
new file mode 100644
index 00000000..cf593abf
--- /dev/null
+++ b/Test/dafny1/Answer
@@ -0,0 +1,56 @@
+

+-------------------- BQueue.bpl --------------------

+

+Boogie program verifier finished with 8 verified, 0 errors

+

+-------------------- Queue.dfy --------------------

+

+Dafny program verifier finished with 22 verified, 0 errors

+

+-------------------- BinaryTree.dfy --------------------

+

+Dafny program verifier finished with 24 verified, 0 errors

+

+-------------------- UnboundedStack.dfy --------------------

+

+Dafny program verifier finished with 12 verified, 0 errors

+

+-------------------- ListCopy.dfy --------------------

+

+Dafny program verifier finished with 4 verified, 0 errors

+

+-------------------- ListReverse.dfy --------------------

+

+Dafny program verifier finished with 2 verified, 0 errors

+

+-------------------- ListContents.dfy --------------------

+

+Dafny program verifier finished with 9 verified, 0 errors

+

+-------------------- SchorrWaite.dfy --------------------

+

+Dafny program verifier finished with 10 verified, 0 errors

+

+-------------------- SumOfCubes.dfy --------------------

+

+Dafny program verifier finished with 17 verified, 0 errors

+

+-------------------- TerminationDemos.dfy --------------------

+

+Dafny program verifier finished with 10 verified, 0 errors

+

+-------------------- Substitution.dfy --------------------

+

+Dafny program verifier finished with 12 verified, 0 errors

+

+-------------------- TreeDatatype.dfy --------------------

+

+Dafny program verifier finished with 6 verified, 0 errors

+

+-------------------- Celebrity.dfy --------------------

+

+Dafny program verifier finished with 11 verified, 0 errors

+

+-------------------- UltraFilter.dfy --------------------

+

+Dafny program verifier finished with 19 verified, 0 errors

diff --git a/Test/dafny1/BQueue.bpl b/Test/dafny1/BQueue.bpl
new file mode 100644
index 00000000..77f1efb3
--- /dev/null
+++ b/Test/dafny1/BQueue.bpl
@@ -0,0 +1,430 @@
+// BQueue.bpl

+// A queue program specified in the style of dynamic frames.

+// Rustan Leino, Michal Moskal, and Wolfram Schulte, 2007.

+

+// ---------------------------------------------------------------

+

+type ref;

+const null: ref;

+

+type Field x;

+

+// this variable represents the heap; read its type as \forall \alpha. ref * Field \alpha --> \alpha

+type HeapType = <x>[ref, Field x]x;

+var H: HeapType;

+

+// every object has an 'alloc' field, which says whether or not the object has been allocated

+const unique alloc: Field bool;

+

+// for simplicity, we say that every object has one field representing its abstract value and one

+// field representing its footprint (aka frame aka data group).

+

+const unique abstractValue: Field Seq;

+const unique footprint: Field [ref]bool;

+

+// ---------------------------------------------------------------

+

+type T;  // the type of the elements of the queue

+const NullT: T;  // some value of type T

+

+// ---------------------------------------------------------------

+

+// Queue:

+const unique head: Field ref;

+const unique tail: Field ref;

+const unique mynodes: Field [ref]bool;

+// Node:

+const unique data: Field T;

+const unique next: Field ref;

+

+function ValidQueue(HeapType, ref) returns (bool);

+axiom (forall h: HeapType, q: ref ::

+  { ValidQueue(h, q) }

+  q != null && h[q,alloc] ==>

+  (ValidQueue(h, q) <==>

+     h[q,head] != null && h[h[q,head],alloc] &&

+     h[q,tail] != null && h[h[q,tail],alloc] &&

+     h[h[q,tail], next] == null &&

+     // The following line can be suppressed now that we have a ValidFootprint invariant

+     (forall o: ref :: { h[q,footprint][o] } o != null && h[q,footprint][o] ==> h[o,alloc]) &&

+     h[q,footprint][q] &&

+     h[q,mynodes][h[q,head]] && h[q,mynodes][h[q,tail]] &&

+     (forall n: ref :: { h[q,mynodes][n] }

+       h[q,mynodes][n] ==>

+           n != null && h[n,alloc] && ValidNode(h, n) &&

+           SubSet(h[n,footprint], h[q,footprint]) &&

+           !h[n,footprint][q] &&

+           (h[n,next] == null ==> n == h[q,tail])

+     ) &&

+     (forall n: ref :: { h[n,next] }

+       h[q,mynodes][n] ==>

+           (h[n,next] != null ==> h[q,mynodes][h[n,next]])

+     ) &&

+     h[q,abstractValue] == h[h[q,head],abstractValue]

+  ));

+

+// frame axiom for ValidQueue

+axiom (forall h0: HeapType, h1: HeapType, n: ref ::

+  { ValidQueue(h0,n), ValidQueue(h1,n) }

+  (forall<alpha> o: ref, f: Field alpha :: o != null && h0[o,alloc] && h0[n,footprint][o]

+      ==> h0[o,f] == h1[o,f])

+  &&

+  (forall<alpha> o: ref, f: Field alpha :: o != null && h1[o,alloc] && h1[n,footprint][o]

+      ==> h0[o,f] == h1[o,f])

+  ==>

+  ValidQueue(h0,n) == ValidQueue(h1,n));

+

+function ValidNode(HeapType, ref) returns (bool);

+axiom (forall h: HeapType, n: ref ::

+  { ValidNode(h, n) }

+  n != null && h[n,alloc] ==>

+  (ValidNode(h, n) <==>

+     // The following line can be suppressed now that we have a ValidFootprint invariant

+     (forall o: ref :: { h[n,footprint][o] } o != null && h[n,footprint][o] ==> h[o,alloc]) &&

+     h[n,footprint][n] &&

+     (h[n,next] != null ==>

+         h[h[n,next],alloc] &&

+         SubSet(h[h[n,next], footprint], h[n,footprint]) &&

+         !h[h[n,next], footprint][n]) &&

+     (h[n,next] == null ==> EqualSeq(h[n,abstractValue], EmptySeq)) &&

+     (h[n,next] != null ==> EqualSeq(h[n,abstractValue],

+                            Append(Singleton(h[h[n,next],data]), h[h[n,next],abstractValue])))

+  ));

+

+// frame axiom for ValidNode

+axiom (forall h0: HeapType, h1: HeapType, n: ref ::

+  { ValidNode(h0,n), ValidNode(h1,n) }

+  (forall<alpha> o: ref, f: Field alpha :: o != null && h0[o,alloc] && h0[n,footprint][o]

+      ==> h0[o,f] == h1[o,f])

+  &&

+  (forall<alpha> o: ref, f: Field alpha :: o != null && h1[o,alloc] && h1[n,footprint][o]

+      ==> h0[o,f] == h1[o,f])

+  ==>

+  ValidNode(h0,n) == ValidNode(h1,n));

+

+// ---------------------------------------------------------------

+

+procedure MakeQueue() returns (q: ref)

+  requires ValidFootprints(H);

+  modifies H;

+  ensures ValidFootprints(H);

+  ensures ModifiesOnlySet(old(H), H, EmptySet);

+  ensures q != null && H[q,alloc];

+  ensures AllNewSet(old(H), H[q,footprint]);

+  ensures ValidQueue(H, q);

+  ensures Length(H[q,abstractValue]) == 0;

+{

+  var n: ref;

+

+  assume Fresh(H,q);

+  H[q,alloc] := true;

+

+  call n := MakeNode(NullT);

+  H[q,head] := n;

+  H[q,tail] := n;

+  H[q,mynodes] := SingletonSet(n);

+  H[q,footprint] := UnionSet(SingletonSet(q), H[n,footprint]);

+  H[q,abstractValue] := H[n,abstractValue];

+}

+

+procedure IsEmpty(q: ref) returns (isEmpty: bool)

+  requires ValidFootprints(H);

+  requires q != null && H[q,alloc] && ValidQueue(H, q);

+  ensures isEmpty <==> Length(H[q,abstractValue]) == 0;

+{

+  isEmpty := H[q,head] == H[q,tail];

+}

+

+procedure Enqueue(q: ref, t: T)

+  requires ValidFootprints(H);

+  requires q != null && H[q,alloc] && ValidQueue(H, q);

+  modifies H;

+  ensures ValidFootprints(H);

+  ensures ModifiesOnlySet(old(H), H, old(H)[q,footprint]);

+  ensures DifferenceIsNew(old(H), old(H)[q,footprint], H[q,footprint]);

+  ensures ValidQueue(H, q);

+  ensures EqualSeq(H[q,abstractValue], Append(old(H)[q,abstractValue], Singleton(t)));

+{

+  var n: ref;

+

+  call n := MakeNode(t);

+

+  // foreach m in q.mynodes { m.footprint := m.footprint U n.footprint }

+  call BulkUpdateFootprint(H[q,mynodes], H[n,footprint]);

+  H[q,footprint] := UnionSet(H[q,footprint], H[n,footprint]);

+

+  // foreach m in q.mynodes { m.abstractValue := Append(m.abstractValue, Singleton(t)) }

+  call BulkUpdateAbstractValue(H[q,mynodes], t);

+  H[q,abstractValue] := H[H[q,head],abstractValue];

+

+  H[q,mynodes] := UnionSet(H[q,mynodes], SingletonSet(n));

+

+  H[H[q,tail], next] := n;

+  H[q,tail] := n;

+}

+

+procedure BulkUpdateFootprint(targetSet: [ref]bool, delta: [ref]bool);

+  requires ValidFootprints(H);

+  modifies H;

+  ensures ValidFootprints(H);

+  ensures ModifiesOnlySetField(old(H), H, targetSet, footprint);

+  ensures (forall o: ref ::

+    o != null && old(H)[o,alloc] && targetSet[o]

+    ==> H[o,footprint] == UnionSet(old(H)[o,footprint], delta));

+

+procedure BulkUpdateAbstractValue(targetSet: [ref]bool, t: T);

+  requires ValidFootprints(H);

+  modifies H;

+  ensures ValidFootprints(H);

+  ensures ModifiesOnlySetField(old(H), H, targetSet, abstractValue);

+  ensures (forall o: ref ::

+    o != null && old(H)[o,alloc] && targetSet[o]

+    ==> EqualSeq(H[o,abstractValue], Append(old(H)[o,abstractValue], Singleton(t))));

+

+procedure Front(q: ref) returns (t: T)

+  requires ValidFootprints(H);

+  requires q != null && H[q,alloc] && ValidQueue(H, q);

+  requires 0 < Length(H[q,abstractValue]);

+  ensures t == Index(H[q,abstractValue], 0);

+{

+  t := H[H[H[q,head], next], data];

+}

+

+procedure Dequeue(q: ref)

+  requires ValidFootprints(H);

+  requires q != null && H[q,alloc] && ValidQueue(H, q);

+  requires 0 < Length(H[q,abstractValue]);

+  modifies H;

+  ensures ValidFootprints(H);

+  ensures ModifiesOnlySet(old(H), H, old(H)[q,footprint]);

+  ensures DifferenceIsNew(old(H), old(H)[q,footprint], H[q,footprint]);

+  ensures ValidQueue(H, q);

+  ensures EqualSeq(H[q,abstractValue], Drop(old(H)[q,abstractValue], 1));

+{

+  var n: ref;

+

+  n := H[H[q,head], next];

+  H[q,head] := n;

+  // we could also remove old(H)[q,head] from H[q,mynodes], and similar for the footprints

+  H[q,abstractValue] := H[n,abstractValue];

+}

+

+// --------------------------------------------------------------------------------

+

+procedure MakeNode(t: T) returns (n: ref)

+  requires ValidFootprints(H);

+  modifies H;

+  ensures ValidFootprints(H);

+  ensures ModifiesOnlySet(old(H), H, EmptySet);

+  ensures n != null && H[n,alloc];

+  ensures AllNewSet(old(H), H[n,footprint]);

+  ensures ValidNode(H, n);

+  ensures H[n,data] == t && H[n,next] == null;

+{

+  assume Fresh(H,n);

+  H[n,alloc] := true;

+

+  H[n,next] := null;

+  H[n,data] := t;

+  H[n,footprint] := SingletonSet(n);

+  H[n,abstractValue] := EmptySeq;

+}

+

+// --------------------------------------------------------------------------------

+

+procedure Main(t: T, u: T, v: T)

+  requires ValidFootprints(H);

+  modifies H;

+  ensures ValidFootprints(H);

+  ensures ModifiesOnlySet(old(H), H, EmptySet);

+{

+  var q0, q1: ref;

+  var w: T;

+

+  call q0 := MakeQueue();

+  call q1 := MakeQueue();

+

+  call Enqueue(q0, t);

+  call Enqueue(q0, u);

+

+  call Enqueue(q1, v);

+

+  assert Length(H[q0,abstractValue]) == 2;

+

+  call w := Front(q0);

+  assert w == t;

+  call Dequeue(q0);

+

+  call w := Front(q0);

+  assert w == u;

+

+  assert Length(H[q0,abstractValue]) == 1;

+  assert Length(H[q1,abstractValue]) == 1;

+}

+

+// --------------------------------------------------------------------------------

+

+procedure Main2(t: T, u: T, v: T, q0: ref, q1: ref)

+  requires q0 != null && H[q0,alloc] && ValidQueue(H, q0);

+  requires q1 != null && H[q1,alloc] && ValidQueue(H, q1);

+  requires DisjointSet(H[q0,footprint], H[q1,footprint]);

+  requires Length(H[q0,abstractValue]) == 0;

+

+  requires ValidFootprints(H);

+  modifies H;

+  ensures ValidFootprints(H);

+  ensures ModifiesOnlySet(old(H), H, UnionSet(old(H)[q0,footprint], old(H)[q1,footprint]));

+{

+  var w: T;

+

+  call Enqueue(q0, t);

+  call Enqueue(q0, u);

+

+  call Enqueue(q1, v);

+

+  assert Length(H[q0,abstractValue]) == 2;

+

+  call w := Front(q0);

+  assert w == t;

+  call Dequeue(q0);

+

+  call w := Front(q0);

+  assert w == u;

+

+  assert Length(H[q0,abstractValue]) == 1;

+  assert Length(H[q1,abstractValue]) == old(Length(H[q1,abstractValue])) + 1;

+}

+

+// ---------------------------------------------------------------

+

+// Helpful predicates used in specs

+

+function ModifiesOnlySet(oldHeap: HeapType, newHeap: HeapType, set: [ref]bool) returns (bool);

+axiom (forall oldHeap: HeapType, newHeap: HeapType, set: [ref]bool ::

+  { ModifiesOnlySet(oldHeap, newHeap, set) }

+  ModifiesOnlySet(oldHeap, newHeap, set) <==>

+    NoDeallocs(oldHeap, newHeap) &&

+    (forall<alpha> o: ref, f: Field alpha :: { newHeap[o,f] }

+      o != null && oldHeap[o,alloc] ==>

+      oldHeap[o,f] == newHeap[o,f] || set[o]));

+

+function ModifiesOnlySetField<alpha>(oldHeap: HeapType, newHeap: HeapType,

+                                     set: [ref]bool, field: Field alpha) returns (bool);

+axiom (forall<alpha> oldHeap: HeapType, newHeap: HeapType, set: [ref]bool, field: Field alpha ::

+  { ModifiesOnlySetField(oldHeap, newHeap, set, field) }

+  ModifiesOnlySetField(oldHeap, newHeap, set, field) <==>

+    NoDeallocs(oldHeap, newHeap) &&

+    (forall<beta> o: ref, f: Field beta :: { newHeap[o,f] }

+      o != null && oldHeap[o,alloc] ==>

+      oldHeap[o,f] == newHeap[o,f] || (set[o] && f == field)));

+

+function NoDeallocs(oldHeap: HeapType, newHeap: HeapType) returns (bool);

+axiom (forall oldHeap: HeapType, newHeap: HeapType ::

+  { NoDeallocs(oldHeap, newHeap) }

+  NoDeallocs(oldHeap, newHeap) <==>

+    (forall o: ref :: { newHeap[o,alloc] }

+      o != null && oldHeap[o,alloc] ==> newHeap[o,alloc]));

+

+function AllNewSet(oldHeap: HeapType, set: [ref]bool) returns (bool);

+axiom (forall oldHeap: HeapType, set: [ref]bool ::

+  { AllNewSet(oldHeap, set) }

+  AllNewSet(oldHeap, set) <==>

+    (forall o: ref :: { oldHeap[o,alloc] }

+      o != null && set[o] ==> !oldHeap[o,alloc]));

+

+function DifferenceIsNew(oldHeap: HeapType, oldSet: [ref]bool, newSet: [ref]bool) returns (bool);

+axiom (forall oldHeap: HeapType, oldSet: [ref]bool, newSet: [ref]bool ::

+  { DifferenceIsNew(oldHeap, oldSet, newSet) }

+  DifferenceIsNew(oldHeap, oldSet, newSet) <==>

+    (forall o: ref :: { oldHeap[o,alloc] }

+      o != null && !oldSet[o] && newSet[o] ==> !oldHeap[o,alloc]));

+

+function ValidFootprints(h: HeapType) returns (bool);

+axiom (forall h: HeapType ::

+  { ValidFootprints(h) }

+  ValidFootprints(h) <==>

+    (forall o: ref, r: ref :: { h[o,footprint][r] }

+      o != null && h[o,alloc] && r != null && h[o,footprint][r] ==> h[r,alloc]));

+

+function Fresh(h: HeapType, o: ref) returns (bool);

+axiom (forall h: HeapType, o: ref ::

+  { Fresh(h,o) }

+  Fresh(h,o) <==>

+    o != null && !h[o,alloc] && h[o,footprint] == SingletonSet(o));

+

+// ---------------------------------------------------------------

+

+const EmptySet: [ref]bool;

+axiom (forall o: ref :: { EmptySet[o] } !EmptySet[o]);

+

+function SingletonSet(ref) returns ([ref]bool);

+axiom (forall r: ref :: { SingletonSet(r) } SingletonSet(r)[r]);

+axiom (forall r: ref, o: ref :: { SingletonSet(r)[o] } SingletonSet(r)[o] <==> r == o);

+

+function UnionSet([ref]bool, [ref]bool) returns ([ref]bool);

+axiom (forall a: [ref]bool, b: [ref]bool, o: ref :: { UnionSet(a,b)[o] }

+  UnionSet(a,b)[o] <==> a[o] || b[o]);

+

+function SubSet([ref]bool, [ref]bool) returns (bool);

+axiom(forall a: [ref]bool, b: [ref]bool :: { SubSet(a,b) }

+  SubSet(a,b) <==> (forall o: ref :: {a[o]} {b[o]} a[o] ==> b[o]));

+

+function EqualSet([ref]bool, [ref]bool) returns (bool);

+axiom(forall a: [ref]bool, b: [ref]bool :: { EqualSet(a,b) }

+  EqualSet(a,b) <==> (forall o: ref :: {a[o]} {b[o]} a[o] <==> b[o]));

+

+function DisjointSet([ref]bool, [ref]bool) returns (bool);

+axiom (forall a: [ref]bool, b: [ref]bool :: { DisjointSet(a,b) }

+  DisjointSet(a,b) <==> (forall o: ref :: {a[o]} {b[o]} !a[o] || !b[o]));

+

+// ---------------------------------------------------------------

+

+// Sequence of T

+type Seq;

+

+function Length(Seq) returns (int);

+axiom (forall s: Seq :: { Length(s) } 0 <= Length(s));

+

+const EmptySeq: Seq;

+axiom Length(EmptySeq) == 0;

+axiom (forall s: Seq :: { Length(s) } Length(s) == 0 ==> s == EmptySeq);

+

+function Singleton(T) returns (Seq);

+axiom (forall t: T :: { Length(Singleton(t)) } Length(Singleton(t)) == 1);

+

+function Append(Seq, Seq) returns (Seq);

+axiom (forall s0: Seq, s1: Seq :: { Length(Append(s0,s1)) }

+  Length(Append(s0,s1)) == Length(s0) + Length(s1));

+

+function Index(Seq, int) returns (T);

+axiom (forall t: T :: { Index(Singleton(t), 0) } Index(Singleton(t), 0) == t);

+axiom (forall s0: Seq, s1: Seq, n: int :: { Index(Append(s0,s1), n) }

+  (n < Length(s0) ==> Index(Append(s0,s1), n) == Index(s0, n)) &&

+  (Length(s0) <= n ==> Index(Append(s0,s1), n) == Index(s1, n - Length(s0))));

+

+function EqualSeq(Seq, Seq) returns (bool);

+axiom (forall s0: Seq, s1: Seq :: { EqualSeq(s0,s1) }

+  EqualSeq(s0,s1) <==>

+    Length(s0) == Length(s1) &&

+    (forall j: int :: { Index(s0,j) } { Index(s1,j) }

+        0 <= j && j < Length(s0) ==> Index(s0,j) == Index(s1,j)));

+

+function Take(s: Seq, howMany: int) returns (Seq);

+axiom (forall s: Seq, n: int :: { Length(Take(s,n)) }

+  0 <= n ==>

+    (n <= Length(s) ==> Length(Take(s,n)) == n) &&

+    (Length(s) < n ==> Length(Take(s,n)) == Length(s)));

+axiom (forall s: Seq, n: int, j: int :: { Index(Take(s,n), j) }

+  0 <= j && j < n && j < Length(s) ==>

+    Index(Take(s,n), j) == Index(s, j));

+

+function Drop(s: Seq, howMany: int) returns (Seq);

+axiom (forall s: Seq, n: int :: { Length(Drop(s,n)) }

+  0 <= n ==>

+    (n <= Length(s) ==> Length(Drop(s,n)) == Length(s) - n) &&

+    (Length(s) < n ==> Length(Drop(s,n)) == 0));

+axiom (forall s: Seq, n: int, j: int :: { Index(Drop(s,n), j) }

+  0 <= n && 0 <= j && j < Length(s)-n ==>

+    Index(Drop(s,n), j) == Index(s, j+n));

+

+// ---------------------------------------------------------------

diff --git a/Test/dafny1/BinaryTree.dfy b/Test/dafny1/BinaryTree.dfy
new file mode 100644
index 00000000..fbda3ecb
--- /dev/null
+++ b/Test/dafny1/BinaryTree.dfy
@@ -0,0 +1,244 @@
+class IntSet {

+  ghost var Contents: set<int>;

+  ghost var Repr: set<object>;

+

+  var root: Node;

+

+  function Valid(): bool

+    reads this, Repr;

+  {

+    this in Repr &&

+    (root == null ==> Contents == {}) &&

+    (root != null ==>

+       root in Repr && root.Repr <= Repr && this !in root.Repr &&

+       root.Valid() &&

+       Contents == root.Contents)

+  }

+

+  method Init()

+    modifies this;

+    ensures Valid() && fresh(Repr - {this});

+    ensures Contents == {};

+  {

+    root := null;

+    Repr := {this};

+    Contents := {};

+  }

+

+  method Find(x: int) returns (present: bool)

+    requires Valid();

+    ensures present <==> x in Contents;

+  {

+    if (root == null) {

+      present := false;

+    } else {

+      call present := root.Find(x);

+    }

+  }

+

+  method Insert(x: int)

+    requires Valid();

+    modifies Repr;

+    ensures Valid() && fresh(Repr - old(Repr));

+    ensures Contents == old(Contents) + {x};

+  { 

+    call t := InsertHelper(x, root);

+    root := t;

+    Contents := root.Contents;

+    Repr := root.Repr + {this};

+  }

+

+  static method InsertHelper(x: int, n: Node) returns (m: Node)

+    requires n == null || n.Valid();

+    modifies n.Repr;

+    ensures m != null && m.Valid();

+    ensures n == null ==> fresh(m.Repr) && m.Contents == {x};

+    ensures n != null ==> m == n && n.Contents == old(n.Contents) + {x};

+    ensures n != null ==> fresh(n.Repr - old(n.Repr));

+    decreases if n == null then {} else n.Repr;

+  {

+    if (n == null) {

+      m := new Node;

+      call m.Init(x);

+    } else if (x == n.data) {

+      m := n;

+    } else {

+      if (x < n.data) {

+        assert n.right == null || n.right.Valid();

+        call t := InsertHelper(x, n.left);

+        n.left := t;

+        n.Repr := n.Repr + n.left.Repr;

+      } else {

+        assert n.left == null || n.left.Valid();

+        call t := InsertHelper(x, n.right);

+        n.right := t;

+        n.Repr := n.Repr + n.right.Repr;

+      }

+      n.Contents := n.Contents + {x};

+      m := n;

+    }

+  }

+

+  method Remove(x: int)

+    requires Valid();

+    modifies Repr;

+    ensures Valid() && fresh(Repr - old(Repr));

+    ensures Contents == old(Contents) - {x};

+  {

+    if (root != null) {

+      call newRoot := root.Remove(x);

+      root := newRoot;

+      if (root == null) {

+        Contents := {};

+        Repr := {this};

+      } else {

+        Contents := root.Contents;

+        Repr := root.Repr + {this};

+      }

+    }

+  }

+}

+

+class Node {

+  ghost var Contents: set<int>;

+  ghost var Repr: set<object>;

+

+  var data: int;

+  var left: Node;

+  var right: Node;

+

+  function Valid(): bool

+    reads this, Repr;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (left != null ==>

+      left in Repr &&

+      left.Repr <= Repr && this !in left.Repr &&

+      left.Valid() &&

+      (forall y :: y in left.Contents ==> y < data)) &&

+    (right != null ==>

+      right in Repr &&

+      right.Repr <= Repr && this !in right.Repr &&

+      right.Valid() &&

+      (forall y :: y in right.Contents ==> data < y)) &&

+    (left == null && right == null ==>

+      Contents == {data}) &&

+    (left != null && right == null ==>

+      Contents == left.Contents + {data}) &&

+    (left == null && right != null ==>

+      Contents == {data} + right.Contents) &&

+    (left != null && right != null ==>

+      left.Repr !! right.Repr &&

+      Contents == left.Contents + {data} + right.Contents)

+  }

+

+  method Init(x: int)

+    modifies this;

+    ensures Valid() && fresh(Repr - {this});

+    ensures Contents == {x};

+  {

+    data := x;

+    left := null;

+    right := null;

+    Contents := {x};

+    Repr := {this};

+  }

+

+  method Find(x: int) returns (present: bool)

+    requires Valid();

+    ensures present <==> x in Contents;

+    decreases Repr;

+  {

+    if (x == data) {

+      present := true;

+    } else if (left != null && x < data) {

+      call present := left.Find(x);

+    } else if (right != null && data < x) {

+      call present := right.Find(x);

+    } else {

+      present := false;

+    }

+  }

+

+  method Remove(x: int) returns (node: Node)

+    requires Valid();

+    modifies Repr;

+    ensures fresh(Repr - old(Repr));

+    ensures node != null ==> node.Valid();

+    ensures node == null ==> old(Contents) <= {x};

+    ensures node != null ==> node.Repr <= Repr && node.Contents == old(Contents) - {x};

+    decreases Repr;

+  {

+    node := this;

+    if (left != null && x < data) {

+      call t := left.Remove(x);

+      left := t;

+      Contents := Contents - {x};

+      if (left != null) { Repr := Repr + left.Repr; }

+    } else if (right != null && data < x) {

+      call t := right.Remove(x);

+      right := t;

+      Contents := Contents - {x};

+      if (right != null) { Repr := Repr + right.Repr; }

+    } else if (x == data) {

+      if (left == null && right == null) {

+        node := null;

+      } else if (left == null) {

+        node := right;

+      } else if (right == null) {

+        node := left;

+      } else {

+        // rotate

+        call min, r := right.RemoveMin();

+        data := min;  right := r;

+        Contents := Contents - {x};

+        if (right != null) { Repr := Repr + right.Repr; }

+      }

+    }

+  }

+

+  method RemoveMin() returns (min: int, node: Node)

+    requires Valid();

+    modifies Repr;

+    ensures fresh(Repr - old(Repr));

+    ensures node != null ==> node.Valid();

+    ensures node == null ==> old(Contents) == {min};

+    ensures node != null ==> node.Repr <= Repr && node.Contents == old(Contents) - {min};

+    ensures min in old(Contents) && (forall x :: x in old(Contents) ==> min <= x);

+    decreases Repr;

+  {

+    if (left == null) {

+      min := data;

+      node := right;

+    } else {

+      call min, t := left.RemoveMin();

+      left := t;

+      node := this;

+      Contents := Contents - {min};

+      if (left != null) { Repr := Repr + left.Repr; }

+    }

+  }

+}

+

+class Main {

+  method Client0(x: int)

+  {

+    var s := new IntSet;

+    call s.Init();

+

+    call s.Insert(12);

+    call s.Insert(24);

+    call present := s.Find(x);

+    assert present <==> x == 12 || x == 24;

+  }

+

+  method Client1(s: IntSet, x: int)

+    requires s != null && s.Valid();

+    modifies s.Repr;

+  {

+    call s.Insert(x);

+    call s.Insert(24);

+    assert old(s.Contents) - {x,24} == s.Contents - {x,24};

+  }

+}

diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy
new file mode 100644
index 00000000..fd267c71
--- /dev/null
+++ b/Test/dafny1/Celebrity.dfy
@@ -0,0 +1,95 @@
+// Celebrity example, inspired by the Rodin tutorial

+

+method Pick<T>(S: set<T>) returns (t: T);

+  requires S != {};

+  ensures t in S;

+

+static function Knows<Person>(a: Person, b: Person): bool;

+  requires a != b;  // forbid asking about the reflexive case

+

+static function IsCelebrity<Person>(c: Person, people: set<Person>): bool

+{

+  c in people &&

+  (forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p))

+}

+

+method FindCelebrity0<Person>(people: set<Person>, ghost c: Person) returns (r: Person)

+  requires (exists c :: IsCelebrity(c, people));

+  ensures r == c;

+{

+  var cc; assume cc == c;  // this line essentially converts ghost c to non-ghost cc

+  r := cc;

+}

+

+method FindCelebrity1<Person>(people: set<Person>, ghost c: Person) returns (r: Person)

+  requires IsCelebrity(c, people);

+  ensures r == c;

+{

+  var Q := people;

+  call x := Pick(Q);

+  while (Q != {x})

+    //invariant Q <= people;  // inv1 in Rodin's Celebrity_1, but it's not needed here

+    invariant IsCelebrity(c, Q);  // inv2

+    invariant x in Q;

+    decreases Q;

+  {

+    call y := Pick(Q - {x});

+    if (Knows(x, y)) {

+      Q := Q - {x};  // remove_1

+    } else {

+      Q := Q - {y};  assert x in Q;  // remove_2

+    }

+    call x := Pick(Q);

+  }

+  r := x;

+}

+

+method FindCelebrity2<Person>(people: set<Person>, ghost c: Person) returns (r: Person)

+  requires IsCelebrity(c, people);

+  ensures r == c;

+{

+  call b := Pick(people);

+  var R := people - {b};

+  while (R != {})

+    invariant R <= people;  // inv1

+    invariant b in people;  // inv2

+    invariant b !in R;  // inv3

+    invariant IsCelebrity(c, R + {b});  // my non-refinement way of saying inv4

+

+    decreases R;

+  {

+    call x := Pick(R);

+    if (Knows(x, b)) {

+      R := R - {x};

+    } else {

+      b := x;

+      R := R - {x};

+    }

+  }

+  r := b;

+}

+

+method FindCelebrity3(n: int, people: set<int>, ghost c: int) returns (r: int)

+  requires 0 < n;

+  requires (forall p :: p in people <==> 0 <= p && p < n);

+  // requires IsCelebrity(c, people);  // see next line:

+  requires c in people && (forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p));  // hack to work around bug in Dafny-to-Boogie translator

+  ensures r == c;

+{

+  r := 0;

+  var a := 1;

+  var b := 0;

+  while (a < n)

+    invariant a <= n;

+    invariant b < a;  // Celebrity_2/inv3 and Celebrity_3/inv2

+    invariant c == b || (a <= c && c < n);

+  {

+    if (Knows(a, b)) {

+      a := a + 1;

+    } else {

+      b := a;

+      a := a + 1;

+    }

+  }

+  r := b;

+}

diff --git a/Test/dafny1/ListContents.dfy b/Test/dafny1/ListContents.dfy
new file mode 100644
index 00000000..62636ce5
--- /dev/null
+++ b/Test/dafny1/ListContents.dfy
@@ -0,0 +1,93 @@
+class Node<T> {

+  var list: seq<T>;

+  var footprint: set<Node<T>>;

+

+  var data: T;

+  var next: Node<T>;

+

+  function Valid(): bool

+    reads this, footprint;

+  {

+    this in this.footprint && null !in this.footprint &&

+    (next == null ==> list == [data]) &&

+    (next != null ==>

+        next in footprint && next.footprint <= footprint &&

+        this !in next.footprint &&

+        list == [data] + next.list &&

+        next.Valid())

+  }

+

+  method Init(d: T)

+    modifies this;

+    ensures Valid() && fresh(footprint - {this});

+    ensures list == [d];

+  {

+    data := d;

+    next := null;

+    list := [d];

+    footprint := {this};

+  }

+

+  method SkipHead() returns (r: Node<T>)

+    requires Valid();

+    ensures r == null ==> |list| == 1;

+    ensures r != null ==> r.Valid() && r.footprint <= footprint;

+    ensures r != null ==> r.list == list[1..];

+  {

+    r := next;

+  }

+

+  method Prepend(d: T) returns (r: Node<T>)

+    requires Valid();

+    ensures r != null && r.Valid() && fresh(r.footprint - old(footprint));

+    ensures r.list == [d] + list;

+  {

+    r := new Node<T>;

+    r.data := d;

+    r.next := this;

+    r.footprint := {r} + this.footprint;

+    r.list := [r.data] + this.list;

+  }

+

+  method ReverseInPlace() returns (reverse: Node<T>)

+    requires Valid();

+    modifies footprint;

+    ensures reverse != null && reverse.Valid();

+    ensures fresh(reverse.footprint - old(footprint));

+    ensures |reverse.list| == |old(list)|;

+    ensures (forall i :: 0 <= i && i < |old(list)| ==> old(list)[i] == reverse.list[|old(list)|-1-i]);

+  {

+    var current := next;

+    reverse := this;

+    reverse.next := null;

+    reverse.footprint := {reverse};

+    reverse.list := [data];

+

+    while (current != null)

+      invariant reverse != null && reverse.Valid();

+      invariant reverse.footprint <= old(footprint);

+      invariant current == null ==> |old(list)| == |reverse.list|;

+      invariant current != null ==>

+        current.Valid() &&

+        current in old(footprint) && current.footprint <= old(footprint) &&

+        current.footprint !! reverse.footprint &&

+        |old(list)| == |reverse.list| + |current.list| &&

+        (forall i :: 0 <= i && i < |current.list| ==> current.list[i] == old(list)[|reverse.list|+i]);

+      invariant

+        (forall i :: 0 <= i && i < |reverse.list| ==> old(list)[i] == reverse.list[|reverse.list|-1-i]);

+      decreases if current != null then |current.list| else -1;

+    {

+      var nx := current.next;

+      assert nx != null ==> (forall i :: 0 <= i && i < |nx.list| ==> current.list[1+i] == nx.list[i]); // lemma

+

+      // ..., reverse, current, nx, ...

+      assert current.data == current.list[0]; // lemma

+      current.next := reverse;

+      current.footprint := {current} + reverse.footprint;

+      current.list := [current.data] + reverse.list;

+

+      reverse := current;

+      current := nx;

+    }

+  }

+}

diff --git a/Test/dafny1/ListCopy.dfy b/Test/dafny1/ListCopy.dfy
new file mode 100644
index 00000000..52f5cf76
--- /dev/null
+++ b/Test/dafny1/ListCopy.dfy
@@ -0,0 +1,55 @@
+class Node {

+  var nxt: Node;

+

+  method Init()

+    modifies this;

+    ensures nxt == null;

+  {

+    nxt := null;

+  }

+

+  method Copy(root: Node) returns (result: Node)

+  {

+    var existingRegion: set<Node>;

+    assume root == null || root in existingRegion;

+    assume (forall o: Node :: o != null && o in existingRegion && o.nxt != null ==> o.nxt in existingRegion);

+

+    var newRoot := null;

+    var oldListPtr := root;

+    var newRegion: set<Node> := {};

+

+    if (oldListPtr != null) {

+      newRoot := new Node;

+      call newRoot.Init();

+      newRegion := newRegion + {newRoot};

+      var prev := newRoot;

+

+      while (oldListPtr != null)

+        invariant newRoot in newRegion;

+        invariant (forall o: Node :: o in newRegion ==> o != null);

+        invariant (forall o: Node :: o in newRegion && o.nxt != null ==> o.nxt in newRegion);

+        invariant prev in newRegion;

+        invariant fresh(newRegion);

+        invariant newRegion !! existingRegion;

+        decreases *;  // omit loop termination check

+      {

+        var tmp := new Node;

+        call tmp.Init();

+

+        newRegion := newRegion + {tmp};

+        prev.nxt := tmp;

+

+        prev := tmp;

+        oldListPtr := oldListPtr.nxt;

+      }

+    } 

+    result := newRoot;

+    assert result == null || result in newRegion;

+    

+    // everything in newRegion is fresh

+    assert fresh(newRegion);

+

+    // newRegion # exisitingRegion

+    assert newRegion !! existingRegion; 

+  }

+}

diff --git a/Test/dafny1/ListReverse.dfy b/Test/dafny1/ListReverse.dfy
new file mode 100644
index 00000000..ef029b88
--- /dev/null
+++ b/Test/dafny1/ListReverse.dfy
@@ -0,0 +1,27 @@
+

+class Node {

+  var nxt: Node;

+

+  method ReverseInPlace(x: Node, r: set<Node>) returns (reverse: Node)

+    requires null !in r;

+    requires x == null || x in r;

+    requires (forall y :: y in r ==> y.nxt == null || y.nxt in r);  // region closure

+    modifies r;

+    ensures reverse == null || reverse in r;

+    ensures (forall y :: y in r ==> y.nxt == null || y.nxt in r);  // region closure

+  {

+    var current := x;

+    reverse := null;

+    while (current != null)

+      invariant current == null || current in r;

+      invariant reverse == null || reverse in r;

+      invariant (forall y :: y in r ==> y.nxt == null || y.nxt in r);  // region closure

+      decreases *;  // omit loop termination check

+    {

+      var tmp := current.nxt;

+      current.nxt := reverse;

+      reverse := current;

+      current := tmp;

+    }

+  }

+}

diff --git a/Test/dafny1/Queue.dfy b/Test/dafny1/Queue.dfy
new file mode 100644
index 00000000..42b7dd64
--- /dev/null
+++ b/Test/dafny1/Queue.dfy
@@ -0,0 +1,202 @@
+// Queue.dfy

+// Dafny version of Queue.bpl

+// Rustan Leino, 2008

+

+class Queue<T> {

+  var head: Node<T>;

+  var tail: Node<T>;

+

+  ghost var contents: seq<T>;

+  ghost var footprint: set<object>;

+  ghost var spine: set<Node<T>>;

+

+  function Valid(): bool

+    reads this, footprint;

+  {

+    this in footprint && spine <= footprint &&

+    head != null && head in spine &&

+    tail != null && tail in spine &&

+    tail.next == null &&

+    (forall n ::

+      n in spine ==>

+        n != null && n.footprint <= footprint && this !in n.footprint &&

+        n.Valid() &&

+        (n.next == null ==> n == tail)) &&

+    (forall n ::

+      n in spine ==>

+        n.next != null ==> n.next in spine) &&

+    contents == head.tailContents

+  }

+

+  method Init()

+    modifies this;

+    ensures Valid() && fresh(footprint - {this});

+    ensures |contents| == 0;

+  {

+    var n := new Node<T>;

+    call n.Init();

+    head := n;

+    tail := n;

+    contents := n.tailContents;

+    footprint := {this} + n.footprint;

+    spine := {n};

+  }

+

+  method Rotate()

+    requires Valid();

+    requires 0 < |contents|;

+    modifies footprint;

+    ensures Valid() && fresh(footprint - old(footprint));

+    ensures contents == old(contents)[1..] + old(contents)[..1];

+  {

+    call t := Front();

+    call Dequeue();

+    call Enqueue(t);

+  }

+

+  method RotateAny()

+    requires Valid();

+    requires 0 < |contents|;

+    modifies footprint;

+    ensures Valid() && fresh(footprint - old(footprint));

+    ensures |contents| == |old(contents)|;

+    ensures (exists i :: 0 <= i && i <= |contents| &&

+              contents == old(contents)[i..] + old(contents)[..i]);

+  {

+    call t := Front();

+    call Dequeue();

+    call Enqueue(t);

+  }

+

+  method IsEmpty() returns (isEmpty: bool)

+    requires Valid();

+    ensures isEmpty <==> |contents| == 0;

+  {

+    isEmpty := head == tail;

+  }

+

+  method Enqueue(t: T)

+    requires Valid();

+    modifies footprint;

+    ensures Valid() && fresh(footprint - old(footprint));

+    ensures contents == old(contents) + [t];

+  {

+    var n := new Node<T>;

+    call n.Init();  n.data := t;

+    tail.next := n;

+    tail := n;

+

+    foreach (m in spine) {

+      m.tailContents := m.tailContents + [t];

+    }

+    contents := head.tailContents;

+

+    foreach (m in spine) {

+      m.footprint := m.footprint + n.footprint;

+    }

+    footprint := footprint + n.footprint;

+

+    spine := spine + {n};

+  }

+

+  method Front() returns (t: T)

+    requires Valid();

+    requires 0 < |contents|;

+    ensures t == contents[0];

+  {

+    t := head.next.data;

+  }

+

+  method Dequeue()

+    requires Valid();

+    requires 0 < |contents|;

+    modifies footprint;

+    ensures Valid() && fresh(footprint - old(footprint));

+    ensures contents == old(contents)[1..];

+  {

+    var n := head.next;

+    head := n;

+    contents := n.tailContents;

+  }

+}

+

+class Node<T> {

+  var data: T;

+  var next: Node<T>;

+

+  ghost var tailContents: seq<T>;

+  ghost var footprint: set<object>;

+

+  function Valid(): bool

+    reads this, footprint;

+  {

+    this in footprint &&

+    (next != null ==> next in footprint && next.footprint <= footprint) &&

+    (next == null ==> tailContents == []) &&

+    (next != null ==> tailContents == [next.data] + next.tailContents)

+  }

+

+  method Init()

+    modifies this;

+    ensures Valid() && fresh(footprint - {this});

+    ensures next == null;

+  {

+    next := null;

+    tailContents := [];

+    footprint := {this};

+  }

+}

+

+class Main<U> {

+  method A<T>(t: T, u: T, v: T)

+  {

+    var q0 := new Queue<T>;

+    call q0.Init();

+    var q1 := new Queue<T>;

+    call q1.Init();

+

+    call q0.Enqueue(t);

+    call q0.Enqueue(u);

+

+    call q1.Enqueue(v);

+

+    assert |q0.contents| == 2;

+

+    call w := q0.Front();

+    assert w == t;

+    call q0.Dequeue();

+

+    call w := q0.Front();

+    assert w == u;

+

+    assert |q0.contents| == 1;

+    assert |q1.contents| == 1;

+  }

+

+  method Main2(t: U, u: U, v: U, q0: Queue<U>, q1: Queue<U>)

+    requires q0 != null && q0.Valid();

+    requires q1 != null && q1.Valid();

+    requires q0.footprint !! q1.footprint;

+    requires |q0.contents| == 0;

+    modifies q0.footprint, q1.footprint;

+    ensures fresh(q0.footprint - old(q0.footprint));

+    ensures fresh(q1.footprint - old(q1.footprint));

+  {

+    call q0.Enqueue(t);

+    call q0.Enqueue(u);

+

+    call q1.Enqueue(v);

+

+    assert |q0.contents| == 2;

+

+    call w := q0.Front();

+    assert w == t;

+    call q0.Dequeue();

+

+    call w := q0.Front();

+    assert w == u;

+

+    assert |q0.contents| == 1;

+    assert |q1.contents| == old(|q1.contents|) + 1;

+  }

+}

diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy
new file mode 100644
index 00000000..a46e83a3
--- /dev/null
+++ b/Test/dafny1/SchorrWaite.dfy
@@ -0,0 +1,272 @@
+// Rustan Leino

+// 7 November 2008

+// Schorr-Waite and other marking algorithms, written and verified in Dafny.

+// Copyright (c) 2008, Microsoft.

+

+class Node {

+  var children: seq<Node>;

+  var marked: bool;

+  var childrenVisited: int;

+  ghost var pathFromRoot: Path;

+}

+

+class Main {

+  method RecursiveMark(root: Node, ghost S: set<Node>)

+    requires root in S;

+    // S is closed under 'children':

+    requires (forall n :: n in S ==> n != null &&

+                (forall ch :: ch in n.children ==> ch == null || ch in S));

+    requires (forall n :: n in S ==> ! n.marked && n.childrenVisited == 0);

+    modifies S;

+    ensures root.marked;

+    // nodes reachable from 'root' are marked:

+    ensures (forall n :: n in S && n.marked ==>

+                (forall ch :: ch in n.children && ch != null ==> ch.marked));

+    ensures (forall n :: n in S ==>

+                n.childrenVisited == old(n.childrenVisited) &&

+                n.children == old(n.children));

+  {

+    call RecursiveMarkWorker(root, S, {});

+  }

+

+  method RecursiveMarkWorker(root: Node, ghost S: set<Node>, ghost stackNodes: set<Node>)

+    requires root != null && root in S;

+    requires (forall n :: n in S ==> n != null &&

+                (forall ch :: ch in n.children ==> ch == null || ch in S));

+    requires (forall n :: n in S && n.marked ==>

+                n in stackNodes ||

+                (forall ch :: ch in n.children && ch != null ==> ch.marked));

+    requires (forall n :: n in stackNodes ==> n != null && n.marked);

+    modifies S;

+    ensures root.marked;

+    // nodes reachable from 'root' are marked:

+    ensures (forall n :: n in S && n.marked ==>

+                n in stackNodes ||

+                (forall ch :: ch in n.children && ch != null ==> ch.marked));

+    ensures (forall n: Node :: n in S && old(n.marked) ==> n.marked);

+    ensures (forall n :: n in S ==>

+                n.childrenVisited == old(n.childrenVisited) &&

+                n.children == old(n.children));

+    decreases S - stackNodes;

+  {

+    if (! root.marked) {

+      root.marked := true;

+      var i := 0;

+      while (i < |root.children|)

+        invariant root.marked && i <= |root.children|;

+        invariant (forall n :: n in S && n.marked ==>

+                n == root ||

+                n in stackNodes ||

+                (forall ch :: ch in n.children && ch != null ==> ch.marked));

+        invariant (forall j :: 0 <= j && j < i ==>

+                    root.children[j] == null || root.children[j].marked);

+        invariant (forall n: Node :: n in S && old(n.marked) ==> n.marked);

+        invariant (forall n :: n in S ==>

+                n.childrenVisited == old(n.childrenVisited) &&

+                n.children == old(n.children));

+        decreases |root.children| - i;

+      {

+        var c := root.children[i];

+        if (c != null) {

+          ghost var D := S - stackNodes;  assert root in D;

+          call RecursiveMarkWorker(c, S, stackNodes + {root});

+        }

+        i := i + 1;

+      }

+    }

+  }

+

+  // ---------------------------------------------------------------------------------

+

+  method IterativeMark(root: Node, ghost S: set<Node>)

+    requires root in S;

+    // S is closed under 'children':

+    requires (forall n :: n in S ==> n != null &&

+                (forall ch :: ch in n.children ==> ch == null || ch in S));

+    requires (forall n :: n in S ==> ! n.marked && n.childrenVisited == 0);

+    modifies S;

+    ensures root.marked;

+    // nodes reachable from 'root' are marked:

+    ensures (forall n :: n in S && n.marked ==>

+                (forall ch :: ch in n.children && ch != null ==> ch.marked));

+    ensures (forall n :: n in S ==>

+                n.childrenVisited == old(n.childrenVisited) &&

+                n.children == old(n.children));

+  {

+    var t := root;

+    t.marked := true;

+    var stackNodes := [];

+    ghost var unmarkedNodes := S - {t};

+    while (true)

+      invariant root.marked && t in S && t !in stackNodes;

+      // stackNodes has no duplicates:

+      invariant (forall i, j :: 0 <= i && i < j && j < |stackNodes| ==>

+                  stackNodes[i] != stackNodes[j]);

+      invariant (forall n :: n in stackNodes ==> n in S);

+      invariant (forall n :: n in stackNodes || n == t ==>

+                  n.marked &&

+                  0 <= n.childrenVisited && n.childrenVisited <= |n.children| &&

+                  (forall j :: 0 <= j && j < n.childrenVisited ==>

+                    n.children[j] == null || n.children[j].marked));

+      invariant (forall n :: n in stackNodes ==> n.childrenVisited < |n.children|);

+      // nodes on the stack are linked:

+      invariant (forall j :: 0 <= j && j+1 < |stackNodes| ==>

+                  stackNodes[j].children[stackNodes[j].childrenVisited] == stackNodes[j+1]);

+      invariant 0 < |stackNodes| ==>

+        stackNodes[|stackNodes|-1].children[stackNodes[|stackNodes|-1].childrenVisited] == t;

+      invariant (forall n :: n in S && n.marked && n !in stackNodes && n != t ==>

+                  (forall ch :: ch in n.children && ch != null ==> ch.marked));

+      invariant (forall n :: n in S && n !in stackNodes && n != t ==>

+                n.childrenVisited == old(n.childrenVisited));

+      invariant (forall n: Node :: n in S ==> n.children == old(n.children));

+      invariant (forall n :: n in S && !n.marked ==> n in unmarkedNodes);

+      decreases unmarkedNodes, stackNodes, |t.children| - t.childrenVisited;

+    {

+      if (t.childrenVisited == |t.children|) {

+        // pop

+        t.childrenVisited := 0;

+        if (|stackNodes| == 0) {

+          return;

+        }

+        t := stackNodes[|stackNodes| - 1];

+        stackNodes := stackNodes[..|stackNodes| - 1];

+        t.childrenVisited := t.childrenVisited + 1;

+      } else if (t.children[t.childrenVisited] == null || t.children[t.childrenVisited].marked) {

+        // just advance to next child

+        t.childrenVisited := t.childrenVisited + 1;

+      } else {

+        // push

+        stackNodes := stackNodes + [t];

+        t := t.children[t.childrenVisited];

+        t.marked := true;

+        unmarkedNodes := unmarkedNodes - {t};

+      }

+    }

+  }

+

+  // ---------------------------------------------------------------------------------

+

+  function Reachable(from: Node, to: Node, S: set<Node>): bool

+    requires null !in S;

+    reads S;

+  {

+    (exists via: Path :: ReachableVia(from, via, to, S))

+  }

+

+  function ReachableVia(from: Node, via: Path, to: Node, S: set<Node>): bool

+    requires null !in S;

+    reads S;

+    decreases via;

+  {

+    match via

+    case Empty => from == to

+    case Extend(prefix, n) => n in S && to in n.children && ReachableVia(from, prefix, n, S)

+  }

+

+  method SchorrWaite(root: Node, ghost S: set<Node>)

+    requires root in S;

+    // S is closed under 'children':

+    requires (forall n :: n in S ==> n != null &&

+                (forall ch :: ch in n.children ==> ch == null || ch in S));

+    // the graph starts off with nothing marked and nothing being indicated as currently being visited:

+    requires (forall n :: n in S ==> ! n.marked && n.childrenVisited == 0);

+    modifies S;

+    // nodes reachable from 'root' are marked:

+    ensures root.marked;

+    ensures (forall n :: n in S && n.marked ==>

+                (forall ch :: ch in n.children && ch != null ==> ch.marked));

+    // every marked node was reachable from 'root' in the pre-state:

+    ensures (forall n :: n in S && n.marked ==> old(Reachable(root, n, S)));

+    // the structure of the graph has not changed:

+    ensures (forall n :: n in S ==>

+                n.childrenVisited == old(n.childrenVisited) &&

+                n.children == old(n.children));

+  {

+    var t := root;

+    var p: Node := null;  // parent of t in original graph

+    ghost var path := #Path.Empty;

+    t.marked := true;

+    t.pathFromRoot := path;

+    ghost var stackNodes := [];

+    ghost var unmarkedNodes := S - {t};

+    while (true)

+      invariant root.marked && t != null && t in S && t !in stackNodes;

+      invariant |stackNodes| == 0 <==> p == null;

+      invariant 0 < |stackNodes| ==> p == stackNodes[|stackNodes|-1];

+      // stackNodes has no duplicates:

+      invariant (forall i, j :: 0 <= i && i < j && j < |stackNodes| ==>

+                  stackNodes[i] != stackNodes[j]);

+      invariant (forall n :: n in stackNodes ==> n in S);

+      invariant (forall n :: n in stackNodes || n == t ==>

+                  n.marked &&

+                  0 <= n.childrenVisited && n.childrenVisited <= |n.children| &&

+                  (forall j :: 0 <= j && j < n.childrenVisited ==>

+                    n.children[j] == null || n.children[j].marked));

+      invariant (forall n :: n in stackNodes ==> n.childrenVisited < |n.children|);

+      invariant (forall n :: n in S && n.marked && n !in stackNodes && n != t ==>

+                  (forall ch :: ch in n.children && ch != null ==> ch.marked));

+      invariant (forall n :: n in S && n !in stackNodes && n != t ==>

+                n.childrenVisited == old(n.childrenVisited));

+      invariant (forall n :: n in S ==> n in stackNodes || n.children == old(n.children));

+      invariant (forall n :: n in stackNodes ==>

+                  |n.children| == old(|n.children|) &&

+                  (forall j :: 0 <= j && j < |n.children| ==>

+                    j == n.childrenVisited || n.children[j] == old(n.children[j])));

+      // every marked node is reachable:

+      invariant old(ReachableVia(root, path, t, S));

+      invariant (forall n, pth :: n in S && n.marked && pth == n.pathFromRoot ==>

+                  old(ReachableVia(root, pth, n, S)));

+      invariant (forall n :: n in S && n.marked ==> old(Reachable(root, n, S)));

+      // the current values of m.children[m.childrenVisited] for m's on the stack:

+      invariant 0 < |stackNodes| ==> stackNodes[0].children[stackNodes[0].childrenVisited] == null;

+      invariant (forall k :: 0 < k && k < |stackNodes| ==>

+                  stackNodes[k].children[stackNodes[k].childrenVisited] == stackNodes[k-1]);

+      // the original values of m.children[m.childrenVisited] for m's on the stack:

+      invariant (forall k :: 0 <= k && k+1 < |stackNodes| ==>

+                  old(stackNodes[k].children)[stackNodes[k].childrenVisited] == stackNodes[k+1]);

+      invariant 0 < |stackNodes| ==>

+        old(stackNodes[|stackNodes|-1].children)[stackNodes[|stackNodes|-1].childrenVisited] == t;

+      invariant (forall n :: n in S && !n.marked ==> n in unmarkedNodes);

+      decreases unmarkedNodes, stackNodes, |t.children| - t.childrenVisited;

+    {

+      if (t.childrenVisited == |t.children|) {

+        // pop

+        t.childrenVisited := 0;

+        if (p == null) {

+          return;

+        }

+        var oldP := p.children[p.childrenVisited];

+        // p.children[p.childrenVisited] := t;

+        p.children := p.children[..p.childrenVisited] + [t] + p.children[p.childrenVisited + 1..];

+        t := p;

+        p := oldP;

+        stackNodes := stackNodes[..|stackNodes| - 1];

+        t.childrenVisited := t.childrenVisited + 1;

+        path := t.pathFromRoot;

+

+      } else if (t.children[t.childrenVisited] == null || t.children[t.childrenVisited].marked) {

+        // just advance to next child

+        t.childrenVisited := t.childrenVisited + 1;

+

+      } else {

+        // push

+

+        var newT := t.children[t.childrenVisited];

+        // t.children[t.childrenVisited] := p;

+        t.children := t.children[..t.childrenVisited] + [p] + t.children[t.childrenVisited + 1..];

+        p := t;

+        stackNodes := stackNodes + [t];

+        path := #Path.Extend(path, t);

+        t := newT;

+        t.marked := true;

+        t.pathFromRoot := path;

+        unmarkedNodes := unmarkedNodes - {t};

+      }

+    }

+  }

+}

+

+datatype Path {

+  Empty;

+  Extend(Path, Node);

+}

diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy
new file mode 100644
index 00000000..72415fea
--- /dev/null
+++ b/Test/dafny1/Substitution.dfy
@@ -0,0 +1,120 @@
+datatype List {

+  Nil;

+  Cons(Expr, List);

+}

+

+datatype Expr {

+  Const(int);

+  Var(int);

+  Nary(int, List);

+}

+

+static function Subst(e: Expr, v: int, val: int): Expr

+  decreases e;

+{

+  match e

+  case Const(c) => e

+  case Var(x) => if x == v then #Expr.Const(val) else e

+  case Nary(op, args) => #Expr.Nary(op, SubstList(args, v, val))

+}

+

+static function SubstList(l: List, v: int, val: int): List

+  decreases l;

+{

+  match l

+  case Nil => l

+  case Cons(e, tail) => #List.Cons(Subst(e, v, val), SubstList(tail, v, val))

+}

+

+static ghost method Theorem(e: Expr, v: int, val: int)

+  ensures Subst(Subst(e, v, val), v, val) == Subst(e, v, val);

+  decreases e;

+{

+  match e {

+    case Const(c) =>

+    case Var(x) =>

+    case Nary(op, args) =>

+      call Lemma(args, v, val);

+  }

+}

+

+static ghost method Lemma(l: List, v: int, val: int)

+  ensures SubstList(SubstList(l, v, val), v, val) == SubstList(l, v, val);

+  decreases l;

+{

+  match l {

+    case Nil =>

+    case Cons(e, tail) =>

+      call Theorem(e, v, val);

+      call Lemma(tail, v, val);

+  }

+}

+

+// -------------------------------

+

+datatype Expression {

+  Const(int);

+  Var(int);

+  Nary(int, seq<Expression>);

+}

+

+static function Substitute(e: Expression, v: int, val: int): Expression

+  decreases e, true;

+{

+  match e

+  case Const(c) => e

+  case Var(x) => if x == v then #Expression.Const(val) else e

+  case Nary(op, args) => #Expression.Nary(op, SubstSeq(e, args, v, val))

+}

+

+static function SubstSeq(/*ghost*/ parent: Expression,

+                         q: seq<Expression>, v: int, val: int): seq<Expression>

+  requires (forall a :: a in q ==> a < parent);

+  decreases parent, false, q;

+{

+  if q == [] then [] else

+  SubstSeq(parent, q[..|q|-1], v, val) + [Substitute(q[|q|-1], v, val)]

+}

+

+static ghost method TheoremSeq(e: Expression, v: int, val: int)

+  ensures Substitute(Substitute(e, v, val), v, val) == Substitute(e, v, val);

+  decreases e, true;

+{

+  match e {

+    case Const(c) =>

+    case Var(x) =>

+    case Nary(op, args) =>

+      ghost var seArgs := SubstSeq(e, args, v, val);

+      call LemmaSeq(e, args, v, val);

+

+      ghost var se := Substitute(e, v, val);

+      ghost var seArgs2 := SubstSeq(se, seArgs, v, val);

+      call LemmaSeq(se, seArgs, v, val);

+

+      var N := |args|;

+      var j := 0;

+      while (j < N)

+        invariant j <= N;

+        invariant (forall k :: 0 <= k && k < j ==> seArgs2[k] == seArgs[k]);

+        decreases N - j;

+      {

+        call TheoremSeq(args[j], v, val);

+        j := j + 1;

+      }

+      assert seArgs == seArgs2;

+  }

+}

+

+static ghost method LemmaSeq(ghost parent: Expression, ghost q: seq<Expression>,

+                                    v: int, val: int)

+  requires (forall a :: a in q ==> a < parent);

+  ensures |SubstSeq(parent, q, v, val)| == |q|;

+  ensures (forall k :: 0 <= k && k < |q| ==>

+            SubstSeq(parent, q, v, val)[k] == Substitute(q[k], v, val));

+  decreases q;

+{

+  if (q == []) {

+  } else {

+    call LemmaSeq(parent, q[..|q|-1], v, val);

+  }

+}

diff --git a/Test/dafny1/SumOfCubes.dfy b/Test/dafny1/SumOfCubes.dfy
new file mode 100644
index 00000000..b4fab490
--- /dev/null
+++ b/Test/dafny1/SumOfCubes.dfy
@@ -0,0 +1,106 @@
+class SumOfCubes {

+  static function SumEmUp(n: int, m: int): int

+    requires 0 <= n && n <= m;

+    decreases m - n;

+  {

+    if m == n then 0 else n*n*n + SumEmUp(n+1, m)

+  }

+

+  static method Socu(n: int, m: int) returns (r: int)

+    requires 0 <= n && n <= m;

+    ensures r == SumEmUp(n, m);

+  {

+    call a := SocuFromZero(m);

+    call b := SocuFromZero(n);

+    r := a - b;

+    call Lemma0(n, m);

+  }

+

+  static method SocuFromZero(k: int) returns (r: int)

+    requires 0 <= k;

+    ensures r == SumEmUp(0, k);

+  {

+    call g := Gauss(k);

+    r := g * g;

+    call Lemma1(k);

+  }

+

+  ghost static method Lemma0(n: int, m: int)

+    requires 0 <= n && n <= m;

+    ensures SumEmUp(n, m) == SumEmUp(0, m) - SumEmUp(0, n);

+  {

+    var k := n;

+    while (k < m) 

+      invariant n <= k && k <= m;

+      invariant SumEmDown(0, n) + SumEmDown(n, k) == SumEmDown(0, k);

+    {

+      k := k + 1;

+    }

+    call Lemma3(0, n);

+    call Lemma3(n, k);

+    call Lemma3(0, k);

+  }

+

+  static function GSum(k: int): int

+    requires 0 <= k;

+    decreases k;

+  {

+    if k == 0 then 0 else GSum(k-1) + k-1

+  }

+

+  static method Gauss(k: int) returns (r: int)

+    requires 0 <= k;

+    ensures r == GSum(k);

+  {

+    r := k * (k - 1) / 2;

+    call Lemma2(k);

+  }

+

+  ghost static method Lemma1(k: int)

+    requires 0 <= k;

+    ensures SumEmUp(0, k) == GSum(k) * GSum(k);

+  {

+    var i := 0;

+    while (i < k)

+      invariant i <= k;

+      invariant SumEmDown(0, i) == GSum(i) * GSum(i);

+    {

+      call Lemma2(i);

+      i := i + 1;

+    }

+    call Lemma3(0, k);

+  }

+

+  ghost static method Lemma2(k: int)

+    requires 0 <= k;

+    ensures 2 * GSum(k) == k * (k - 1);

+  {

+    var i := 0;

+    while (i < k)

+      invariant i <= k;

+      invariant 2 * GSum(i) == i * (i - 1);

+    {

+      i := i + 1;

+    }

+  }

+

+  static function SumEmDown(n: int, m: int): int

+    requires 0 <= n && n <= m;

+    decreases m;

+  {

+    if m == n then 0 else SumEmDown(n, m-1) + (m-1)*(m-1)*(m-1)

+  }

+

+  ghost static method Lemma3(n: int, m: int)

+    requires 0 <= n && n <= m;

+    ensures SumEmUp(n, m) == SumEmDown(n, m);

+  {

+    var k := n;

+    while (k < m)

+      invariant n <= k && k <= m;

+      invariant SumEmUp(n, m) == SumEmDown(n, k) + SumEmUp(k, m);

+    {

+      k := k + 1;

+    }

+  }

+}

diff --git a/Test/dafny1/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy
new file mode 100644
index 00000000..6b63bfec
--- /dev/null
+++ b/Test/dafny1/TerminationDemos.dfy
@@ -0,0 +1,80 @@
+class Example {

+  method M(n: int)

+  {

+    var i := 0;

+    while (i < n)

+      decreases n - i;

+    {

+      i := i + 1;

+    }

+  }

+}

+

+// -----------------------------------

+

+class Fibonacci {

+  function Fib(n: int): int

+    decreases n;

+  {

+    if n < 2 then n else Fib(n-2) + Fib(n-1)

+  }

+}

+

+// -----------------------------------

+

+class Ackermann {

+  function F(m: int, n: int): int

+    decreases m, n;

+  {

+    if m <= 0 then

+      n + 1

+    else if n <= 0 then

+      F(m - 1, 1)

+    else

+      F(m - 1, F(m, n - 1))

+  }

+}

+

+// -----------------------------------

+

+class List {

+  var data: int;

+  var next: List;

+  ghost var ListNodes: set<List>;

+  function IsAcyclic(): bool

+    reads *;

+    decreases ListNodes;

+  {

+    this in ListNodes &&

+    (next != null ==>

+      next.ListNodes <= ListNodes && this !in next.ListNodes &&

+      next.IsAcyclic())

+  }

+

+  method Singleton(x: int) returns (list: List)

+    ensures list != null && list.IsAcyclic();

+  {

+    list := new List;

+    list.data := x;

+    list.next := null;

+    list.ListNodes := {list};

+  }

+

+  method Prepend(x: int, tail: List) returns (list: List)

+    requires tail == null || tail.IsAcyclic();

+    ensures list != null && list.IsAcyclic();

+  {

+    list := new List;

+    list.data := x;

+    list.next := tail;

+    list.ListNodes := if tail == null then {list} else {list} + tail.ListNodes;

+  }

+

+  function Sum(): int

+    requires IsAcyclic();

+    reads *;

+    decreases ListNodes;

+  {

+    if next == null then data else data + next.Sum()

+  }

+}

diff --git a/Test/dafny1/TreeDatatype.dfy b/Test/dafny1/TreeDatatype.dfy
new file mode 100644
index 00000000..58124171
--- /dev/null
+++ b/Test/dafny1/TreeDatatype.dfy
@@ -0,0 +1,72 @@
+// ------------------ generic list, non-generic tree

+

+datatype List<T> {

+  Nil;

+  Cons(T, List<T>);

+}

+

+datatype Tree {

+  Node(int, List<Tree>);

+}

+

+static function Inc(t: Tree): Tree

+  decreases t;

+{

+  match t

+  case Node(n, children) => #Tree.Node(n+1, ForestInc(children))

+}

+

+static function ForestInc(forest: List<Tree>): List<Tree>

+  decreases forest;

+{

+  match forest

+  case Nil => forest

+  case Cons(tree, tail) => #List.Cons(Inc(tree), ForestInc(tail))

+}

+

+// ------------------ generic list, generic tree (but GInc defined only for GTree<int>

+

+datatype GTree<T> {

+  Node(T, List<GTree<T>>);

+}

+

+static function GInc(t: GTree<int>): GTree<int>

+  decreases t;

+{

+  match t

+  case Node(n, children) => #GTree.Node(n+1, GForestInc(children))

+}

+

+static function GForestInc(forest: List<GTree<int>>): List<GTree<int>>

+  decreases forest;

+{

+  match forest

+  case Nil => forest

+  case Cons(tree, tail) => #List.Cons(GInc(tree), GForestInc(tail))

+}

+

+// ------------------ non-generic structures

+

+datatype TreeList {

+  Nil;

+  Cons(OneTree, TreeList);

+}

+

+datatype OneTree {

+  Node(int, TreeList);

+}

+

+static function XInc(t: OneTree): OneTree

+  decreases t;

+{

+  match t

+  case Node(n, children) => #OneTree.Node(n+1, XForestInc(children))

+}

+

+static function XForestInc(forest: TreeList): TreeList

+  decreases forest;

+{

+  match forest

+  case Nil => forest

+  case Cons(tree, tail) => #TreeList.Cons(XInc(tree), XForestInc(tail))

+}

diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy
new file mode 100644
index 00000000..61e86836
--- /dev/null
+++ b/Test/dafny1/UltraFilter.dfy
@@ -0,0 +1,108 @@
+// ultra filter

+

+class UltraFilter<G> {

+  static function IsFilter(f: set<set<G>>, S: set<G>): bool

+  {

+    (forall A, B :: A in f && A <= B ==> B in f) &&

+    (forall C, D :: C in f && D in f ==> C * D in f) &&

+    S in f &&

+    {} !in f

+  }

+

+  static function IsUltraFilter(f: set<set<G>>, S: set<G>): bool

+  {

+    IsFilter(f, S) &&

+    (forall g :: IsFilter(g, S) && f <= g ==> f == g)

+  }

+

+  method Theorem(f: set<set<G>>, S: set<G>, M: set<G>, N: set<G>)

+    requires IsUltraFilter(f, S);

+    requires M + N in f;

+    ensures M in f || N in f;

+  {

+    if (M !in f) {

+      // instantiate 'g' with the following 'h'

+      call h := H(f, S, M);

+      call Lemma_HIsFilter(h, f, S, M);

+      call Lemma_FHOrdering0(h, f, S, M);

+    }

+  }

+

+  // Dafny currently does not have a set comprehension expression, so this method stub will have to do

+  method H(f: set<set<G>>, S: set<G>, M: set<G>) returns (h: set<set<G>>);

+    ensures (forall X :: X in h <==> M + X in f);

+

+  method Lemma_HIsFilter(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)

+    requires IsFilter(f, S);

+    requires (forall X :: X in h <==> M + X in f);

+    requires M !in f;

+    ensures IsFilter(h, S);

+  {

+    // call Lemma_H0(h, f, S, M, *, *);

+    assume (forall A, B :: A in h && A <= B ==> B in h);

+

+    // call Lemma_H1(h, f, S, M, *, *);

+    assume (forall C, D :: C in h && D in h ==> C * D in h);

+

+    call Lemma_H2(h, f, S, M);

+

+    call Lemma_H3(h, f, S, M);

+  }

+

+  method Lemma_H0(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>, A: set<G>, B: set<G>)

+    requires IsFilter(f, S);

+    requires (forall X :: X in h <==> M + X in f);

+    requires A in h && A <= B;

+    ensures B in h;

+  {

+    assert M + A <= M + B;

+  }

+

+  method Lemma_H1(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>, C: set<G>, D: set<G>)

+    requires IsFilter(f, S);

+    requires (forall X :: X in h <==> M + X in f);

+    requires C in h && D in h;

+    ensures C * D in h;

+  {

+    assert (M + C) * (M + D) == M + (C * D);

+  }

+

+  method Lemma_H2(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)

+    requires IsFilter(f, S);

+    requires (forall X :: X in h <==> M + X in f);

+    ensures S in h;

+  {

+    // S is intended to stand for the universal set, but this is the only place where that plays a role

+    assume M <= S;

+

+    assert M + S == S;

+  }

+

+  method Lemma_H3(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)

+    requires IsFilter(f, S);

+    requires (forall X :: X in h <==> M + X in f);

+    requires M !in f;

+    ensures {} !in h;

+  {

+    assert M + {} == M;

+  }

+

+  method Lemma_FHOrdering0(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)

+    requires IsFilter(f, S);

+    requires (forall X :: X in h <==> M + X in f);

+    requires IsFilter(h, S);

+    ensures f <= h;

+  {

+    // call Lemma_FHOrdering1(h, f, S, M, *);

+    assume (forall Y :: Y in f ==> Y in h);

+    assume f <= h;  // hickup in boxing

+  }

+

+  method Lemma_FHOrdering1(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>, Y: set<G>)

+    requires IsFilter(f, S);

+    requires (forall X :: X in h <==> M + X in f);

+    ensures Y in f ==> Y in h;

+  {

+    assert Y <= M + Y;

+  }

+}

diff --git a/Test/dafny1/UnboundedStack.dfy b/Test/dafny1/UnboundedStack.dfy
new file mode 100644
index 00000000..4c3b095a
--- /dev/null
+++ b/Test/dafny1/UnboundedStack.dfy
@@ -0,0 +1,98 @@
+class UnboundedStack<T> {

+  ghost var representation: set<object>;

+  ghost var content: seq<T>;

+  var top: Node<T>;

+

+  function IsUnboundedStack(): bool

+    reads this, representation;

+  {

+    this in representation &&

+    (top == null ==>

+      content == []) &&

+    (top != null ==>

+      top in representation && this !in top.footprint && top.footprint <= representation &&

+      content == top.content &&

+      top.Valid())

+  }

+

+  method InitUnboundedStack()

+    modifies this;

+    ensures IsUnboundedStack();

+    ensures content == [];

+  {

+    this.top := null;

+    this.content := [];

+    this.representation := {this};

+  }

+

+  method Push(val: T)

+    requires IsUnboundedStack();

+    modifies this;

+    ensures IsUnboundedStack();

+    ensures content == [val] + old(content);

+  {

+    var tmp := new Node<T>;

+    call tmp.InitNode(val,top);

+    top := tmp;

+    representation := representation + top.footprint;

+    content := [val] + content;

+  }

+

+  method Pop() returns (result: T)

+    requires IsUnboundedStack();

+    requires content != [];

+    modifies this;

+    ensures IsUnboundedStack();

+    ensures content == old(content)[1..];

+  {

+    result := top.val;

+    top := top.next;

+    content := content[1..];

+  }

+

+  method isEmpty() returns (result: bool)

+    requires IsUnboundedStack();

+    ensures result <==> content == [];

+  {

+    result := top == null;

+  }

+}

+

+class Node<T> {

+  ghost var footprint: set<object>;

+  ghost var content: seq<T>;

+  var val: T;

+  var next: Node<T>;

+

+  function Valid(): bool

+    reads this, footprint;

+  {

+    this in footprint &&

+    (next == null ==>

+      content == [val]) &&

+    (next != null ==>

+      next in footprint && next.footprint <= footprint && this !in next.footprint &&

+      content == [val] + next.content &&

+      next.Valid())

+  }

+

+  method InitNode(val: T, next: Node<T>)

+    requires next != null ==> next.Valid() && !(this in next.footprint);

+    modifies this;

+    ensures Valid();

+    ensures next != null ==> content == [val] + next.content && 

+                             footprint == {this} + next.footprint;

+    ensures next == null ==> content == [val] &&

+                             footprint == {this};

+  {

+    this.val := val;

+    this.next := next;

+    if (next == null) {

+      this.footprint := {this};

+      this.content := [val];      

+    } else {

+      this.footprint := {this} + next.footprint;

+      this.content := [val] + next.content;      

+    }

+  }

+}

diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat
new file mode 100644
index 00000000..aab76ff9
--- /dev/null
+++ b/Test/dafny1/runtest.bat
@@ -0,0 +1,26 @@
+@echo off

+setlocal

+

+set BOOGIEDIR=..\..\Binaries

+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

+set BPLEXE=%BOOGIEDIR%\Boogie.exe

+

+for %%f in (BQueue.bpl) do (

+  echo.

+  echo -------------------- %%f --------------------

+  %BPLEXE% %* %%f

+)

+

+for %%f in (Queue.dfy

+            BinaryTree.dfy

+            UnboundedStack.dfy

+            ListCopy.dfy ListReverse.dfy ListContents.dfy

+            SchorrWaite.dfy

+            SumOfCubes.dfy

+            TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy

+            Celebrity.dfy

+            UltraFilter.dfy) do (

+  echo.

+  echo -------------------- %%f --------------------

+  %DAFNY_EXE% /compile:0 %* %%f

+)