Dafny:

* Added full support for multi-dimensional arrays (except for one issue that still needs to be added in compilation)
* Changed syntax of array length from |a| to a.Length (for one-dimensional arrays).  The syntax for either dimensions is, for example, b.Length0 and b.Length1 for 2-dimensional arrays.
* Internally, this meant adding support for built-in classes and readonly fields

12 files changed, 209 insertions, 40 deletions

diff --git a/Test/VSComp2010/Problem1-SumMax.dfy b/Test/VSComp2010/Problem1-SumMax.dfy
index be7cc2c8..1b105ac1 100644
--- a/Test/VSComp2010/Problem1-SumMax.dfy
+++ b/Test/VSComp2010/Problem1-SumMax.dfy
@@ -8,7 +8,7 @@
 // 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]);

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

   ensures sum <= N * max;

 {

   sum := 0;

@@ -39,5 +39,5 @@ method Main()
   a[8] := 10;

   a[9] := 6;

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

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

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

 }

diff --git a/Test/VSComp2010/Problem2-Invert.dfy b/Test/VSComp2010/Problem2-Invert.dfy
index 63da4cb5..bf6aca37 100644
--- a/Test/VSComp2010/Problem2-Invert.dfy
+++ b/Test/VSComp2010/Problem2-Invert.dfy
@@ -23,7 +23,7 @@
 // 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 0 <= N && A != null && B != null && N == A.Length && N == B.Length && 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

@@ -72,7 +72,7 @@ method PrintArray(a: array<int>)
   requires a != null;

 {

   var i := 0;

-  while (i < |a|) {

+  while (i < a.Length) {

     print a[i], "\n";

     i := i + 1;

   }

diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy
index 1021ee85..6c6f11b3 100644
--- a/Test/VSI-Benchmarks/b2.dfy
+++ b/Test/VSI-Benchmarks/b2.dfy
@@ -2,18 +2,18 @@
 class Benchmark2 {

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

     requires a != null;

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

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

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

+    ensures -1 <= result && result < a.Length;

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

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

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

   {

     var low := 0;

-    var high := |a|;

+    var high := a.Length;

 

     while (low < high)

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

+      invariant 0 <= low && low <= high && high <= a.Length;

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

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

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

     {

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

       var midVal := a[mid];

@@ -49,7 +49,7 @@ method Main() {
 

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

   requires a != null;

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

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

 {

   var b := new Benchmark2;

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

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index b698f917..4b4bf920 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -267,7 +267,7 @@ 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

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

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

@@ -280,11 +280,11 @@ Execution trace:
 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

+Array.dfy(56,12): Error: assignment may update an array element 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

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

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

@@ -301,15 +301,29 @@ 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

+Array.dfy(131,10): Error: assignment may update an array element 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

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

 Execution trace:

     (0,0): anon0

 

 Dafny program verifier finished with 22 verified, 11 errors

 

+-------------------- MultiDimArray.dfy --------------------

+MultiDimArray.dfy(53,21): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon9_Then

+    (0,0): anon10_Then

+MultiDimArray.dfy(80,25): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+    (0,0): anon6_Then

+

+Dafny program verifier finished with 8 verified, 2 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
index 928f2bc5..048ecd7a 100644
--- a/Test/dafny0/Array.dfy
+++ b/Test/dafny0/Array.dfy
@@ -5,8 +5,8 @@ class A {
   }

 

   method N0() {

-    var a;

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

+    var a: array<int>;

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

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

     }

   }

@@ -14,7 +14,7 @@ class A {
   method N1(a: array<int>)

     modifies a;

   {

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

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

   }

 

   method N2(a: array<int>)

@@ -25,9 +25,9 @@ class A {
   }

 

   method N3(a: array<int>)

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

+    requires a != null && 5 < a.Length;

     modifies a;

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

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

   {

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

   }

@@ -52,21 +52,21 @@ class A {
   method P0()

     modifies this;

   {

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

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

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

     }

   }

   method P1()

     modifies this`x;

   {

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

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

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

     }

   }

   method P2()

     modifies x;

   {

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

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

       x[5] := 12;  // fine

     }

   }

@@ -76,7 +76,7 @@ class A {
     y[5] := null;

     y[0..] := null;

     y[..83] := null;

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

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

   }

 

   method R() {

@@ -91,7 +91,7 @@ class A {
     assert y[55] == 90;

     assert y[83] == 25;

     assert y[8] == 30;

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

+    assert y[90] + y[91] + y[0] + 20 == y.Length;

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

   }

 }

@@ -103,7 +103,7 @@ class B { }
 class ArrayTests {

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

   {

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

+    a != null && 10 <= a.Length &&

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

   }

 

@@ -111,28 +111,28 @@ class ArrayTests {
   function F1(): bool

     reads this;

   {

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

+    b != null && 10 <= b.Length &&

     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 != null && 10 <= a.Length &&

     a[7] == 13  // good

     &&

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

+    b != null && 10 <= b.Length &&

     b[7] == 13  // good

   }

 

   method M0(a: array<int>)

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

+    requires a != null && 10 <= a.Length;

   {

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

   }

 

   method M1()

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

+    requires b != null && 10 <= b.Length;

     modifies this;

   {

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

@@ -146,8 +146,8 @@ class ArrayTests {
   }

 

   method M3(a: array<int>)

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

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

+    requires a != null && 10 <= a.Length;

+    requires b != null && 10 <= b.Length;

     modifies this, b, a;

   {

     a[7] := 13;  // good

diff --git a/Test/dafny0/MultiDimArray.dfy b/Test/dafny0/MultiDimArray.dfy
new file mode 100644
index 00000000..ba5dc9da
--- /dev/null
+++ b/Test/dafny0/MultiDimArray.dfy
@@ -0,0 +1,91 @@
+class A {

+  // all of the following array types are allowed

+  var a: array<int>;

+  var b: array  <bool>;

+  var c: array <A>;

+  var d: array1 <A>;  // this is a synonym for array<A>

+  var e: array2 <A>;

+  var f: array3 <A>;

+  var g: array300 <A>;

+  var h: array3000 <array2<int>>;

+

+  method M0()

+    requires a != null && b != null;

+    modifies a;

+  {

+    if (5 <= a.Length && a.Length <= b.Length) {

+      var x := b[2];

+      var y := a[1];

+      var z := a[2];

+      a[2] := a[2] + 1;

+      assert x == b[2];

+      assert y == a[1];

+      assert z == a[2] - 1;

+    }

+  }

+

+  method M1()

+    requires a != null && d != null;

+    modifies a;

+  {

+    if (5 <= a.Length && a.Length <= d.Length) {

+      var x := d[2];

+      var y := a[1];

+      var z := a[2];

+      a[2] := a[2] + 1;

+      assert y == a[1];

+      assert z == a[2] - 1;

+      assert x == d[2];  // error: a and d may be equal

+    }

+  }

+

+  method M2(i: int, j: int, k: int, val: A)

+    requires f != null;

+    requires 0 <= i && i < f.Length0;

+    requires 0 <= j && j < f.Length1;

+    requires 0 <= k && k < f.Length2;

+    modifies f;

+  {

+    if (*) {

+      if (k < f.Length0) {

+        var save := f[k,j,k];

+        f[i,j,k] := val;

+        assert save == f[k,j,k];  // error: k and i may be equal

+      }

+    } else if (k < f.Length0 && k != i) {

+      if (k < f.Length0) {

+        var save := f[k,j,k];

+        f[i,j,k] := val;

+        assert save == f[k,j,k];  // fine

+      }

+    }

+  }

+

+  method M3(i: int, j: int, k: int)

+    requires f != null;

+    requires 0 <= i && i < f.Length0;

+    requires 0 <= j && j < f.Length1;

+    requires 0 <= k && k < f.Length2;

+    modifies f;

+    decreases i;

+  {

+    if (i != 0) {

+      var z := new A[2,3,5];  // first three primes (nice!)

+      var s := z[1,2,4];  // first three powers of 2 (tra-la-la)

+      var some: A;

+      f[i,j,k] := some;

+      call M3(i-1, j, k);

+      assert s == z[1,2,4];

+      if (*) {

+        assert f[i,j,k] == some;  // error: the recursive call may have modified any element in 'f'

+      }

+    }

+  }

+

+  method M4(a: array2<bool>) returns (k: int)

+    requires a != null;

+    ensures 0 <= k;

+  {

+    k := a.Length0 + a.Length1;

+  }

+}

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index ccdbcb91..6e8e2b72 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -49,7 +49,7 @@ datatype ReverseOrder_TheCounterpart<T> {
 

 class ArrayTests {

   ghost method G(a: array<int>)

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

+    requires a != null && 10 <= a.Length;

     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 d29edd34..16596fa5 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -11,7 +11,7 @@ for %%f in (Simple.dfy) do (
   %DAFNY_EXE% %* /dprint:- /env:0 /noVerify %%f

 )

 

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

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

             Modules0.dfy Modules1.dfy BadFunction.dfy

             Termination.dfy Use.dfy DTypes.dfy

             TypeParameters.dfy Datatypes.dfy SplitExpr.dfy Refinement.dfy RefinementErrors.dfy) do (

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index 71646dab..c81c0268 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -31,6 +31,10 @@ Dafny program verifier finished with 2 verified, 0 errors
 

 Dafny program verifier finished with 9 verified, 0 errors

 

+-------------------- MatrixFun.dfy --------------------

+

+Dafny program verifier finished with 4 verified, 0 errors

+

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

 

 Dafny program verifier finished with 10 verified, 0 errors

diff --git a/Test/dafny1/MatrixFun.dfy b/Test/dafny1/MatrixFun.dfy
new file mode 100644
index 00000000..96d89ad6
--- /dev/null
+++ b/Test/dafny1/MatrixFun.dfy
@@ -0,0 +1,59 @@
+method MirrorImage<T>(m: array2<T>)

+  requires m != null;

+  modifies m;

+  ensures (forall i,j :: 0 <= i && i < m.Length0 && 0 <= j && j < m.Length1 ==>

+            m[i,j] == old(m[i, m.Length1-1-j]));

+{

+  var a := 0;

+  while (a < m.Length0)

+    invariant a <= m.Length0;

+    invariant (forall i,j :: 0 <= i && i < a && 0 <= j && j < m.Length1 ==>

+                m[i,j] == old(m[i, m.Length1-1-j]));

+    invariant (forall i,j :: a <= i && i < m.Length0 && 0 <= j && j < m.Length1 ==>

+                m[i,j] == old(m[i,j]));

+  {

+    var b := 0;

+    while (b < m.Length1 / 2)

+      invariant  b <= m.Length1 / 2;

+      invariant (forall i,j :: 0 <= i && i < a && 0 <= j && j < m.Length1 ==>

+                  m[i,j] == old(m[i, m.Length1-1-j]));

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

+                  m[a,j] == old(m[a, m.Length1-1-j]) &&

+                  old(m[a,j]) == m[a, m.Length1-1-j]);

+      invariant (forall j :: b <= j && j < m.Length1-b ==> m[a,j] == old(m[a,j]));

+      invariant (forall i,j :: a+1 <= i && i < m.Length0 && 0 <= j && j < m.Length1 ==>

+                  m[i,j] == old(m[i,j]));

+    {

+      var tmp := m[a, m.Length1-1-b];

+      m[a, m.Length1-1-b] := m[a, b];

+      m[a, b] := tmp;

+      b := b + 1;

+    }

+    a := a + 1;

+  }

+}

+

+method Flip<T>(m: array2<T>)

+  requires m != null && m.Length0 == m.Length1;

+  modifies m;

+  ensures (forall i,j :: 0 <= i && i < m.Length0 && 0 <= j && j < m.Length1 ==> m[i,j] == old(m[j,i]));

+{

+  var N := m.Length0;

+  var a := 0;

+  var b := 0;

+  while (a != N)

+    invariant a <= b && b <= N;

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

+                (if i < a || (i == a && j < b)

+                  then m[i,j] == old(m[j,i]) && m[j,i] == old(m[i,j])

+                  else m[i,j] == old(m[i,j]) && m[j,i] == old(m[j,i])));

+    decreases N-a, N-b;

+  {

+    if (b < N) {

+      var tmp := m[a,b];  m[a,b] := m[b,a];  m[b,a] := tmp;

+      b := b + 1;

+    } else {

+      a := a + 1;  b := a;

+    }

+  }

+}

diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat
index eaee07d4..ea5b0ec7 100644
--- a/Test/dafny1/runtest.bat
+++ b/Test/dafny1/runtest.bat
@@ -16,6 +16,7 @@ for %%f in (Queue.dfy
             UnboundedStack.dfy

             SeparationLogicList.dfy

             ListCopy.dfy ListReverse.dfy ListContents.dfy

+            MatrixFun.dfy

             SchorrWaite.dfy

             SumOfCubes.dfy

             TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy

diff --git a/Test/vacid0/LazyInitArray.dfy b/Test/vacid0/LazyInitArray.dfy
index c5a032fe..fc4d687d 100644
--- a/Test/vacid0/LazyInitArray.dfy
+++ b/Test/vacid0/LazyInitArray.dfy
@@ -11,11 +11,11 @@ class LazyInitArray<T> {
     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| &&

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

+    b.Length == |Contents| &&

+    c.Length == |Contents| &&

     b != c &&

-    0 <= n && n <= |c| &&

+    0 <= n && n <= c.Length &&

     (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| ==>