Dafny: Added Dafny solutions to the VSComp 2010 problems

7 files changed, 647 insertions, 0 deletions

diff --git a/Test/VSComp2010/Answer b/Test/VSComp2010/Answer
new file mode 100644
index 00000000..74aaae2b
--- /dev/null
+++ b/Test/VSComp2010/Answer
@@ -0,0 +1,25 @@
+

+-------------------- Problem1-SumMax.dfy --------------------

+

+Dafny program verifier finished with 4 verified, 0 errors

+Compiled program written to out.cs

+

+-------------------- Problem2-Invert.dfy --------------------

+

+Dafny program verifier finished with 7 verified, 0 errors

+Compiled program written to out.cs

+

+-------------------- Problem3-FindZero.dfy --------------------

+

+Dafny program verifier finished with 7 verified, 0 errors

+Compiled program written to out.cs

+

+-------------------- Problem4-Queens.dfy --------------------

+

+Dafny program verifier finished with 15 verified, 0 errors

+Compiled program written to out.cs

+

+-------------------- Problem5-DoubleEndedQueue.dfy --------------------

+

+Dafny program verifier finished with 21 verified, 0 errors

+Compiled program written to out.cs

diff --git a/Test/VSComp2010/Problem1-SumMax.dfy b/Test/VSComp2010/Problem1-SumMax.dfy
new file mode 100644
index 00000000..be7cc2c8
--- /dev/null
+++ b/Test/VSComp2010/Problem1-SumMax.dfy
@@ -0,0 +1,43 @@
+// VSComp 2010, problem 1, compute the sum and max of the elements of an array and prove

+// that 'sum <= N * max'.

+// Rustan Leino, 18 August 2010.

+//

+// The problem statement gave the pseudo-code for the method, but did not ask to prove

+// that 'sum' or 'max' return as the sum and max, respectively, of the array.  The

+// given assumption that the array's elements are non-negative is not needed to establish

+// the requested postcondition.

+

+method M(N: int, a: array<int>) returns (sum: int, max: int)

+  requires 0 <= N && a != null && |a| == N && (forall k :: 0 <= k && k < N ==> 0 <= a[k]);

+  ensures sum <= N * max;

+{

+  sum := 0;

+  max := 0;

+  var i := 0;

+  while (i < N)

+    invariant i <= N && sum <= i * max;

+  {

+    if (max < a[i]) {

+      max := a[i];

+    }

+    sum := sum + a[i];

+    i := i + 1;

+  }

+}

+

+method Main()

+{

+  var a := new int[10];

+  a[0] := 9;

+  a[1] := 5;

+  a[2] := 0;

+  a[3] := 2;

+  a[4] := 7;

+  a[5] := 3;

+  a[6] := 2;

+  a[7] := 1;

+  a[8] := 10;

+  a[9] := 6;

+  call s, m := M(10, a);

+  print "N = ", |a|, "  sum = ", s, "  max = ", m, "\n";

+}

diff --git a/Test/VSComp2010/Problem2-Invert.dfy b/Test/VSComp2010/Problem2-Invert.dfy
new file mode 100644
index 00000000..63da4cb5
--- /dev/null
+++ b/Test/VSComp2010/Problem2-Invert.dfy
@@ -0,0 +1,79 @@
+// VSComp 2010, problem 2, compute the inverse 'B' of a permutation 'A' and prove that 'B' is

+// indeed an inverse of 'A' (or at least prove that 'B' is injective).

+// Rustan Leino, 31 August 2010.

+//

+// In the version of this program that I wrote during the week of VSTTE 2010, I had

+// used a lemma (stated as a ghost method) that I proved inductively (using a loop and

+// a loop invariant).  Here, I have simplified that version by just including an

+// assertion of the crucial property, which follows from the surjectivity of 'A'.

+//

+// The difficulty in proving this program with an SMT solver stems from the fact that

+// the quantifier that states the surjectivity property has no good matching trigger

+// (because there are no function symbols mentioned in the antecedent of that quantifier,

+// only built-in predicates).  Therefore, I introduced a dummy function 'inImage' and

+// defined it always to equal 'true'.  I can then mention this function in the crucial

+// assertion, which causes the appropriate triggering to take place.

+//

+// A slight annoyance is that the loop's modifications of the heap, which is checked

+// to include only the elements of 'B'.  Since 'A' and 'B' are arrays stored at different

+// locations in the heap, it then follows that the elements of 'A' are not modified.

+// However, the fact that the heap has changed at all makes the symbolic expressions

+// denoting the elements of 'A' look different before and after the heap.  The

+// assertion after the loop (which, like all assertions, is proved) is needed to

+// connect the two.

+

+method M(N: int, A: array<int>, B: array<int>)

+  requires 0 <= N && A != null && B != null && N == |A| && N == |B| && A != B;

+  requires (forall k :: 0 <= k && k < N ==> 0 <= A[k] && A[k] < N);

+  requires (forall j,k :: 0 <= j && j < k && k < N ==> A[j] != A[k]);  // A is injective

+  requires (forall m :: 0 <= m && m < N && inImage(m) ==> (exists k :: 0 <= k && k < N && A[k] == m));  // A is surjective

+  modifies B;

+  ensures (forall k :: 0 <= k && k < N ==> 0 <= B[k] && B[k] < N);

+  ensures (forall k :: 0 <= k && k < N ==> B[A[k]] == k && A[B[k]] == k);  // A and B are each other's inverses

+  ensures (forall j,k :: 0 <= j && j < k && k < N ==> B[j] != B[k]);  // (which means that) B is injective

+{

+  var n := 0;

+  while (n < N)

+    invariant n <= N;

+    invariant (forall k :: 0 <= k && k < n ==> B[A[k]] == k);

+  {

+    B[A[n]] := n;

+    n := n + 1;

+  }

+  assert (forall i :: 0 <= i && i < N ==> A[i] == old(A[i]));  // the elements of A were not changed by the loop

+  // it now follows from the surjectivity of A that A is the inverse of B:

+  assert (forall j :: 0 <= j && j < N && inImage(j) ==> 0 <= B[j] && B[j] < N && A[B[j]] == j);

+}

+

+static function inImage(i: int): bool { true }  // this function is used to trigger the surjective quantification

+

+method Main()

+{

+  var a := new int[10];

+  a[0] := 9;

+  a[1] := 3;

+  a[2] := 8;

+  a[3] := 2;

+  a[4] := 7;

+  a[5] := 4;

+  a[6] := 0;

+  a[7] := 1;

+  a[8] := 5;

+  a[9] := 6;

+  var b := new int[10];

+  call M(10, a, b);

+  print "a:\n";

+  call PrintArray(a);

+  print "b:\n";

+  call PrintArray(b);

+}

+

+method PrintArray(a: array<int>)

+  requires a != null;

+{

+  var i := 0;

+  while (i < |a|) {

+    print a[i], "\n";

+    i := i + 1;

+  }

+}

diff --git a/Test/VSComp2010/Problem3-FindZero.dfy b/Test/VSComp2010/Problem3-FindZero.dfy
new file mode 100644
index 00000000..03e6bdfe
--- /dev/null
+++ b/Test/VSComp2010/Problem3-FindZero.dfy
@@ -0,0 +1,92 @@
+// VSComp 2010, problem 3, find a 0 in a linked list and return how many nodes were skipped

+// until the first 0 (or end-of-list) was found.

+// Rustan Leino, 18 August 2010.

+//

+// The difficulty in this problem lies in specifying what the return value 'r' denotes and in

+// proving that the program terminates.  Both of these are addressed by declaring a ghost

+// field 'List' in each linked-list node, abstractly representing the linked-list elements

+// from the node to the end of the linked list.  The specification can now talk about that

+// sequence of elements and can use 'r' as an index into the sequence, and termination can

+// be proved from the fact that all sequences in Dafny are finite.

+//

+// We only want to deal with linked lists whose 'List' field is properly filled in (which

+// can only happen in an acyclic list, for example).  To that avail, the standard idiom in

+// Dafny is to declare a predicate 'Valid()' that is true of an object when the data structure

+// representing object's abstract value is properly formed.  The definition of 'Valid()'

+// is what one intuitively would think of as the ''object invariant'', and it is mentioned

+// explicitly in method pre- and postconditions.  As part of this standard idiom, one also

+// declared a ghost variable 'Repr' that is maintained as the set of objects that make up

+// the representation of the aggregate object--in this case, the Node itself and all its

+// successors.

+

+class Node {

+  ghost var List: seq<int>;

+  ghost var Repr: set<Node>;

+  var head: int;

+  var next: Node;

+

+  function Valid(): bool

+    reads this, Repr;

+  {

+    this in Repr &&

+    1 <= |List| && List[0] == head &&

+    (next == null ==> |List| == 1) &&

+    (next != null ==>

+      next in Repr && next.Repr <= Repr && this !in next.Repr && next.Valid() && next.List == List[1..])

+  }

+

+  static method Cons(x: int, tail: Node) returns (n: Node)

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

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

+    ensures if tail == null then n.List == [x] else n.List == [x] + tail.List;

+  {

+    n := new Node;

+    n.head := x;

+    n.next := tail;

+    if (tail == null) {

+      n.List := [x];

+      n.Repr := {n};

+    } else {

+      n.List := [x] + tail.List;

+      n.Repr := {n} + tail.Repr;

+    }

+  }

+}

+

+static method Search(ll: Node) returns (r: int)

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

+  ensures ll == null ==> r == 0;

+  ensures ll != null ==>

+            0 <= r && r <= |ll.List| &&

+            (r < |ll.List| ==> ll.List[r] == 0 && 0 !in ll.List[..r]) &&

+            (r == |ll.List| ==> 0 !in ll.List);

+{

+  if (ll == null) {

+    r := 0;

+  } else {

+    var jj := ll;

+    var i := 0;

+    while (jj != null && jj.head != 0)

+      invariant jj != null ==> jj.Valid() && i + |jj.List| == |ll.List| && ll.List[i..] == jj.List;

+      invariant jj == null ==> i == |ll.List|;

+      invariant 0 !in ll.List[..i];

+      decreases |ll.List| - i;

+    {

+      jj := jj.next;

+      i := i + 1;

+    }

+    r := i;

+  }

+}

+

+method Main()

+{

+  var list: Node := null;

+  call list := list.Cons(0, list);

+  call list := list.Cons(5, list);

+  call list := list.Cons(0, list);

+  call list := list.Cons(8, list);

+  call r := Search(list);

+  print "Search returns ", r, "\n";

+  assert r == 1;

+}

diff --git a/Test/VSComp2010/Problem4-Queens.dfy b/Test/VSComp2010/Problem4-Queens.dfy
new file mode 100644
index 00000000..a07a2a5e
--- /dev/null
+++ b/Test/VSComp2010/Problem4-Queens.dfy
@@ -0,0 +1,219 @@
+// VSComp 2010, problem 4, N queens

+// Rustan Leino, 31 August 2010.

+//

+// In the version of this program that I wrote during the week of VSTTE 2010, I had

+// an unproved assumption.  In this version, I simply changed the existential quantifier

+// in that assumption to specify a particular witness, which is enough of a hint for

+// Dafny to fully prove the correctness of the program.

+//

+// Oh, I also added some comments in this version of the program.

+//

+// The correctness of this program relies on some properties of Queens boards.  These

+// are stated and proved as lemmas, which can be declared in Dafny as ghost methods.

+//

+// There are two annoyances in this program:

+//

+// One has to do with Dafny's split between ''ghost'' variables/code and ''physical''

+// variables/code.  The ''ghost'' things are used by the verifier, but are ignored by

+// the compiler.  This is generally good, since any additional specifications are ghost

+// state that are needed to convince the verifier that a program is correct (let alone

+// express what it means for the program to be correct) are not required at run time.

+// However, Dafny currently considers *all* quantifiers to be ghost-only, which

+// necessitates some duplication of the 'IsConsistent' condition.

+//

+// The other annoyance is that Dafny's proof-term representation of the function

+// 'IsConsistent' implicitly takes the heap as an argument, despite the fact that

+// 'IsConsistent' does not depend on any part of the heap.  Dafny ought to be able

+// to figure that out from the fact that 'IsConsistent' has no 'reads' clause.

+// Maybe a future version of Dafny will do just that.  But until then, some methods

+// below are specified with an (easy-to-prove) postcondition that 'IsConsistent(B,p)'

+// does not change for any 'B' and 'p', even if the method may change the heap in

+// some way.

+

+

+// The Search method returns whether or not there exists an N-queens solution for the

+// given N.  If 'success' returns as 'true', 'board' indicates a solution.  If 'success'

+// returns as 'false', no solution exists, as stated in the second postcondition.

+method Search(N: int) returns (success: bool, board: seq<int>)

+  requires 0 <= N;

+  ensures success ==>

+              |board| == N &&

+              (forall p :: 0 <= p && p < N ==> IsConsistent(board, p));

+  ensures !success ==>

+              (forall B ::

+                  |B| == N && (forall i :: 0 <= i && i < N ==> 0 <= B[i] && B[i] < N)

+                  ==>

+                  (exists p :: 0 <= p && p < N && !IsConsistent(B, p)));

+{

+  call success, board := SearchAux(N, []);

+}

+

+// Given a board, this function says whether or not the queen placed in column 'pos'

+// is consistent with the queens placed in columns to its left.

+static function IsConsistent(board: seq<int>, pos: int): bool

+{

+  0 <= pos && pos < |board| &&

+  (forall q :: 0 <= q && q < pos ==>

+      board[q] != board[pos] &&

+      board[q] - board[pos] != pos - q &&

+      board[pos] - board[q] != pos - q)

+}

+

+// The following lemma says that 'IsConsistent' is monotonic in its first argument.

+// More precisely, if 'short' is a board with a queen consistently placed in column

+// 'pos', then that queen is also consistently placed in any extension 'long' of the

+// board 'short' (that is, the sequence of queen positions 'short' is a prefix of the

+// sequence of queen positions 'long').  In other words, consistency of a queen in

+// column 'pos' does not depend on columns to the right of 'pos'.

+ghost method Lemma0(short: seq<int>, long: seq<int>, pos: int)

+  requires short <= long;

+  ensures IsConsistent(short, pos) ==> IsConsistent(long, pos);

+{

+  if (IsConsistent(short, pos)) {

+    assert IsConsistent(long, pos);

+  }

+}

+

+// Lemma1 states Lemma0 for every column in the board 'short'.

+ghost method Lemma1(short: seq<int>, long: seq<int>)

+  requires short <= long;

+  ensures (forall k :: 0 <= k && k < |short| && IsConsistent(short, k) ==> IsConsistent(long, k));

+  ensures (forall B, p :: IsConsistent(B, p) <==> old(IsConsistent(B, p)));

+{

+  var j := 0;

+  while (j < |short|)

+    invariant j <= |short|;

+    invariant (forall k :: 0 <= k && k < j && IsConsistent(short, k) ==> IsConsistent(long, k));

+  {

+    call Lemma0(short, long, j);

+    j := j + 1;

+  }

+}

+

+method CheckConsistent(board: seq<int>, pos: int) returns (b: bool)

+  ensures b <==> IsConsistent(board, pos);

+  ensures (forall B, p :: IsConsistent(B, p) <==> old(IsConsistent(B, p)));

+{

+  // The Dafny compiler won't compile a function with a 'forall' inside.  (This seems reasonable

+  // in general, since quantifiers could range over all the integers.  Here, however, where the

+  // range of the quantifier is bounded, it just seems stupid.)  Therefore, we

+  // have to provide a method that computes the same thing as the function defines.

+  if (0 <= pos && pos < |board|) {

+    var p := 0;

+    while (p < pos)

+      invariant p <= pos;

+      invariant (forall q :: 0 <= q && q < p ==>

+                  board[q] != board[pos] &&

+                  board[q] - board[pos] != pos - q &&

+                  board[pos] - board[q] != pos - q);

+    {

+      if (!(board[p] != board[pos] &&

+            board[p] - board[pos] != pos - p &&

+            board[pos] - board[p] != pos - p)) {

+        b := false;

+        return;

+      }

+      p := p + 1;

+    }

+    b := true;

+    return;

+  }

+  b := false;

+}

+

+// Here comes the method where the real work is being done.  With an ultimate board size of 'N'

+// in mind and given the consistent placement 'boardSoFar' of '|boardSoFar|' columns, this method

+// will search for a solution for the remaining columns.  If 'success' returns as 'true',

+// then 'newBoard' is a consistent placement of 'N' queens.  If 'success' returns as 'false',

+// then there is no way to extend 'boardSoFar' to get a solution for 'N' queens.

+method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard: seq<int>)

+  requires 0 <= N && |boardSoFar| <= N;

+  // consistent so far:

+  requires (forall k :: 0 <= k && k < |boardSoFar| ==> IsConsistent(boardSoFar, k));

+  ensures success ==>

+              |newBoard| == N &&

+              (forall p :: 0 <= p && p < N ==> IsConsistent(newBoard, p));

+  ensures !success ==>

+              (forall B ::

+                  |B| == N && (forall i :: 0 <= i && i < N ==> 0 <= B[i] && B[i] < N) &&

+                  boardSoFar <= B

+                  ==>

+                  (exists p :: 0 <= p && p < N && !IsConsistent(B, p)));

+  ensures (forall B, p :: IsConsistent(B, p) <==> old(IsConsistent(B, p)));

+  decreases N - |boardSoFar|;

+{

+  var pos := |boardSoFar|;

+  if (pos == N) {

+    // The given board already has the desired size.

+    newBoard := boardSoFar;

+    success := true;

+  } else {

+    // Exhaustively try all possibilities for the new column, 'pos'.

+    var n := 0;

+    while (n < N)

+      invariant n <= N;

+      invariant (forall B ::

+                  // For any board 'B' with 'N' queens, each placed in an existing row

+                  |B| == N && (forall i :: 0 <= i && i < N ==> 0 <= B[i] && B[i] < N) &&

+                  // ... where 'B' is an extension of 'boardSoFar'

+                  boardSoFar <= B &&

+                  // ... and the first column to extend 'boardSoFar' has a queen in one of

+                  // the first 'n' rows

+                  0 <= B[pos] && B[pos] < n

+                  ==>

+                  // ... the board 'B' is not entirely consistent

+                  (exists p :: 0 <= p && p < N && !IsConsistent(B, p)));

+    {

+      // Let's try to extend the board-so-far with a queen in column 'n':

+      var candidateBoard := boardSoFar + [n];

+      call consistent := CheckConsistent(candidateBoard, pos);

+      if (consistent) {

+        // The new queen is consistent.  Thus, 'candidateBoard' is consistent in column 'pos'.

+        // The consistency of the queens in columns left of 'pos' follows from the

+        // consistency of those queens in 'boardSoFar' and the fact that 'candidateBoard' is

+        // an extension of 'boardSoFar', as Lemma1 tells us:

+        call Lemma1(boardSoFar, candidateBoard);

+        // Thus, we meet the precondition of 'SearchAux' on 'candidateBoard', so let's search

+        // for a solution that extends 'candidateBoard'.

+        call s, b := SearchAux(N, candidateBoard);

+        if (s) {

+          // The recursive call to 'SearchAux' found consistent positions for all remaining columns

+          newBoard := b;

+          success := true;

+          return;

+        }

+        // The recursive call to 'SearchAux' determined that no consistent extensions to 'candidateBoard'

+        // exist.

+      } else {

+        // Since 'n' is not a consistent placement for a queen in column 'pos', there is also

+        // no extension of 'candidateBoard' that would make the entire board consistent.

+        assert (forall B ::

+                  |B| == N && (forall i :: 0 <= i && i < N ==> 0 <= B[i] && B[i] < N) &&

+                  candidateBoard <= B

+                  ==>

+                  !IsConsistent(B, pos));

+      }

+      n := n + 1;

+    }

+

+    success := false;

+  }

+}

+

+method Main()

+{

+  call s, b := Search(2);

+  print "N=2 returns ", s, "\n";

+  call s, b := Search(4);

+  print "N=4 returns ", s, "\n";

+  call PrintSeq(b);

+}

+

+method PrintSeq(b: seq<int>)

+{

+  var i := 0;

+  while (i < |b|) {

+    print "  ", b[i], "\n";

+    i := i + 1;

+  }

+}

diff --git a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
new file mode 100644
index 00000000..70b38a5d
--- /dev/null
+++ b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
@@ -0,0 +1,174 @@
+// VSComp 2010, problem 5, double-ended queue.

+// Rustan Leino, 18 August 2010.

+//

+// This program employs the standard Valid()/Repr idiom used in the dynamic-frames

+// style of specifications, see for example the comment in Problem3-FindZero.dfy.

+// Within that idiom, the specification is straightforward (if verbose), and there

+// are no particular wrinkles or annoyances in getting the verifier to prove the

+// correctness.

+

+class AmortizedQueue<T> {

+  // The front of the queue.

+  var front: LinkedList<T>;

+  // The rear of the queue (stored in reversed order).

+  var rear: LinkedList<T>;

+

+  ghost var Repr: set<object>;

+  ghost var List: seq<T>;

+

+  function Valid(): bool

+    reads this, Repr;

+  {

+    this in Repr &&

+    front != null && front in Repr && front.Repr <= Repr && front.Valid() &&

+    rear != null && rear in Repr && rear.Repr <= Repr && rear.Valid() &&

+    |rear.List| <= |front.List| &&

+    List == front.List + rear.ReverseSeq(rear.List)

+  }

+

+  method Init()

+    modifies this;

+    ensures Valid() && List == [];

+  {

+    var tmp := new LinkedList<T>;

+    front := tmp;

+    call front.Init();

+    tmp := new LinkedList<T>;

+    rear := tmp;

+    call rear.Init();

+    Repr := {this};

+    Repr := Repr + front.Repr + rear.Repr;

+    List := [];

+  }

+

+  method InitFromPieces(f: LinkedList<T>, r: LinkedList<T>)

+    requires f != null && f.Valid() && r != null && r.Valid();

+    modifies this;

+    ensures Valid() && List == f.List + r.ReverseSeq(r.List);

+  {

+    if (r.length <= f.length) {

+      front := f;

+      rear := r;

+    } else {

+      call rr := r.Reverse();

+      call ff := f.Concat(rr);

+      front := ff;

+

+      var tmp := new LinkedList<T>;

+      call tmp.Init();

+      rear := tmp;

+    }

+    Repr := {this};

+    Repr := Repr + front.Repr + rear.Repr;

+    List := front.List + rear.ReverseSeq(rear.List);

+  }

+

+  method Front() returns (t: T)

+    requires Valid() && List != [];

+    ensures t == List[0];

+  {

+    t := front.head;

+  }

+

+  method Tail() returns (r: AmortizedQueue<T>)

+    requires Valid() && List != [];

+    ensures r != null && r.Valid() && r.List == List[1..];

+  {

+    r := new AmortizedQueue<T>;

+    call r.InitFromPieces(front.tail, rear);

+  }

+

+  method Enqueue(item: T) returns (r: AmortizedQueue<T>)

+    requires Valid();

+    ensures r != null && r.Valid() && r.List == List + [item];

+  {

+    call rr := rear.Cons(item);

+    var tmp := new AmortizedQueue<T>;

+    call tmp.InitFromPieces(front, rr);

+    r := tmp;

+  }

+}

+

+

+class LinkedList<T> {

+  var head: T;

+  var tail: LinkedList<T>;

+  var length: int;

+

+  ghost var List: seq<T>;

+  ghost var Repr: set<LinkedList<T>>;

+

+  function Valid(): bool

+    reads this, Repr;

+  {

+    this in Repr &&

+    0 <= length && length == |List| &&

+    (length == 0 ==> List == [] && tail == null) &&

+    (length != 0 ==>

+      tail != null && tail in Repr &&

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

+      tail.Valid() &&

+      List == [head] + tail.List &&

+      length == tail.length + 1)

+  }

+

+  method Init()

+    modifies this;

+    ensures Valid() && List == [];

+  {

+    tail := null;

+    length := 0;

+    List := [];

+    Repr := {this};

+  }

+

+  method Cons(d: T) returns (r: LinkedList<T>)

+    requires Valid();

+    ensures r != null && r.Valid() && r.List == [d] + List;

+  {

+    r := new LinkedList<T>;

+    r.head := d;

+    r.tail := this;

+    r.length := length + 1;

+    r.List := [d] + List;

+    r.Repr := {r} + Repr;

+  }

+

+  method Concat(end: LinkedList<T>) returns (r: LinkedList<T>)

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

+    ensures r != null && r.Valid() && r.List == List + end.List;

+    decreases Repr;

+  {

+    if (length == 0) {

+      r := end;

+    } else {

+      call c := tail.Concat(end);

+      call r := c.Cons(head);

+    }

+  }

+

+  method Reverse() returns (r: LinkedList<T>)

+    requires Valid();

+    ensures r != null && r.Valid() && |List| == |r.List|;

+    ensures (forall k :: 0 <= k && k < |List| ==> List[k] == r.List[|List|-1-k]);

+    ensures r.List == ReverseSeq(List);

+    decreases Repr;

+  {

+    if (length == 0) {

+      r := this;

+    } else {

+      call r := tail.Reverse();

+      var e := new LinkedList<T>;

+      call e.Init();

+      call e := e.Cons(head);

+      call r := r.Concat(e);

+    }

+  }

+

+  static function method ReverseSeq(s: seq<T>): seq<T>

+    decreases s;

+  {

+    if s == [] then [] else

+    ReverseSeq(s[1..]) + [s[0]]

+  }

+}

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

+setlocal

+

+set BOOGIEDIR=..\..\Binaries

+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

+set BPLEXE=%BOOGIEDIR%\Boogie.exe

+

+

+for %%f in (Problem1-SumMax.dfy Problem2-Invert.dfy

+            Problem3-FindZero.dfy Problem4-Queens.dfy

+            Problem5-DoubleEndedQueue.dfy) do (

+  echo.

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

+  %DAFNY_EXE% %* %%f

+)