Dafny: Allow field selections and array-element selection as LHSs of assignments where RHS is not just an expression

1 files changed, 4 insertions, 8 deletions

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);

   }

 }