From 2918a80203d42a51c45872dd6900eb3677d130eb Mon Sep 17 00:00:00 2001
From: Unknown <leino@LEINO4.redmond.corp.microsoft.com>
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/VSComp2010/Problem5-DoubleEndedQueue.dfy | 12 ++++--------
 1 file changed, 4 insertions(+), 8 deletions(-)

(limited to 'Test/VSComp2010')

diff --git a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
index cf109c1a..df8cb1b7 100644
--- a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
+++ b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
@@ -30,10 +30,8 @@ class AmortizedQueue<T> {
     modifies this;
     ensures Valid() && List == [];
   {
-    var tmp := new LinkedList<T>.Init();
-    front := tmp;
-    tmp := new LinkedList<T>.Init();
-    rear := tmp;
+    front := new LinkedList<T>.Init();
+    rear := new LinkedList<T>.Init();
     Repr := {this};
     Repr := Repr + front.Repr + rear.Repr;
     List := [];
@@ -52,8 +50,7 @@ class AmortizedQueue<T> {
       call ff := f.Concat(rr);
       front := ff;
 
-      var tmp := new LinkedList<T>.Init();
-      rear := tmp;
+      rear := new LinkedList<T>.Init();
     }
     Repr := {this};
     Repr := Repr + front.Repr + rear.Repr;
@@ -79,8 +76,7 @@ class AmortizedQueue<T> {
     ensures r != null && r.Valid() && r.List == List + [item];
   {
     call rr := rear.Cons(item);
-    var tmp := new AmortizedQueue<T>.InitFromPieces(front, rr);
-    r := tmp;
+    r := new AmortizedQueue<T>.InitFromPieces(front, rr);
   }
 }
 
-- 
cgit v1.2.3