From 7cabbe6e10f11b90df4e4b5f5a3bb1c2253b87c5 Mon Sep 17 00:00:00 2001 From: Jason Koenig Date: Wed, 13 Jun 2012 11:54:11 -0700 Subject: Dafny: liberalized equality to work when the types could possibly be the same (i.e. a != b is allowed when a: array and b: array) --- Test/vacid0/LazyInitArray.dfy | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'Test/vacid0') diff --git a/Test/vacid0/LazyInitArray.dfy b/Test/vacid0/LazyInitArray.dfy index e56a8317..3e5a95ef 100644 --- a/Test/vacid0/LazyInitArray.dfy +++ b/Test/vacid0/LazyInitArray.dfy @@ -11,10 +11,10 @@ class LazyInitArray { reads this, a, b, c; { a != null && b != null && c != null && - a.Length == |Contents| + 1 && // TODO: remove the "+ 1" hack, which currently serves the purpose of distinguishing 'a' from 'b' and 'c' + a.Length == |Contents| && b.Length == |Contents| && c.Length == |Contents| && - b != c && + b != c && a != b && a != 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)) && @@ -41,7 +41,7 @@ class LazyInitArray { ensures |Contents| == N && Zero == zero; ensures (forall x :: x in Contents ==> x == zero); { - a := new T[N+1]; + a := new T[N]; b := new int[N]; c := new int[N]; n := 0; -- cgit v1.2.3