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/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";

 }