From 3baf6dafea70401444ddc94f1b353c3d32a66743 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Fri, 17 Sep 2010 01:26:47 +0000
Subject: 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

---
 Test/VSComp2010/Problem1-SumMax.dfy | 4 ++--
 Test/VSComp2010/Problem2-Invert.dfy | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'Test/VSComp2010')

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;
   }
-- 
cgit v1.2.3