From 2918a80203d42a51c45872dd6900eb3677d130eb Mon Sep 17 00:00:00 2001 From: Unknown Date: Tue, 5 Apr 2011 17:03:28 -0700 Subject: Dafny: Allow field selections and array-element selection as LHSs of assignments where RHS is not just an expression --- 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 fc4d687d..e56a8317 100644 --- a/Test/vacid0/LazyInitArray.dfy +++ b/Test/vacid0/LazyInitArray.dfy @@ -41,9 +41,9 @@ class LazyInitArray { ensures |Contents| == N && Zero == zero; ensures (forall x :: x in Contents ==> x == zero); { - var aa := new T[N+1]; a := aa; - var ii := new int[N]; b := ii; - ii := new int[N]; c := ii; + a := new T[N+1]; + b := new int[N]; + c := new int[N]; n := 0; // initialize ghost variable Contents to a sequence of length N containing only zero's, -- cgit v1.2.3