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.

15 files changed, 3 insertions, 1958 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index e1b83c87..0c152d6e 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -64,10 +64,6 @@ class C {
 

 Dafny program verifier finished with 0 verified, 0 errors

 

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

-

-Boogie program verifier finished with 8 verified, 0 errors

-

 -------------------- TypeTests.dfy --------------------

 TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, got D)

 TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)

@@ -338,30 +334,6 @@ Execution trace:
 

 Dafny program verifier finished with 2 verified, 1 error

 

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

-

-Dafny program verifier finished with 22 verified, 0 errors

-

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

-

-Dafny program verifier finished with 4 verified, 0 errors

-

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

-

-Dafny program verifier finished with 24 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

-

 -------------------- Termination.dfy --------------------

 

 Dafny program verifier finished with 13 verified, 0 errors

@@ -423,27 +395,3 @@ Dafny program verifier finished with 24 verified, 2 errors
 -------------------- Datatypes.dfy --------------------

 

 Dafny program verifier finished with 10 verified, 0 errors

-

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

-

-Dafny program verifier finished with 12 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

-

--------------------- Tree.dfy --------------------

-

-Dafny program verifier finished with 6 verified, 0 errors

-

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

-

-Dafny program verifier finished with 11 verified, 0 errors

diff --git a/Test/dafny0/BQueue.bpl b/Test/dafny0/BQueue.bpl
deleted file mode 100644
index 77f1efb3..00000000
--- a/Test/dafny0/BQueue.bpl
+++ /dev/null
@@ -1,430 +0,0 @@
-// 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/dafny0/BinaryTree.dfy b/Test/dafny0/BinaryTree.dfy
deleted file mode 100644
index 8b4892dd..00000000
--- a/Test/dafny0/BinaryTree.dfy
+++ /dev/null
@@ -1,244 +0,0 @@
-class IntSet {

-  ghost var contents: set<int>;

-  ghost var footprint: set<object>;

-

-  var root: Node;

-

-  function Valid(): bool

-    reads this, footprint;

-  {

-    this in footprint &&

-    (root == null ==> contents == {}) &&

-    (root != null ==>

-       root in footprint && root.footprint <= footprint && this !in root.footprint &&

-       root.Valid() &&

-       contents == root.contents)

-  }

-

-  method Init()

-    modifies this;

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

-    ensures contents == {};

-  {

-    root := null;

-    footprint := {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 footprint;

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

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

-  { 

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

-    root := t;

-    contents := root.contents;

-    footprint := root.footprint + {this};

-  }

-

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

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

-    modifies n.footprint;

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

-    ensures n == null ==> fresh(m.footprint) && m.contents == {x};

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

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

-    decreases if n == null then {} else n.footprint;

-  {

-    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.footprint := n.footprint + n.left.footprint;

-      } else {

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

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

-        n.right := t;

-        n.footprint := n.footprint + n.right.footprint;

-      }

-      n.contents := n.contents + {x};

-      m := n;

-    }

-  }

-

-  method Remove(x: int)

-    requires Valid();

-    modifies footprint;

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

-    ensures contents == old(contents) - {x};

-  {

-    if (root != null) {

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

-      root := newRoot;

-      if (root == null) {

-        contents := {};

-        footprint := {this};

-      } else {

-        contents := root.contents;

-        footprint := root.footprint + {this};

-      }

-    }

-  }

-}

-

-class Node {

-  ghost var contents: set<int>;

-  ghost var footprint: set<object>;

-

-  var data: int;

-  var left: Node;

-  var right: Node;

-

-  function Valid(): bool

-    reads this, footprint;

-  {

-    this in footprint &&

-    null !in footprint &&

-    (left != null ==>

-      left in footprint &&

-      left.footprint <= footprint && this !in left.footprint &&

-      left.Valid() &&

-      (forall y :: y in left.contents ==> y < data)) &&

-    (right != null ==>

-      right in footprint &&

-      right.footprint <= footprint && this !in right.footprint &&

-      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.footprint !! right.footprint &&

-      contents == left.contents + {data} + right.contents)

-  }

-

-  method Init(x: int)

-    modifies this;

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

-    ensures contents == {x};

-  {

-    data := x;

-    left := null;

-    right := null;

-    contents := {x};

-    footprint := {this};

-  }

-

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

-    requires Valid();

-    ensures present <==> x in contents;

-    decreases footprint;

-  {

-    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 footprint;

-    ensures fresh(footprint - old(footprint));

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

-    ensures node == null ==> old(contents) <= {x};

-    ensures node != null ==> node.footprint <= footprint && node.contents == old(contents) - {x};

-    decreases footprint;

-  {

-    node := this;

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

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

-      left := t;

-      contents := contents - {x};

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

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

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

-      right := t;

-      contents := contents - {x};

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

-    } 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) { footprint := footprint + right.footprint; }

-      }

-    }

-  }

-

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

-    requires Valid();

-    modifies footprint;

-    ensures fresh(footprint - old(footprint));

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

-    ensures node == null ==> old(contents) == {min};

-    ensures node != null ==> node.footprint <= footprint && node.contents == old(contents) - {min};

-    ensures min in old(contents) && (forall x :: x in old(contents) ==> min <= x);

-    decreases footprint;

-  {

-    if (left == null) {

-      min := data;

-      node := right;

-    } else {

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

-      left := t;

-      node := this;

-      contents := contents - {min};

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

-    }

-  }

-}

-

-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.footprint;

-  {

-    call s.Insert(x);

-    call s.Insert(24);

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

-  }

-}

diff --git a/Test/dafny0/Celebrity.dfy b/Test/dafny0/Celebrity.dfy
deleted file mode 100644
index fd267c71..00000000
--- a/Test/dafny0/Celebrity.dfy
+++ /dev/null
@@ -1,95 +0,0 @@
-// 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/dafny0/ListContents.dfy b/Test/dafny0/ListContents.dfy
deleted file mode 100644
index 62636ce5..00000000
--- a/Test/dafny0/ListContents.dfy
+++ /dev/null
@@ -1,93 +0,0 @@
-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/dafny0/ListCopy.dfy b/Test/dafny0/ListCopy.dfy
deleted file mode 100644
index 52f5cf76..00000000
--- a/Test/dafny0/ListCopy.dfy
+++ /dev/null
@@ -1,55 +0,0 @@
-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/dafny0/ListReverse.dfy b/Test/dafny0/ListReverse.dfy
deleted file mode 100644
index ef029b88..00000000
--- a/Test/dafny0/ListReverse.dfy
+++ /dev/null
@@ -1,27 +0,0 @@
-

-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/dafny0/Queue.dfy b/Test/dafny0/Queue.dfy
deleted file mode 100644
index 42b7dd64..00000000
--- a/Test/dafny0/Queue.dfy
+++ /dev/null
@@ -1,202 +0,0 @@
-// 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/dafny0/SchorrWaite.dfy b/Test/dafny0/SchorrWaite.dfy
deleted file mode 100644
index a46e83a3..00000000
--- a/Test/dafny0/SchorrWaite.dfy
+++ /dev/null
@@ -1,272 +0,0 @@
-// 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/dafny0/Substitution.dfy b/Test/dafny0/Substitution.dfy
deleted file mode 100644
index 72415fea..00000000
--- a/Test/dafny0/Substitution.dfy
+++ /dev/null
@@ -1,120 +0,0 @@
-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/dafny0/SumOfCubes.dfy b/Test/dafny0/SumOfCubes.dfy
deleted file mode 100644
index b4fab490..00000000
--- a/Test/dafny0/SumOfCubes.dfy
+++ /dev/null
@@ -1,106 +0,0 @@
-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/dafny0/TerminationDemos.dfy b/Test/dafny0/TerminationDemos.dfy
deleted file mode 100644
index 6b63bfec..00000000
--- a/Test/dafny0/TerminationDemos.dfy
+++ /dev/null
@@ -1,80 +0,0 @@
-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/dafny0/Tree.dfy b/Test/dafny0/Tree.dfy
deleted file mode 100644
index 58124171..00000000
--- a/Test/dafny0/Tree.dfy
+++ /dev/null
@@ -1,72 +0,0 @@
-// ------------------ 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/dafny0/UnboundedStack.dfy b/Test/dafny0/UnboundedStack.dfy
deleted file mode 100644
index 4c3b095a..00000000
--- a/Test/dafny0/UnboundedStack.dfy
+++ /dev/null
@@ -1,98 +0,0 @@
-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/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index eb7ea4f7..aa45ca05 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -11,19 +11,10 @@ for %%f in (Simple.dfy) do (
   %DAFNY_EXE% %* /dprint:- /env:0 /noVerify %%f

 )

 

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

-  echo.

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

-  %BPLEXE% %* %%f

-)

-

 for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy Array.dfy

-            Modules0.dfy Modules1.dfy BadFunction.dfy Queue.dfy ListCopy.dfy

-            BinaryTree.dfy ListReverse.dfy ListContents.dfy

-            SchorrWaite.dfy Termination.dfy Use.dfy DTypes.dfy

-            TypeParameters.dfy Datatypes.dfy UnboundedStack.dfy

-            SumOfCubes.dfy TerminationDemos.dfy Substitution.dfy

-            Tree.dfy Celebrity.dfy) do (

+            Modules0.dfy Modules1.dfy BadFunction.dfy

+            Termination.dfy Use.dfy DTypes.dfy

+            TypeParameters.dfy Datatypes.dfy) do (

   echo.

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

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