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

3 files changed, 7 insertions, 11 deletions

diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy
index b790eea5..4ceca552 100644
--- a/Test/dafny1/ExtensibleArray.dfy
+++ b/Test/dafny1/ExtensibleArray.dfy
@@ -39,7 +39,7 @@ class ExtensibleArray<T> {
     ensures Valid() && fresh(Repr - {this});

     ensures Contents == [];

   {

-    var arr := new T[256];  elements := arr;

+    elements := new T[256];

     more := null;

     length := 0;

     M := 0;

@@ -90,15 +90,14 @@ class ExtensibleArray<T> {
       elements[length - M] := t;

     } else {

       if (more == null) {

-        var mr := new ExtensibleArray<array<T>>.Init();

-        more := mr;

-        Repr := Repr + {mr} + mr.Repr;

+        more := new ExtensibleArray<array<T>>.Init();

+        Repr := Repr + {more} + more.Repr;

       }

       // "elements" is full, so move it into "more" and allocate a new array

       call more.Append(elements);

       Repr := Repr + more.Repr;

       M := M + 256;

-      var arr := new T[256];  elements := arr;

+      elements := new T[256];

       Repr := Repr + {elements};

       elements[0] := t;

     }

diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy
index 957eb7cb..db1c60fa 100644
--- a/Test/dafny1/PriorityQueue.dfy
+++ b/Test/dafny1/PriorityQueue.dfy
@@ -27,8 +27,7 @@ class PriorityQueue {
     ensures N == capacity;

   {

     N := capacity;

-    var arr := new int[N+1];

-    a := arr;

+    a := new int[N+1];

     n := 0;

     Repr := {this};

     Repr := Repr + {a};

@@ -143,8 +142,7 @@ class PriorityQueue_Alternative {
     ensures N == capacity;

   {

     N := capacity;

-    var arr := new int[N+1];

-    a := arr;

+    a := new int[N+1];

     n := 0;

     Repr := {this};

     Repr := Repr + {a};

diff --git a/Test/dafny1/UnboundedStack.dfy b/Test/dafny1/UnboundedStack.dfy
index 940e1a0a..dfc10327 100644
--- a/Test/dafny1/UnboundedStack.dfy
+++ b/Test/dafny1/UnboundedStack.dfy
@@ -31,8 +31,7 @@ class UnboundedStack<T> {
     ensures IsUnboundedStack();

     ensures content == [val] + old(content);

   {

-    var tmp := new Node<T>.InitNode(val,top);

-    top := tmp;

+    top := new Node<T>.InitNode(val,top);

     representation := representation + top.footprint;

     content := [val] + content;

   }