From 3baf6dafea70401444ddc94f1b353c3d32a66743 Mon Sep 17 00:00:00 2001 From: rustanleino 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/vacid0/LazyInitArray.dfy | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'Test/vacid0') 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 { 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| ==> -- cgit v1.2.3