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

1 files changed, 2 insertions, 2 deletions

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;

   }