Dafny:

* Added arrays
* Beefed up set axiomatization to know more things about set displays
* Added a simple heuristic that can infer some simple decreases clauses for loops
* Added Dafny solutions to a couple of VACID benchmarks

16 files changed, 652 insertions, 67 deletions

diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer
index 1efeba04..2a4587f4 100644
--- a/Test/VSI-Benchmarks/Answer
+++ b/Test/VSI-Benchmarks/Answer
@@ -5,7 +5,7 @@ Dafny program verifier finished with 10 verified, 0 errors
 

 -------------------- b2.dfy --------------------

 

-Dafny program verifier finished with 12 verified, 0 errors

+Dafny program verifier finished with 6 verified, 0 errors

 

 -------------------- b3.dfy --------------------

 

diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy
index ec255ed1..fd20a72b 100644
--- a/Test/VSI-Benchmarks/b2.dfy
+++ b/Test/VSI-Benchmarks/b2.dfy
@@ -1,27 +1,23 @@
 

-// Note:Implemented arrays as Dafny does not provide them

-

 class Benchmark2 {

-  method BinarySearch(a: Array, key: int) returns (result: int)

+  method BinarySearch(a: array<int>, key: int) returns (result: int)

     requires a != null;

-    requires (forall i, j ::

-                0 <= i && i < j && j < a.Length() ==> a.Get(i) <= a.Get(j));

-    ensures -1 <= result && result < a.Length();

-    ensures 0 <= result ==> a.Get(result) == key;

-    ensures result == -1 ==>

-              (forall i :: 0 <= i && i < a.Length() ==> a.Get(i) != key);

+    requires (forall i, j :: 0 <= i && i < j && j < |a| ==> a[i] <= a[j]);

+    ensures -1 <= result && result < |a|;

+    ensures 0 <= result ==> a[result] == key;

+    ensures result == -1 ==> (forall i :: 0 <= i && i < |a| ==> a[i] != key);

   {

     var low := 0;

-    var high := a.Length();

+    var high := |a|;

 

     while (low < high)

-      invariant 0 <= low && low <= high && high <= a.Length();

-      invariant (forall i :: 0 <= i && i < low ==> a.Get(i) < key);

-      invariant (forall i :: high <= i && i < a.Length() ==> key < a.Get(i));

+      invariant 0 <= low && low <= high && high <= |a|;

+      invariant (forall i :: 0 <= i && i < low ==> a[i] < key);

+      invariant (forall i :: high <= i && i < |a| ==> key < a[i]);

       decreases high - low;

     {

       var mid := low + (high - low) / 2;

-      var midVal := a.Get(mid);

+      var midVal := a[mid];

 

       if (midVal < key) {

         low := mid + 1;

@@ -36,47 +32,13 @@ class Benchmark2 {
   }

 }

 

-class Array {

-  var contents: seq<int>;

-  method Init(n: int)

-    requires 0 <= n;

-    modifies this;

-    ensures |contents| == n;

-  {

-    var i := 0;

-    contents := [];

-    while (i < n)

-      invariant i <= n && i == |contents|;

-      decreases n - i;

-    {

-      contents := contents + [0];

-      i := i + 1;

-    }

-  }

-   function method Length(): int

-    reads this;

-  { |contents| }

-   function method Get(i: int): int

-    requires 0 <= i && i < |contents|;

-    reads this;

-  { contents[i] }

-  method Set(i: int, x: int)

-    requires 0 <= i && i < |contents|;

-    modifies this;

-    ensures contents == old(contents)[i := x];

-  {

-    contents := contents[i := x];

-  }

-}

-

 method Main() {

-  var a := new Array;

-  call a.Init(5);

-  call a.Set(0, -4);

-  call a.Set(1, -2);

-  call a.Set(2, -2);

-  call a.Set(3, 0);

-  call a.Set(4, 25);

+  var a := new int[5];

+  a[0] := -4;

+  a[1] := -2;

+  a[2] := -2;

+  a[3] := 0;

+  a[4] := 25;

   call TestSearch(a, 4);

   call TestSearch(a, -8);

   call TestSearch(a, -2);

@@ -86,9 +48,9 @@ method Main() {
   call TestSearch(a, 27);

 }

 

-method TestSearch(a: Array, key: int)

+method TestSearch(a: array<int>, key: int)

   requires a != null;

-  requires (forall i, j :: 0 <= i && i < j && j < a.Length() ==> a.Get(i) <= a.Get(j));

+  requires (forall i, j :: 0 <= i && i < j && j < |a| ==> a[i] <= a[j]);

 {

   var b := new Benchmark2;

   call r := b.BinarySearch(a, key);

diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index 37b73cba..6d9c3ddd 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -64,7 +64,6 @@ class Benchmark3 {
 		invariant n <= |q.contents|;

 		invariant n == |p|;

 		invariant (forall i: int :: 0 <= i && i < n ==> p[i] == i);

-		decreases |q.contents| - n;

    {

 		p := p + [n];

 		n := n + 1;

@@ -121,7 +120,6 @@ class Benchmark3 {
       invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j]; //i.e. rotated

       invariant 0 <= k && k < |old(q.contents)| && old(q.contents)[k] == m;

       invariant (forall i ::0<= i && i < j ==> m <= old(q.contents)[i]); //m is min so far   

-      decreases n-j;

     {

 		call x:= q.Dequeue();

 		call q.Enqueue(x);

@@ -134,7 +132,6 @@ class Benchmark3 {
     while (j < k)

       invariant j <= k;

       invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j]; 

-      decreases k-j;

     {     

       call x := q.Dequeue();

       call q.Enqueue(x);

diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index ab1285f6..d2fca9bc 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -95,7 +95,6 @@ class Map<Key,Value> {
     while (j < |keys|)

       invariant j <= |keys|;

       invariant key !in keys[..j];

-      decreases |keys| -j;

     {

       if (keys[j] == key) {

         idx := j;

diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy
index e5af6357..2304e602 100644
--- a/Test/VSI-Benchmarks/b7.dfy
+++ b/Test/VSI-Benchmarks/b7.dfy
@@ -142,7 +142,6 @@ class Client {
     call wr.Create();

     while (0 < |q.contents|)

       invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && q !in wr.footprint;

-      decreases |q.contents|;

     {

       call ch := q.Dequeue();  

       call wr.PutChar(ch);    

diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index d8ee2013..34e0cfef 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -104,7 +104,6 @@ class Glossary {
         invariant q !in wr.footprint;

         invariant qcon == q.contents;

         invariant (forall k :: k in q.contents ==> k in glossary.keys);

-        decreases |definition| -i;

       {

         var w := definition[i];

         call present, d := glossary.Find(w);

@@ -342,7 +341,6 @@ class Map<Key,Value> {
     while (j < |keys|)

       invariant j <= |keys|;

       invariant key !in keys[..j];

-      decreases |keys| -j;

     {

       if (keys[j] == key) {

         idx := j;

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 726a6c13..59582de8 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -78,7 +78,8 @@ TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 0 (expected i
 TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 1 (expected C, got int)

 TypeTests.dfy(20,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Nothing' can be constructed

 TypeTests.dfy(23,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed

-9 resolution/type errors detected in TypeTests.dfy

+TypeTests.dfy(55,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+10 resolution/type errors detected in TypeTests.dfy

 

 -------------------- SmallTests.dfy --------------------

 SmallTests.dfy(30,7): Error: RHS expression must be well defined

@@ -123,7 +124,7 @@ Execution trace:
     (0,0): anon4_Else

     (0,0): anon3

 

-Dafny program verifier finished with 22 verified, 9 errors

+Dafny program verifier finished with 24 verified, 9 errors

 

 -------------------- Definedness.dfy --------------------

 Definedness.dfy(8,7): Error: possible division by zero

@@ -265,6 +266,50 @@ Execution trace:
 

 Dafny program verifier finished with 21 verified, 29 errors

 

+-------------------- Array.dfy --------------------

+Array.dfy(10,12): Error: assignment may update an array not in the enclosing method's modifies clause

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

+Array.dfy(17,9): Error: RHS expression must be well defined

+Execution trace:

+    (0,0): anon0

+Array.dfy(24,10): Error: LHS expression must be well defined

+Execution trace:

+    (0,0): anon0

+Array.dfy(48,20): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Array.dfy(56,12): Error: assignment may update an array not in the enclosing method's modifies clause

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

+Array.dfy(63,12): Error: assignment may update an array not in the enclosing method's modifies clause

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

+Array.dfy(95,18): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Array.dfy(107,6): Error: insufficient reads clause to read array element

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Then

+    (0,0): anon5_Then

+Array.dfy(115,6): Error: insufficient reads clause to read array element

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Then

+    (0,0): anon5_Then

+Array.dfy(131,10): Error: assignment may update an array not in the enclosing method's modifies clause

+Execution trace:

+    (0,0): anon0

+Array.dfy(138,10): Error: assignment may update an array not in the enclosing method's modifies clause

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 22 verified, 11 errors

+

 -------------------- Modules0.dfy --------------------

 Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T

 Modules0.dfy(13,7): Error: module T named among imports does not exist

diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy
new file mode 100644
index 00000000..928f2bc5
--- /dev/null
+++ b/Test/dafny0/Array.dfy
@@ -0,0 +1,156 @@
+class A {

+  method M() {

+    var y := new A[100];

+    y[5] := null;

+  }

+

+  method N0() {

+    var a;

+    if (a != null && 5 < |a|) {

+      a[5] := 12;  // error: violates modifies clause

+    }

+  }

+

+  method N1(a: array<int>)

+    modifies a;

+  {

+    var b := |a|;  // error: a may be null

+  }

+

+  method N2(a: array<int>)

+    requires a != null;

+    modifies a;

+  {

+    a[5] := 12;  // error: index may be outside bounds

+  }

+

+  method N3(a: array<int>)

+    requires a != null && 5 < |a|;

+    modifies a;

+    ensures (forall i :: 0 <= i && i < |a| ==> a[i] == old(a[i]) || (i == 5 && a[i] == 12));

+  {

+    a[5] := 12;  // all is good

+  }

+

+  var zz0: array<A>;

+  var zz1: array<B>;

+  method O() {

+    var zz2 := new A[25];

+    assert zz2 != zz0;  // holds because zz2 is newly allocated

+    /******  These would be good things to be able to verify, but the current encoding is not up to the task

+    var o: object := zz0;

+    assert this != o;  // holds because zz0 has a different type

+    if (zz0 != null && zz1 != null && 2 <= |zz0| && |zz0| == |zz1|) {

+      o := zz1[1];

+      assert zz0[1] == o ==> o == null;  // holds because zz0 and zz1 have different element types

+    }

+    ******/

+    assert zz2[20] == null;  // error: no reason that this must hold

+  }

+

+  var x: array<int>;

+  method P0()

+    modifies this;

+  {

+    if (x != null && 100 <= |x|) {

+      x[5] := 12;  // error: violates modifies clause

+    }

+  }

+  method P1()

+    modifies this`x;

+  {

+    if (x != null && 100 <= |x|) {

+      x[5] := 12;  // error: violates modifies clause

+    }

+  }

+  method P2()

+    modifies x;

+  {

+    if (x != null && 100 <= |x|) {

+      x[5] := 12;  // fine

+    }

+  }

+

+  method Q() {

+    var y := new object[100];

+    y[5] := null;

+    y[0..] := null;

+    y[..83] := null;

+    y[0..|y|] := null;

+  }

+

+  method R() {

+    var y := new int[100];

+    y[55] := 80;

+    y[10..] := 25;

+    y[..83] := 30;

+    y[50..60] := 35;

+    y[55] := 90;

+

+    assert y[54] == 35;

+    assert y[55] == 90;

+    assert y[83] == 25;

+    assert y[8] == 30;

+    assert y[90] + y[91] + y[0] + 20 == |y|;

+    assert y[93] == 24;  // error (it's 25)

+  }

+}

+

+class B { }

+

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

+

+class ArrayTests {

+  function F0(a: array<int>): bool

+  {

+    a != null && 10 <= |a| &&

+    a[7] == 13  // error: reads on something outside reads clause

+  }

+

+  var b: array<int>;

+  function F1(): bool

+    reads this;

+  {

+    b != null && 10 <= |b| &&

+    b[7] == 13  // error: reads on something outside reads clause

+  }

+

+  function F2(a: array<int>): bool

+    reads this, b, a;

+  {

+    a != null && 10 <= |a| &&

+    a[7] == 13  // good

+    &&

+    b != null && 10 <= |b| &&

+    b[7] == 13  // good

+  }

+

+  method M0(a: array<int>)

+    requires a != null && 10 <= |a|;

+  {

+    a[7] := 13;  // error: updates location not in modifies clause

+  }

+

+  method M1()

+    requires b != null && 10 <= |b|;

+    modifies this;

+  {

+    b[7] := 13;  // error: updates location not in modifies clause

+  }

+

+  method M2()

+    modifies this;

+  {

+    var bb := new int[75];

+    b := bb;  // fine

+  }

+

+  method M3(a: array<int>)

+    requires a != null && 10 <= |a|;

+    requires b != null && 10 <= |b|;

+    modifies this, b, a;

+  {

+    a[7] := 13;  // good

+    b[7] := 13;  // good

+  }

+}

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index ba6c8e0c..4e3fab69 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -150,4 +150,14 @@ class Modifies {
       m.x := m.x + 1;  // error: may violate modifies clause

     }

   }

+

+  method SetConstruction() {

+    var s := {1};

+    assert s != {};

+    if (*) {

+      assert s != {0,1};

+    } else {

+      assert s != {1,0};

+    }

+  }

 }

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 1616234e..fe8644be 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -45,3 +45,13 @@ datatype ReverseOrder_TheCounterpart<T> {
   More(ReverseOrder_MutuallyRecursiveDataType<T>);

 }

 

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

+

+class ArrayTests {

+  ghost method G(a: array<int>)

+    requires a != null && 10 <= |a|;

+    modifies a;

+  {

+    a[7] := 13;  // error: array elements are not ghost locations

+  }

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index fd90e479..c43ea782 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -17,7 +17,7 @@ for %%f in (BQueue.bpl) do (
   %BPLEXE% %* %%f

 )

 

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

+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

diff --git a/Test/vacid0/Answer b/Test/vacid0/Answer
new file mode 100644
index 00000000..6f270f92
--- /dev/null
+++ b/Test/vacid0/Answer
@@ -0,0 +1,12 @@
+

+-------------------- LazyInitArray.dfy --------------------

+

+Dafny program verifier finished with 7 verified, 0 errors

+

+-------------------- SparseArray.dfy --------------------

+

+Dafny program verifier finished with 9 verified, 0 errors

+

+-------------------- Composite.dfy --------------------

+

+Dafny program verifier finished with 14 verified, 0 errors

diff --git a/Test/vacid0/Composite.dfy b/Test/vacid0/Composite.dfy
new file mode 100644
index 00000000..28074c7b
--- /dev/null
+++ b/Test/vacid0/Composite.dfy
@@ -0,0 +1,160 @@
+class Composite {

+  var left: Composite;

+  var right: Composite;

+  var parent: Composite;

+  var val: int;

+  var sum: int;

+

+  function Valid(S: set<Composite>): bool

+    reads this, parent, left, right;

+  {

+    this in S &&

+    (parent != null ==> parent in S && (parent.left == this || parent.right == this)) &&

+    (left != null ==> left in S && left.parent == this && left != right) &&

+    (right != null ==> right in S && right.parent == this && left != right) &&

+    sum == val + (if left == null then 0 else left.sum) + (if right == null then 0 else right.sum)

+  }

+

+  function Acyclic(S: set<Composite>): bool

+    reads S;

+  {

+    this in S &&

+    (parent != null ==> parent.Acyclic(S - {this}))

+  }

+

+  method Init(x: int)

+    modifies this;

+    ensures Valid({this}) && Acyclic({this}) && val == x && parent == null;

+  {

+    parent := null;

+    left := null;

+    right := null;

+    val := x;

+    sum := val;

+  }

+

+  method Update(x: int, ghost S: set<Composite>)

+    requires this in S && Acyclic(S);

+    requires (forall c :: c in S ==> c != null && c.Valid(S));

+    modifies S;

+    ensures (forall c :: c in S ==> c.Valid(S));

+    ensures (forall c :: c in S ==> c.left == old(c.left) && c.right == old(c.right) && c.parent == old(c.parent));

+    ensures (forall c :: c in S && c != this ==> c.val == old(c.val));

+    ensures val == x;

+  {

+    var delta := x - val;

+    val := x;

+    call Adjust(delta, S, S);

+  }

+

+  method Add(ghost S: set<Composite>, child: Composite, ghost U: set<Composite>)

+    requires this in S && Acyclic(S);

+    requires (forall c :: c in S ==> c != null && c.Valid(S));

+    requires child != null && child in U;

+    requires (forall c :: c in U ==> c != null && c.Valid(U));

+    requires S !! U;

+    requires left == null || right == null;

+    requires child.parent == null;

+    // modifies only one of this.left and this.right, and child.parent, and various sum fields:

+    modifies S, child;

+    ensures child.left == old(child.left) && child.right == old(child.right) && child.val == old(child.val);

+    ensures (forall c :: c in S && c != this ==> c.left == old(c.left) && c.right == old(c.right));

+    ensures old(left) != null ==> left == old(left);

+    ensures old(right) != null ==> right == old(right);

+    ensures (forall c :: c in S ==> c.parent == old(c.parent) && c.val == old(c.val));

+    // sets child.parent to this:

+    ensures child.parent == this;

+    // leaves everything in S+U valid:

+    ensures (forall c :: c in S+U ==> c.Valid(S+U));

+  {

+    if (left == null) {

+      left := child;

+    } else {

+      right := child;

+    }

+    child.parent := this;

+    call Adjust(child.sum, S, S+U);

+  }

+

+  method Dislodge(ghost S: set<Composite>)

+    requires this in S && Acyclic(S);

+    requires (forall c :: c in S ==> c != null && c.Valid(S));

+    modifies S;

+    ensures (forall c :: c in S ==> c.Valid(S));

+    ensures (forall c :: c in S ==> c.val == old(c.val));

+    ensures (forall c :: c in S && c != this ==> c.parent == old(c.parent));

+    ensures (forall c :: c in S ==> c.left == old(c.left) || (old(c.left) == this && c.left == null));

+    ensures (forall c :: c in S ==> c.right == old(c.right) || (old(c.right) == this && c.right == null));

+    ensures Acyclic({this});

+  {

+    var p := parent;

+    parent := null;

+    if (p != null) {

+      assert (p.left == this) != (p.right == this);

+      if (p.left == this) {

+        p.left := null;

+      } else {

+        p.right := null;

+      }

+      var delta := -sum;

+      call p.Adjust(delta, S - {this}, S);

+    }

+  }

+

+  /*private*/ method Adjust(delta: int, ghost U: set<Composite>, ghost S: set<Composite>)

+    requires U <= S && Acyclic(U);

+    // everything else is valid:

+    requires (forall c :: c in S && c != this ==> c != null && c.Valid(S));

+    // this is almost valid:

+    requires parent != null ==> parent in S && (parent.left == this || parent.right == this);

+    requires left != null ==> left in S && left.parent == this && left != right;

+    requires right != null ==> right in S && right.parent == this && left != right;

+    // ... except that sum needs to be adjusted by delta:

+    requires sum + delta == val + (if left == null then 0 else left.sum) + (if right == null then 0 else right.sum);

+    // modifies sum fields in U:

+    modifies U`sum;

+    // everything is valid, including this:

+    ensures (forall c :: c in S ==> c.Valid(S));

+  {

+    var p := this;

+    ghost var T := U;

+    while (p != null)

+      invariant T <= U;

+      invariant p == null || p.Acyclic(T);

+      invariant (forall c :: c in S && c != p ==> c.Valid(S));

+      invariant p != null ==> p.sum + delta == p.val + (if p.left == null then 0 else p.left.sum) + (if p.right == null then 0 else p.right.sum);

+      invariant (forall c :: c in S ==> c.left == old(c.left) && c.right == old(c.right) && c.parent == old(c.parent) && c.val == old(c.val));

+      decreases T;

+    {

+      p.sum := p.sum + delta;

+      T := T - {p};

+      p := p.parent;

+    }

+  }

+}

+

+method Main()

+{

+  var c0 := new Composite;

+  call c0.Init(57);

+

+  var c1 := new Composite;

+  call c1.Init(12);

+  call c0.Add({c0}, c1, {c1});

+

+  var c2 := new Composite;

+  call c2.Init(48);

+

+  var c3 := new Composite;

+  call c3.Init(48);

+  call c2.Add({c2}, c3, {c3});

+  call c0.Add({c0,c1}, c2, {c2,c3});

+

+  ghost var S := {c0, c1, c2, c3};

+  call c1.Update(100, S);

+  call c2.Update(102, S);

+

+  call c2.Dislodge(S);

+  call c2.Update(496, S);

+  call c0.Update(0, S);

+}

diff --git a/Test/vacid0/LazyInitArray.dfy b/Test/vacid0/LazyInitArray.dfy
new file mode 100644
index 00000000..6ae00e24
--- /dev/null
+++ b/Test/vacid0/LazyInitArray.dfy
@@ -0,0 +1,105 @@
+class LazyInitArray<T> {

+  ghost var Contents: seq<T>;

+  var Zero: T;

+  /*private*/ var a: array<T>;

+  /*private*/ var b: array<int>;

+  /*private*/ var c: array<int>;

+  /*private*/ var n: int;

+  /*private*/ ghost var d: seq<int>;

+  /*private*/ ghost var e: seq<int>;

+  function Valid(): bool

+    reads this, a, b, c;

+  {

+    a != null && b != null && c != null &&

+    |a| == |Contents| + 1 &&  // TODO: remove the "+ 1" hack, which currently serves the purpose of distinguishing 'a' from 'b' and 'c'

+    |b| == |Contents| &&

+    |c| == |Contents| &&

+    b != c &&

+    0 <= n && n <= |c| &&

+    (forall i :: 0 <= i && i < |Contents| ==>

+       Contents[i] == (if 0 <= b[i] && b[i] < n && c[b[i]] == i then a[i] else Zero)) &&

+    (forall i :: 0 <= i && i < |Contents| ==>

+              ((exists j :: 0 <= j && j < n && c[j] == i)

+               <==>

+               0 <= b[i] && b[i] < n && c[b[i]] == i)) &&

+    // The idea behind d and e is the following:

+    //  *  d is a permutation of the first |Contents| natural numbers

+    //  *  e describes which permutation d is

+    //  *  c[..n] == d[..n]

+    |d| == |Contents| &&

+    |e| == |Contents| &&

+    (forall i :: 0 <= i && i < n ==> c[i] == d[i]) &&

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

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

+    (forall i :: 0 <= i && i < |e| ==> d[e[i]] == i)

+  }

+

+  method Init(N: int, zero: T)

+    requires 0 <= N;

+    modifies this, a, b, c;

+    ensures Valid();

+    ensures |Contents| == N && Zero == zero;

+    ensures (forall x :: x in Contents ==> x == zero);

+  {

+    var aa := new T[N+1];  a := aa;

+    var ii := new int[N];  b := ii;

+    ii := new int[N];      c := ii;

+    n := 0;

+

+    // initialize ghost variable Contents to a sequence of length N containing only zero's,

+    // and ghost variables d and e to be the identity sequences of length N

+    ghost var s := [];

+    ghost var id := [];

+    ghost var k := 0;

+    while (k < N)

+      invariant k <= N;

+      invariant |s| == k && (forall i :: 0 <= i && i < |s| ==> s[i] == zero);

+      invariant |id| == k && (forall i :: 0 <= i && i < k ==> id[i] == i);

+    {

+      s := s + [zero];

+      id := id + [k];

+      k := k + 1;

+    }

+

+    d := id;

+    e := id;

+    Zero := zero;

+    Contents := s;

+  }

+

+  method Get(i: int) returns (x: T)

+    requires Valid();

+    requires 0 <= i && i < |Contents|;

+    ensures x == Contents[i];

+  {

+    if (0 <= b[i] && b[i] < n && c[b[i]] == i) {

+      x := a[i];

+    } else {

+      x := Zero;

+    }

+  }

+

+  method Set(i: int, x: T)

+    requires Valid();

+    requires 0 <= i && i < |Contents|;

+    modifies this, a, b, c;

+    ensures Valid();

+    ensures |Contents| == |old(Contents)| && Contents == Contents[i := x];

+    ensures Zero == old(Zero);

+  {

+    if (0 <= b[i] && b[i] < n && c[b[i]] == i) {

+    } else {

+      assert n <= e[i];

+      b[i] := n;

+      c[n] := i;

+      ghost var t := d[n];

+      ghost var k := e[i];

+      d := d[n := i][k := t];

+      e := e[i := n][t := k];

+      n := n + 1;

+    }

+

+    a[i] := x;

+    Contents := Contents[i := x];

+  }

+}

diff --git a/Test/vacid0/SparseArray.dfy b/Test/vacid0/SparseArray.dfy
new file mode 100644
index 00000000..da1f63bb
--- /dev/null
+++ b/Test/vacid0/SparseArray.dfy
@@ -0,0 +1,120 @@
+class SparseArray<T> {

+  ghost var Contents: seq<T>;

+  var zero: T;

+  /*private*/ var a: seq<T>;  // should really be an array

+  /*private*/ var b: seq<int>;  // should really be an array

+  /*private*/ var c: seq<int>;  // should really be an array

+  /*private*/ var n: int;

+  /*private*/ ghost var d: seq<int>;  // would be better as an array

+  /*private*/ ghost var e: seq<int>;  // would be better as an array

+  function Valid(): bool

+    reads this;

+  {

+    |a| == |Contents| &&

+    |b| == |Contents| &&

+    |c| == |Contents| &&

+    0 <= n && n <= |c| &&

+    (forall i :: 0 <= i && i < |Contents| ==>

+       Contents[i] == (if 0 <= b[i] && b[i] < n && c[b[i]] == i then a[i] else zero)) &&

+    (forall i :: 0 <= i && i < |Contents| ==>

+              (i in c[..n] <==> 0 <= b[i] && b[i] < n && c[b[i]] == i)) &&

+    // The idea behind d and e is the following:

+    //  *  d is a permutation of the first |Contents| natural numbers

+    //  *  e describes which permutation d is

+    //  *  c[..n] == d[..n]

+    |d| == |Contents| &&

+    |e| == |Contents| &&

+    (forall i :: 0 <= i && i < n ==> c[i] == d[i]) &&

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

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

+    (forall i :: 0 <= i && i < |e| ==> d[e[i]] == i)

+  }

+

+  method Init(N: int, zero: T)

+    requires 0 <= N;

+    modifies this;

+    ensures Valid();

+    ensures |Contents| == N && this.zero == zero;

+    ensures (forall x :: x in Contents ==> x == zero);

+  {

+    var aa;

+    var ii;

+    call aa := AllocateArray(N);  this.a := aa;

+    call ii := AllocateArray(N);  this.b := ii;

+    call ii := AllocateArray(N);  this.c := ii;

+    this.n := 0;

+

+    // initialize ghost variable Contents to a sequence of length N containing only zero's,

+    // and ghost variables d and e to be the identity sequences of length N

+    ghost var s := [];

+    ghost var id := [];

+    ghost var k := 0;

+    while (k < N)

+      invariant k <= N;

+      invariant |s| == k;

+      // TODO: why doesn't this work instead of the next line?  invariant (forall x :: x in s ==> x == zero);

+      invariant (forall i :: 0 <= i && i < |s| ==> s[i] == zero);

+      invariant |id| == k && (forall i :: 0 <= i && i < k ==> id[i] == i);

+      decreases N - k;

+    {

+      s := s + [zero];

+      id := id + [k];

+      k := k + 1;

+    }

+

+    this.zero := zero;

+    this.Contents := s;

+    this.d := id;

+    this.e := id;

+  }

+  method Get(i: int) returns (x: T)

+    requires Valid();

+    requires 0 <= i && i < |Contents|;

+    ensures x == Contents[i];

+  {

+    if (0 <= b[i] && b[i] < n && c[b[i]] == i) {

+      x := a[i];

+    } else {

+      x := zero;

+    }

+  }

+  method Set(i: int, x: T)

+    requires Valid();

+    requires 0 <= i && i < |Contents|;

+    modifies this;

+    ensures Valid();

+    ensures |Contents| == |old(Contents)| && Contents == Contents[i := x];

+    ensures zero == old(zero);

+  {

+    if (0 <= b[i] && b[i] < n && c[b[i]] == i) {

+    } else {

+      assert n <= e[i];

+      b := b[i := n];

+      c := c[n := i];

+      ghost var t := d[n];

+      ghost var k := e[i];

+      d := d[n := i][k := t];

+      e := e[i := n][t := k];

+      n := n + 1;

+    }

+    a := a[i := x];

+    Contents := Contents[i := x];

+  }

+

+  /* The following method is here only to simulate support of arrays in Dafny */

+  /*private*/ static method AllocateArray<G>(n: int) returns (arr: seq<G>)

+    requires 0 <= n;

+    ensures |arr| == n;

+  {

+    arr := [];

+    var i := 0;

+    while (i < n)

+      invariant i <= n && |arr| == i;

+      decreases n - i;

+    {

+      var g: G;

+      arr := arr + [g];

+      i := i + 1;

+    }

+  }

+}

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

+setlocal

+

+set BOOGIEDIR=..\..\Binaries

+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

+set BPLEXE=%BOOGIEDIR%\Boogie.exe

+

+for %%f in (LazyInitArray.dfy SparseArray.dfy Composite.dfy) do (

+  echo.

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

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

+)