Dafny: Translate general LHSs for var and := (not yet for call, no compilation yet)

10 files changed, 406 insertions, 160 deletions

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index dae4125e..10314038 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -741,7 +741,7 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall>
     | "." Ident<out x>

       "("                              (. args = new List<Expression/*!*/>(); .)

         [ Expressions<args> ]

-      ")"                              (. initCall = new CallStmt(x, new List<IdentifierExpr>(),

+      ")"                              (. initCall = new CallStmt(x, new List<Expression>(),

                                                                   receiverForInitCall, x.val, args); .)

     ]

     (. if (ee != null) {

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 125d923c..ff525820 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -1546,13 +1546,13 @@ namespace Microsoft.Dafny {
       Contract.Invariant(cce.NonNullElements(Args));

     }

 

-    public readonly List<IdentifierExpr/*!*/>/*!*/ Lhs;

+    public readonly List<Expression/*!*/>/*!*/ Lhs;

     public readonly Expression/*!*/ Receiver;

     public readonly string/*!*/ MethodName;

     public readonly List<Expression/*!*/>/*!*/ Args;

     public Method Method;  // filled in by resolution

 

-    public CallStmt(IToken tok, List<IdentifierExpr/*!*/>/*!*/ lhs, Expression/*!*/ receiver,

+    public CallStmt(IToken tok, List<Expression/*!*/>/*!*/ lhs, Expression/*!*/ receiver,

       string/*!*/ methodName, List<Expression/*!*/>/*!*/ args)

       : base(tok) {

       Contract.Requires(tok != null);

diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index e26477ff..c3648310 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -1309,7 +1309,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 						Expressions(args);

 					}

 					Expect(34);

-					initCall = new CallStmt(x, new List<IdentifierExpr>(),

+					initCall = new CallStmt(x, new List<Expression>(),

 					                       receiverForInitCall, x.val, args); 

 				}

 			}

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index f8320f10..7afeda44 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -806,7 +806,7 @@ namespace Microsoft.Dafny {
           } else {

             Error(t.tok, "Type parameter expects no type arguments: {0}", t.Name);

           }

-        } else if (t.ResolvedClass == null) {  // this test is becausee 'array' is already resolved; TODO: an alternative would be to pre-populate 'classes' with built-in references types like 'array' (and perhaps in the future 'string')

+        } else if (t.ResolvedClass == null) {  // this test is because 'array' is already resolved; TODO: an alternative would be to pre-populate 'classes' with built-in references types like 'array' (and perhaps in the future 'string')

           TopLevelDecl d;

           if (!classes.TryGetValue(t.Name, out d)) {

             Error(t.tok, "Undeclared top-level type or type parameter: {0}", t.Name);

@@ -1186,10 +1186,15 @@ namespace Microsoft.Dafny {
       } else if (stmt is UpdateStmt) {

         var s = (UpdateStmt)stmt;

         int prevErrorCount = ErrorCount;

-        // First, resolve all LHS's and expression-looking RHS's.  When resolving these, allow ghosts for now, but enforce restrictions later.

+        // First, resolve all LHS's and expression-looking RHS's.

+        SeqSelectExpr arrayRangeLhs = null;

         foreach (var lhs in s.Lhss) {

           if (lhs is SeqSelectExpr) {

-            ResolveSeqSelectExpr((SeqSelectExpr)lhs, true, true);

+            var sse = (SeqSelectExpr)lhs;

+            ResolveSeqSelectExpr(sse, true, true);

+            if (arrayRangeLhs == null && !sse.SelectOne) {

+              arrayRangeLhs = sse;

+            }

           } else {

             ResolveExpression(lhs, true);

           }

@@ -1199,8 +1204,9 @@ namespace Microsoft.Dafny {
         foreach (var rhs in s.Rhss) {

           bool isEffectful;

           if (rhs is TypeRhs) {

-            ResolveTypeRhs((TypeRhs)rhs, stmt, specContextOnly, method);

-            isEffectful = true;

+            var tr = (TypeRhs)rhs;

+            ResolveTypeRhs(tr, stmt, specContextOnly, method);

+            isEffectful = tr.InitCall != null;

           } else if (rhs is HavocRhs) {

             isEffectful = false;

           } else {

@@ -1228,7 +1234,7 @@ namespace Microsoft.Dafny {
           var ie = lhs.Resolved as IdentifierExpr;

           if (ie != null) {

             if (lhsNameSet.ContainsKey(ie.Name)) {

-              Error(s, "Duplicate variable in left-hand side of call statement: {0}", ie.Name);

+              Error(s, "Duplicate variable in left-hand side of {1} statement: {0}", ie.Name, callRhs != null ? "call" : "assignment");

             } else {

               lhsNameSet.Add(ie.Name, null);

             }

@@ -1242,19 +1248,21 @@ namespace Microsoft.Dafny {
             Error(s, "expected method call, found expression");

           } else  if (s.Lhss.Count != s.Rhss.Count) {

             Error(s, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, s.Rhss.Count);

+          } else if (arrayRangeLhs != null && s.Lhss.Count != 1) {

+            Error(arrayRangeLhs, "array-range may not be used as LHS of multi-assignment; use separate assignment statements for each array-range assignment");

           } else if (ErrorCount == prevErrorCount) {

+            // add the statements here in a sequence, but don't use that sequence later for translation (instead, should translated properly as multi-assignment)

             for (int i = 0; i < s.Lhss.Count; i++) {

               var a = new AssignStmt(s.Tok, s.Lhss[i].Resolved, s.Rhss[i]);

               s.ResolvedStatements.Add(a);

             }

-            if (s.Lhss.Count != 1) {

-              Error(s, "multi-assignments not yet supported");  // TODO

-            }

           }

         } else {

           // if there was an effectful RHS, that must be the only RHS

           if (s.Rhss.Count != 1) {

             Error(firstEffectfulRhs, "an update statement is allowed an effectful RHS only if there is just one RHS");

+          } else if (arrayRangeLhs != null) {

+            Error(arrayRangeLhs, "Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable");

           } else if (callRhs == null) {

             // must be a single TypeRhs

             if (s.Lhss.Count != 1) {

@@ -1267,16 +1275,11 @@ namespace Microsoft.Dafny {
           } else {

             // a call statement

             if (ErrorCount == prevErrorCount) {

-              var idLhss = new List<IdentifierExpr>();

+              var resolvedLhss = new List<Expression>();

               foreach (var ll in s.Lhss) {

-                var ie = ll.Resolved as IdentifierExpr;  // TODO: the CallStmt should handle all LHS's, not just identifier expressions

-                if (ie == null) {

-                  Error(ll, "actual out-parameters of calls must be variables, not fields");

-                } else {

-                  idLhss.Add(ie);

-                }

+                resolvedLhss.Add(ll.Resolved);

               }

-              var a = new CallStmt(callRhs.Tok, idLhss, callRhs.Receiver, callRhs.MethodName, callRhs.Args);

+              var a = new CallStmt(callRhs.Tok, resolvedLhss, callRhs.Receiver, callRhs.MethodName, callRhs.Args);

               s.ResolvedStatements.Add(a);

             }

           }

@@ -1799,13 +1802,29 @@ namespace Microsoft.Dafny {
         }

         for (int i = 0; i < callee.Outs.Count; i++) {

           Type st = SubstType(callee.Outs[i].Type, subst);

-          IdentifierExpr lhs = s.Lhs[i];

+          var lhs = s.Lhs[i];

           if (!UnifyTypes(cce.NonNull(lhs.Type), st)) {

             Error(s, "incorrect type of method out-parameter {0} (expected {1}, got {2})", i, st, lhs.Type);

-          } else if (!specContextOnly && !cce.NonNull(lhs.Var).IsGhost && (s.IsGhost || callee.Outs[i].IsGhost)) {

-            if (lhs is AutoGhostIdentifierExpr && lhs.Var is VarDecl) {

-              ((VarDecl)lhs.Var).MakeGhost();

+          } else if (!specContextOnly && (s.IsGhost || callee.Outs[i].IsGhost)) {

+            // LHS must denote a ghost

+            lhs = lhs.Resolved;

+            if (lhs is IdentifierExpr) {

+              var ll = (IdentifierExpr)lhs;

+              if (!ll.Var.IsGhost) {

+                if (ll is AutoGhostIdentifierExpr && ll.Var is VarDecl) {

+                  // the variable was actually declared in this statement, so auto-declare it as ghost

+                  ((VarDecl)ll.Var).MakeGhost();

+                } else {

+                  Error(s, "actual out-parameter {0} is required to be a ghost variable", i);

+                }

+              }

+            } else if (lhs is FieldSelectExpr) {

+              var ll = (FieldSelectExpr)lhs;

+              if (!ll.Field.IsGhost) {

+                Error(s, "actual out-parameter {0} is required to be a ghost field", i);

+              }

             } else {

+              // this is an array update, and arrays are always non-ghost

               Error(s, "actual out-parameter {0} is required to be a ghost variable", i);

             }

           }

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 8752ffea..00071fd8 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -914,19 +914,19 @@ namespace Microsoft.Dafny {
 

     /// <summary>

     /// Returns an expression whose value is the same as "expr", but that is guaranteed to preserve the its value passed

-    /// the evaluation of "rhs".  If necessary, a new local variable called "name" with type "ty" is added to "locals" and

+    /// the evaluation of other expressions.  If necessary, a new local variable called "name" with type "ty" is added to "locals" and

     /// assigned in "builder" to be used to hold the value of "expr".  It is assumed that all requests for a given "name"

     /// have the same type "ty" and that these variables can be shared.

+    /// As an optimization, if "otherExprsCanAffectPreviouslyKnownExpressions" is "false", then "expr" itself is returned.

     /// </summary>

-    Bpl.Expr SaveInTemp(Bpl.Expr expr, AssignmentRhs rhs, string name, Bpl.Type ty, Bpl.StmtListBuilder builder, Bpl.VariableSeq locals) {

+    Bpl.Expr SaveInTemp(Bpl.Expr expr, bool otherExprsCanAffectPreviouslyKnownExpressions, string name, Bpl.Type ty, Bpl.StmtListBuilder builder, Bpl.VariableSeq locals) {

       Contract.Requires(expr != null);

-      Contract.Requires(rhs != null);

       Contract.Requires(name != null);

       Contract.Requires(ty != null);

       Contract.Requires(locals != null);

       Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

 

-      if (rhs.CanAffectPreviouslyKnownExpressions) {

+      if (otherExprsCanAffectPreviouslyKnownExpressions) {

         var save = GetTmpVar_IdExpr(expr.tok, name, ty, locals);

         builder.Add(Bpl.Cmd.SimpleAssign(expr.tok, save, expr));

         return save;

@@ -2963,10 +2963,57 @@ namespace Microsoft.Dafny {
       } else if (stmt is ReturnStmt) {

         AddComment(builder, stmt, "return statement");

         builder.Add(new Bpl.ReturnCmd(stmt.Tok));

+      } else if (stmt is UpdateStmt) {

+        var s = (UpdateStmt)stmt;

+        // This UpdateStmt can be single-target assignment, a multi-assignment, a call statement, or

+        // an array-range update.  Handle the multi-assignment here and handle the others as for .ResolvedStatements.

+        var resolved = s.ResolvedStatements;

+        if (resolved.Count == 1) {

+          TrStmt(resolved[0], builder, locals, etran);

+        } else {

+          AddComment(builder, s, "update statement");

+          var lhss = new List<Expression>();

+          foreach (var lhs in s.Lhss) {

+            lhss.Add(lhs.Resolved);

+          }

+          bool rhssCanAffectPreviouslyKnownExpressions = !s.Rhss.TrueForAll(rhs => !rhs.CanAffectPreviouslyKnownExpressions);

+          List<AssignToLhs> lhsBuilder;

+          List<Bpl.IdentifierExpr> bLhss;

+          ProcessLhss(lhss, rhssCanAffectPreviouslyKnownExpressions, builder, locals, etran, out lhsBuilder, out bLhss);

+          ProcessRhss(lhsBuilder, bLhss, lhss, s.Rhss, builder, locals, etran);

+          builder.Add(CaptureState(s.Tok));

+        }

+

       } else if (stmt is AssignStmt) {

         AddComment(builder, stmt, "assignment statement");

         AssignStmt s = (AssignStmt)stmt;

-        TrAssignment(stmt.Tok, s.Lhs.Resolved, s.Rhs, builder, locals, etran);

+        var sel = s.Lhs.Resolved as SeqSelectExpr;

+        if (sel != null && !sel.SelectOne) {

+          // check LHS for definedness

+          TrStmt_CheckWellformed(sel, builder, locals, etran, true);

+          // array-range assignment

+          var obj = etran.TrExpr(sel.Seq);

+          Bpl.Expr low = sel.E0 == null ? Bpl.Expr.Literal(0) : etran.TrExpr(sel.E0);

+          Bpl.Expr high = sel.E1 == null ? ArrayLength(s.Tok, obj, 1, 0) : etran.TrExpr(sel.E1);

+          // check frame:

+          // assert (forall i: int :: low <= i && i < high ==> $_Frame[arr,i]);

+          Bpl.Variable iVar = new Bpl.BoundVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$i", Bpl.Type.Int));

+          Bpl.IdentifierExpr ie = new Bpl.IdentifierExpr(s.Tok, iVar);

+          Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Le(low, ie), Bpl.Expr.Lt(ie, high));

+          Bpl.Expr fieldName = FunctionCall(s.Tok, BuiltinFunction.IndexField, null, ie);

+          Bpl.Expr cons = Bpl.Expr.SelectTok(s.Tok, etran.TheFrame(s.Tok), obj, fieldName);

+          Bpl.Expr q = new Bpl.ForallExpr(s.Tok, new Bpl.VariableSeq(iVar), Bpl.Expr.Imp(ante, cons));

+          builder.Add(Assert(s.Tok, q, "assignment may update an array element not in the enclosing method's modifies clause"));

+          // compute the RHS

+          Bpl.Expr bRhs = TrAssignmentRhs(s.Tok, null, null, s.Rhs, sel.Type, builder, locals, etran);

+          // do the update:  call UpdateArrayRange(arr, low, high, rhs);

+          builder.Add(new Bpl.CallCmd(s.Tok, "UpdateArrayRange",

+            new Bpl.ExprSeq(obj, low, high, bRhs),

+            new Bpl.IdentifierExprSeq()));

+          builder.Add(CaptureState(s.Tok));

+        } else {

+          TrAssignment(stmt.Tok, s.Lhs.Resolved, s.Rhs, builder, locals, etran);

+        }

       } else if (stmt is VarDecl) {

         AddComment(builder, stmt, "var-declaration statement");

         VarDecl s = (VarDecl)stmt;

@@ -3218,7 +3265,6 @@ namespace Microsoft.Dafny {
 

       } else if (stmt is ConcreteSyntaxStatement) {

         var s = (ConcreteSyntaxStatement)stmt;

-        // TODO: Update statements should perform multiple assignments in parallel!

         foreach (var ss in s.ResolvedStatements) {

           TrStmt(ss, builder, locals, etran);

         }

@@ -3490,7 +3536,7 @@ namespace Microsoft.Dafny {
       builder.Add(call);

       for (int i = 0; i < s.Lhs.Count; i++) {

         Bpl.IdentifierExpr tmpVarIdE = tmpOuts[i];

-        IdentifierExpr e = s.Lhs[i];

+        var e = (IdentifierExpr)s.Lhs[i];  // TODO: make this work also for non-IdentifierExpr LHSs!

         Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(e);  // TODO: is this cast always justified?

         if (tmpVarIdE != null) {

           // Instead of an assignment:

@@ -3888,96 +3934,205 @@ namespace Microsoft.Dafny {
       }

     }

 

-    void TrAssignment(IToken tok, Expression lhs, AssignmentRhs rhs, Bpl.StmtListBuilder builder, Bpl.VariableSeq locals,

-                      ExpressionTranslator etran)

+    void TrAssignment(IToken tok, Expression lhs, AssignmentRhs rhs,

+      Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran)

     {

       Contract.Requires(tok != null);

       Contract.Requires(lhs != null);

       Contract.Requires(!(lhs is ConcreteSyntaxExpression));

+      Contract.Requires(!(lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne));  // array-range assignments are handled elsewhere

       Contract.Requires(rhs != null);

       Contract.Requires(builder != null);

       Contract.Requires(cce.NonNullElements(locals));

       Contract.Requires(etran != null);

       Contract.Requires(predef != null);

 

-      TrStmt_CheckWellformed(lhs, builder, locals, etran, true);

+      List<AssignToLhs> lhsBuilder;

+      List<Bpl.IdentifierExpr> bLhss;

+      var lhss = new List<Expression>() { lhs.Resolved };

+      ProcessLhss(lhss, rhs.CanAffectPreviouslyKnownExpressions, builder, locals, etran,

+        out lhsBuilder, out bLhss);

+      Contract.Assert(lhsBuilder.Count == 1 && bLhss.Count == 1);  // guaranteed by postcondition of ProcessLhss

 

-      if (lhs is IdentifierExpr) {

-        var bLhs = (Bpl.IdentifierExpr)etran.TrExpr(lhs);  // TODO: is this cast always justified?

-        TrAssignmentRhs(tok, bLhs, lhs.Type, rhs, lhs.Type, builder, locals, etran);

+      var rhss = new List<AssignmentRhs>() { rhs };

+      ProcessRhss(lhsBuilder, bLhss, lhss, rhss, builder, locals, etran);

+    }

 

-      } else if (lhs is FieldSelectExpr) {

-        var fse = (FieldSelectExpr)lhs;

-        Contract.Assert(fse.Field != null);

-        var obj = SaveInTemp(etran.TrExpr(fse.Obj), rhs, "$obj", predef.RefType, builder, locals);

-        // check that the enclosing modifies clause allows this object to be written:  assert $_Frame[obj]);

-        builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, GetField(fse)), "assignment may update an object not in the enclosing method's modifies clause"));

+    void ProcessRhss(List<AssignToLhs> lhsBuilder, List<Bpl.IdentifierExpr/*may be null*/> bLhss,

+      List<Expression> lhss, List<AssignmentRhs> rhss,

+      Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran) {

+      Contract.Requires(lhsBuilder != null);

+      Contract.Requires(bLhss != null);

+      Contract.Requires(cce.NonNullElements(lhss));

+      Contract.Requires(cce.NonNullElements(rhss));

+      Contract.Requires(builder != null);

+      Contract.Requires(cce.NonNullElements(locals));

+      Contract.Requires(etran != null);

+      Contract.Requires(predef != null);

 

-        Bpl.Expr bRhs = TrAssignmentRhs(tok, null, fse.Field.Type, rhs, lhs.Type, builder, locals, etran);

+      var finalRhss = new List<Bpl.IdentifierExpr>();

+      for (int i = 0; i < lhss.Count; i++) {

+        var lhs = lhss[i];

+        // the following assumes are part of the precondition, really

+        Contract.Assume(!(lhs is ConcreteSyntaxExpression));

+        Contract.Assume(!(lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne));  // array-range assignments are handled elsewhere

+

+        Type lhsType = null;

+        if (lhs is IdentifierExpr) {

+          lhsType = lhs.Type;

+        } else if (lhs is FieldSelectExpr) {

+          var fse = (FieldSelectExpr)lhs;

+          lhsType = fse.Field.Type;

+        }

+        var bRhs = TrAssignmentRhs(rhss[i].Tok, bLhss[i], lhsType, rhss[i], lhs.Type, builder, locals, etran);

+        if (bRhs != bLhss[i]) {

+          finalRhss.Add(bRhs);

+        } else {

+          // assignment has already been done by by TrAssignmentRhs

+          finalRhss.Add(null);

+        }

+      }

+      for (int i = 0; i < lhss.Count; i++) {

+        if (finalRhss[i] != null) {

+          lhsBuilder[i](finalRhss[i], builder, etran);

+        }

+      }

+    }

 

-        var h = (Bpl.IdentifierExpr)etran.HeapExpr;  // TODO: is this cast always justified?

-        Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, ExpressionTranslator.UpdateHeap(tok, h, obj, new Bpl.IdentifierExpr(tok, GetField(fse.Field)), bRhs));

-        builder.Add(cmd);

-        // assume $IsGoodHeap($Heap);

-        builder.Add(AssumeGoodHeap(tok, etran));

+    delegate void AssignToLhs(Bpl.Expr rhs, Bpl.StmtListBuilder builder, ExpressionTranslator etran);

 

-      } else if (lhs is SeqSelectExpr) {

-        SeqSelectExpr sel = (SeqSelectExpr)lhs;

-        Contract.Assert(sel.Seq.Type != null && sel.Seq.Type.IsArrayType);

-        if (sel.SelectOne) {

+    /// <summary>

+    /// Creates a list of protected Boogie LHSs for the given Dafny LHSs.  Along the way,

+    /// builds code that checks that the LHSs are well-defined, denote different locations,

+    /// and are allowed by the enclosing modifies clause.

+    /// </summary>

+    List<AssignToLhs> ProcessLhss(List<Expression> lhss, bool rhsCanAffectPreviouslyKnownExpressions,

+      Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran,

+      out List<AssignToLhs> lhsBuilders, out List<Bpl.IdentifierExpr/*may be null*/> bLhss) {

+      Contract.Requires(cce.NonNullElements(lhss));

+      // Contract.Requires(rhs != null);

+      Contract.Requires(builder != null);

+      Contract.Requires(cce.NonNullElements(locals));

+      Contract.Requires(etran != null);

+      Contract.Requires(predef != null);

+      Contract.Ensures(Contract.ValueAtReturn(out lhsBuilders).Count == lhss.Count);

+      Contract.Ensures(Contract.ValueAtReturn(out lhsBuilders).Count == Contract.ValueAtReturn(out bLhss).Count);

+

+      rhsCanAffectPreviouslyKnownExpressions = rhsCanAffectPreviouslyKnownExpressions || lhss.Count != 1;

+

+      // for each Dafny LHS, build a protected Boogie LHS for the eventual assignment

+      lhsBuilders = new List<AssignToLhs>();

+      bLhss = new List<Bpl.IdentifierExpr>();

+      var prevObj = new Bpl.Expr[lhss.Count];

+      var prevIndex = new Bpl.Expr[lhss.Count];

+      int i = 0;

+      foreach (var lhs in lhss) {

+        Contract.Assume(!(lhs is ConcreteSyntaxExpression));

+        IToken tok = lhs.tok;

+        TrStmt_CheckWellformed(lhs, builder, locals, etran, true);

+

+        if (lhs is IdentifierExpr) {

+          var bLhs = (Bpl.IdentifierExpr)etran.TrExpr(lhs);  // TODO: is this cast always justified?

+          // Note, the resolver checks for duplicate IdentifierExpr's in LHSs

+          bLhss.Add(rhsCanAffectPreviouslyKnownExpressions ? null : bLhs);

+          lhsBuilders.Add(delegate(Bpl.Expr rhs, Bpl.StmtListBuilder bldr, ExpressionTranslator et) {

+            builder.Add(Bpl.Cmd.SimpleAssign(tok, bLhs, rhs));

+          });

+

+        } else if (lhs is FieldSelectExpr) {

+          var fse = (FieldSelectExpr)lhs;

+          Contract.Assert(fse.Field != null);

+          var obj = SaveInTemp(etran.TrExpr(fse.Obj), rhsCanAffectPreviouslyKnownExpressions,

+            "$obj" + i, predef.RefType, builder, locals);

+          prevObj[i] = obj;

+          // check that the enclosing modifies clause allows this object to be written:  assert $_Frame[obj]);

+          builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, GetField(fse)), "assignment may update an object not in the enclosing method's modifies clause"));

+

+          // check that this LHS is not the same as any previous LHSs

+          for (int j = 0; j < i; j++) {

+            var prev = lhss[j] as FieldSelectExpr;

+            if (prev != null && prev.Field == fse.Field) {

+              builder.Add(Assert(tok, Bpl.Expr.Neq(prevObj[j], obj), string.Format("left-hand sides {0} and {1} may refer to the same location", j, i)));

+            }

+          }

+

+          bLhss.Add(null);

+          lhsBuilders.Add(delegate(Bpl.Expr rhs, Bpl.StmtListBuilder bldr, ExpressionTranslator et) {

+            var h = (Bpl.IdentifierExpr)et.HeapExpr;  // TODO: is this cast always justified?

+            Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, ExpressionTranslator.UpdateHeap(tok, h, obj, new Bpl.IdentifierExpr(tok, GetField(fse.Field)), rhs));

+            builder.Add(cmd);

+            // assume $IsGoodHeap($Heap);

+            builder.Add(AssumeGoodHeap(tok, et));

+          });

+

+        } else if (lhs is SeqSelectExpr) {

+          SeqSelectExpr sel = (SeqSelectExpr)lhs;

+          Contract.Assert(sel.SelectOne);  // array-range assignments are handled elsewhere, see precondition

+          Contract.Assert(sel.Seq.Type != null && sel.Seq.Type.IsArrayType);

           Contract.Assert(sel.E0 != null);

-          var obj = SaveInTemp(etran.TrExpr(sel.Seq), rhs, "$obj", predef.RefType, builder, locals);

-          var fieldName = SaveInTemp(FunctionCall(tok, BuiltinFunction.IndexField, null, etran.TrExpr(sel.E0)), rhs, "$index", predef.FieldName(tok, predef.BoxType), builder, locals);

+          var obj = SaveInTemp(etran.TrExpr(sel.Seq), rhsCanAffectPreviouslyKnownExpressions,

+            "$obj" + i, predef.RefType, builder, locals);

+          var fieldName = SaveInTemp(FunctionCall(tok, BuiltinFunction.IndexField, null, etran.TrExpr(sel.E0)), rhsCanAffectPreviouslyKnownExpressions,

+            "$index" + i, predef.FieldName(tok, predef.BoxType), builder, locals);

+          prevObj[i] = obj;

+          prevIndex[i] = fieldName;

           // check that the enclosing modifies clause allows this object to be written:  assert $_Frame[obj,index]);

           builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing method's modifies clause"));

 

-          Bpl.Expr bRhs = TrAssignmentRhs(tok, null, null, rhs, lhs.Type, builder, locals, etran);

+          // check that this LHS is not the same as any previous LHSs

+          for (int j = 0; j < i; j++) {

+            var prev = lhss[j] as SeqSelectExpr;

+            if (prev != null) {

+              builder.Add(Assert(tok,

+                Bpl.Expr.Or(Bpl.Expr.Neq(prevObj[j], obj), Bpl.Expr.Neq(prevIndex[j], fieldName)),

+                string.Format("left-hand sides {0} and {1} may refer to the same location", j, i)));

+            }

+          }

 

-          var h = (Bpl.IdentifierExpr)etran.HeapExpr;  // TODO: is this cast always justified?

-          Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, ExpressionTranslator.UpdateHeap(tok, h, obj, fieldName, bRhs));

-          builder.Add(cmd);

-          // assume $IsGoodHeap($Heap);

-          builder.Add(AssumeGoodHeap(tok, etran));

+          bLhss.Add(null);

+          lhsBuilders.Add(delegate(Bpl.Expr rhs, Bpl.StmtListBuilder bldr, ExpressionTranslator et) {

+            var h = (Bpl.IdentifierExpr)et.HeapExpr;  // TODO: is this cast always justified?

+            Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, ExpressionTranslator.UpdateHeap(tok, h, obj, fieldName, rhs));

+            builder.Add(cmd);

+            // assume $IsGoodHeap($Heap);

+            builder.Add(AssumeGoodHeap(tok, et));

+          });

 

         } else {

-          var obj = etran.TrExpr(sel.Seq);

-          Bpl.Expr low = sel.E0 == null ? Bpl.Expr.Literal(0) : etran.TrExpr(sel.E0);

-          Bpl.Expr high = sel.E1 == null ? ArrayLength(tok, obj, 1, 0) : etran.TrExpr(sel.E1);

-          // check frame:

-          // assert (forall i: int :: low <= i && i < high ==> $_Frame[arr,i]);

-          Bpl.Variable iVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$i", Bpl.Type.Int));

-          Bpl.IdentifierExpr ie = new Bpl.IdentifierExpr(tok, iVar);

-          Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Le(low, ie), Bpl.Expr.Lt(ie, high));

-          Bpl.Expr fieldName = FunctionCall(tok, BuiltinFunction.IndexField, null, ie);

-          Bpl.Expr cons = Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName);

-          Bpl.Expr q = new Bpl.ForallExpr(tok, new Bpl.VariableSeq(iVar), Bpl.Expr.Imp(ante, cons));

-          builder.Add(Assert(tok, q, "assignment may update an array element not in the enclosing method's modifies clause"));

-          // compute the RHS

-          Bpl.Expr bRhs = TrAssignmentRhs(tok, null, null, rhs, lhs.Type, builder, locals, etran);

-          // do the update:  call UpdateArrayRange(arr, low, high, rhs);

-          builder.Add(new Bpl.CallCmd(tok, "UpdateArrayRange",

-            new Bpl.ExprSeq(obj, low, high, bRhs),

-            new Bpl.IdentifierExprSeq()));

-        }

-

-      } else {

-        MultiSelectExpr mse = (MultiSelectExpr)lhs;

-        Contract.Assert(mse.Array.Type != null && mse.Array.Type.IsArrayType);

+          MultiSelectExpr mse = (MultiSelectExpr)lhs;

+          Contract.Assert(mse.Array.Type != null && mse.Array.Type.IsArrayType);

+

+          var obj = SaveInTemp(etran.TrExpr(mse.Array), rhsCanAffectPreviouslyKnownExpressions,

+            "$obj" + i, predef.RefType, builder, locals);

+          var fieldName = SaveInTemp(etran.GetArrayIndexFieldName(mse.tok, mse.Indices), rhsCanAffectPreviouslyKnownExpressions, 

+            "$index" + i, predef.FieldName(mse.tok, predef.BoxType), builder, locals);

+          prevObj[i] = obj;

+          prevIndex[i] = fieldName;

+          builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing method's modifies clause"));

 

-        var obj = SaveInTemp(etran.TrExpr(mse.Array), rhs, "$obj", predef.RefType, builder, locals);

-        var fieldName = SaveInTemp(etran.GetArrayIndexFieldName(mse.tok, mse.Indices), rhs, "$index", predef.FieldName(mse.tok, predef.BoxType), builder, locals);

-        builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing method's modifies clause"));

+          // check that this LHS is not the same as any previous LHSs

+          for (int j = 0; j < i; j++) {

+            var prev = lhss[j] as SeqSelectExpr;

+            if (prev != null) {

+              builder.Add(Assert(tok,

+                Bpl.Expr.Or(Bpl.Expr.Neq(prevObj[j], obj), Bpl.Expr.Neq(prevIndex[j], fieldName)),

+                string.Format("left-hand sides {0} and {1} may refer to the same location", j, i)));

+            }

+          }

 

-        Bpl.Expr bRhs = TrAssignmentRhs(tok, null, null, rhs, lhs.Type, builder, locals, etran);

+          bLhss.Add(null);

+          lhsBuilders.Add(delegate(Bpl.Expr rhs, Bpl.StmtListBuilder bldr, ExpressionTranslator et) {

+            var h = (Bpl.IdentifierExpr)et.HeapExpr;  // TODO: is this cast always justified?

+            Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, ExpressionTranslator.UpdateHeap(tok, h, obj, fieldName, rhs));

+            builder.Add(cmd);

+            // assume $IsGoodHeap($Heap);

+            builder.Add(AssumeGoodHeap(tok, etran));

+          });

+        }

 

-        var h = (Bpl.IdentifierExpr)etran.HeapExpr;  // TODO: is this cast always justified?

-        Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, ExpressionTranslator.UpdateHeap(tok, h, obj, fieldName, bRhs));

-        builder.Add(cmd);

-        // assume $IsGoodHeap($Heap);

-        builder.Add(AssumeGoodHeap(tok, etran));

+        i++;

       }

-

-      builder.Add(CaptureState(tok));

+      return lhsBuilders;

     }

 

     /// <summary>

@@ -3990,6 +4145,7 @@ namespace Microsoft.Dafny {
                                        Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran) {

       Contract.Requires(tok != null);

       Contract.Requires(rhs != null);

+      Contract.Requires(!(rhs is CallRhs));  // calls are handled in a different translation method

       Contract.Requires(builder != null);

       Contract.Requires(cce.NonNullElements(locals));

       Contract.Requires(etran != null);

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index c82d3803..75025b2f 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -85,7 +85,7 @@ TypeTests.dfy(87,8): Error: sorry, cannot instantiate 'array' type with a subran
 NatTypes.dfy(7,5): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon0

-NatTypes.dfy(31,5): Error: value assigned to a nat must be non-negative

+NatTypes.dfy(31,10): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon0

     NatTypes.dfy(19,3): anon10_LoopHead

@@ -111,7 +111,7 @@ Execution trace:
     (0,0): anon0

     (0,0): anon5_Else

     (0,0): anon6_Then

-NatTypes.dfy(86,16): Error: value assigned to a nat must be non-negative

+NatTypes.dfy(86,19): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

@@ -450,7 +450,7 @@ ParseErrors.dfy(18,18): error: chaining not allowed from the previous operator
 9 parse errors detected in ParseErrors.dfy

 

 -------------------- Array.dfy --------------------

-Array.dfy(10,12): Error: assignment may update an array element not in the enclosing method's modifies clause

+Array.dfy(10,8): Error: assignment may update an array element not in the enclosing method's modifies clause

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

@@ -465,13 +465,13 @@ Execution trace:
 Array.dfy(48,20): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Array.dfy(56,12): Error: assignment may update an array element not in the enclosing method's modifies clause

+Array.dfy(56,8): Error: assignment may update an array element not in the enclosing method's modifies clause

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

     (0,0): anon2

     (0,0): anon6_Then

-Array.dfy(63,12): Error: assignment may update an array element not in the enclosing method's modifies clause

+Array.dfy(63,8): Error: assignment may update an array element not in the enclosing method's modifies clause

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

@@ -490,10 +490,10 @@ Execution trace:
     (0,0): anon7_Else

     (0,0): anon8_Then

     (0,0): anon9_Then

-Array.dfy(131,10): Error: assignment may update an array element not in the enclosing method's modifies clause

+Array.dfy(131,6): Error: assignment may update an array element not in the enclosing method's modifies clause

 Execution trace:

     (0,0): anon0

-Array.dfy(138,10): Error: assignment may update an array element not in the enclosing method's modifies clause

+Array.dfy(138,6): Error: assignment may update an array element not in the enclosing method's modifies clause

 Execution trace:

     (0,0): anon0

 

@@ -598,8 +598,31 @@ Execution trace:
     (0,0): anon10

     Basics.dfy(66,95): anon18_Else

     (0,0): anon12

+Basics.dfy(86,16): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon10_Then

+Basics.dfy(99,12): Error: left-hand sides 0 and 1 may refer to the same location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3

+    (0,0): anon11_Else

+    (0,0): anon6

+    (0,0): anon12_Then

+Basics.dfy(105,10): Error: left-hand sides 0 and 1 may refer to the same location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon10_Then

+    (0,0): anon3

+    (0,0): anon11_Then

+    (0,0): anon6

+    (0,0): anon12_Then

+    (0,0): anon9

+Basics.dfy(119,10): Error: left-hand sides 0 and 1 may refer to the same location

+Execution trace:

+    (0,0): anon0

 

-Dafny program verifier finished with 7 verified, 2 errors

+Dafny program verifier finished with 9 verified, 6 errors

 

 -------------------- ControlStructures.dfy --------------------

 ControlStructures.dfy(5,3): Error: missing case in case statement: Blue

@@ -638,112 +661,112 @@ ControlStructures.dfy(72,3): Error: alternative cases fail to cover all possibil
 Execution trace:

     (0,0): anon0

     (0,0): anon5_Else

-ControlStructures.dfy(218,18): Error: assertion violation

+ControlStructures.dfy(215,18): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    ControlStructures.dfy(197,3): anon62_LoopHead

+    ControlStructures.dfy(194,3): anon62_LoopHead

     (0,0): anon62_LoopBody

-    ControlStructures.dfy(197,3): anon63_Else

+    ControlStructures.dfy(194,3): anon63_Else

     (0,0): anon3

-    ControlStructures.dfy(197,3): anon64_Else

+    ControlStructures.dfy(194,3): anon64_Else

     (0,0): anon5

-    ControlStructures.dfy(201,5): anon65_LoopHead

+    ControlStructures.dfy(198,5): anon65_LoopHead

     (0,0): anon65_LoopBody

-    ControlStructures.dfy(201,5): anon66_Else

+    ControlStructures.dfy(198,5): anon66_Else

     (0,0): anon8

-    ControlStructures.dfy(201,5): anon67_Else

+    ControlStructures.dfy(198,5): anon67_Else

     (0,0): anon10

     (0,0): anon71_Then

-    ControlStructures.dfy(213,9): anon72_LoopHead

+    ControlStructures.dfy(210,9): anon72_LoopHead

     (0,0): anon72_LoopBody

-    ControlStructures.dfy(213,9): anon73_Else

+    ControlStructures.dfy(210,9): anon73_Else

     (0,0): anon20

     (0,0): anon74_Then

     (0,0): anon29

-ControlStructures.dfy(235,21): Error: assertion violation

+ControlStructures.dfy(232,21): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    ControlStructures.dfy(197,3): anon62_LoopHead

+    ControlStructures.dfy(194,3): anon62_LoopHead

     (0,0): anon62_LoopBody

-    ControlStructures.dfy(197,3): anon63_Else

+    ControlStructures.dfy(194,3): anon63_Else

     (0,0): anon3

-    ControlStructures.dfy(197,3): anon64_Else

+    ControlStructures.dfy(194,3): anon64_Else

     (0,0): anon5

-    ControlStructures.dfy(201,5): anon65_LoopHead

+    ControlStructures.dfy(198,5): anon65_LoopHead

     (0,0): anon65_LoopBody

-    ControlStructures.dfy(201,5): anon66_Else

+    ControlStructures.dfy(198,5): anon66_Else

     (0,0): anon8

-    ControlStructures.dfy(201,5): anon67_Else

+    ControlStructures.dfy(198,5): anon67_Else

     (0,0): anon10

     (0,0): anon71_Then

-    ControlStructures.dfy(213,9): anon72_LoopHead

+    ControlStructures.dfy(210,9): anon72_LoopHead

     (0,0): anon72_LoopBody

-    ControlStructures.dfy(213,9): anon73_Else

+    ControlStructures.dfy(210,9): anon73_Else

     (0,0): anon20

-    ControlStructures.dfy(213,9): anon74_Else

+    ControlStructures.dfy(210,9): anon74_Else

     (0,0): anon22

     (0,0): anon75_Then

     (0,0): after_4

-    ControlStructures.dfy(224,7): anon77_LoopHead

+    ControlStructures.dfy(221,7): anon77_LoopHead

     (0,0): anon77_LoopBody

-    ControlStructures.dfy(224,7): anon78_Else

+    ControlStructures.dfy(221,7): anon78_Else

     (0,0): anon33

-    ControlStructures.dfy(224,7): anon79_Else

+    ControlStructures.dfy(221,7): anon79_Else

     (0,0): anon35

     (0,0): anon81_Then

     (0,0): anon38

     (0,0): after_9

     (0,0): anon86_Then

     (0,0): anon53

-ControlStructures.dfy(238,30): Error: assertion violation

+ControlStructures.dfy(235,30): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    ControlStructures.dfy(197,3): anon62_LoopHead

+    ControlStructures.dfy(194,3): anon62_LoopHead

     (0,0): anon62_LoopBody

-    ControlStructures.dfy(197,3): anon63_Else

+    ControlStructures.dfy(194,3): anon63_Else

     (0,0): anon3

-    ControlStructures.dfy(197,3): anon64_Else

+    ControlStructures.dfy(194,3): anon64_Else

     (0,0): anon5

-    ControlStructures.dfy(201,5): anon65_LoopHead

+    ControlStructures.dfy(198,5): anon65_LoopHead

     (0,0): anon65_LoopBody

-    ControlStructures.dfy(201,5): anon66_Else

+    ControlStructures.dfy(198,5): anon66_Else

     (0,0): anon8

-    ControlStructures.dfy(201,5): anon67_Else

+    ControlStructures.dfy(198,5): anon67_Else

     (0,0): anon10

     (0,0): anon68_Then

     (0,0): after_5

     (0,0): anon87_Then

     (0,0): anon88_Then

     (0,0): anon58

-ControlStructures.dfy(241,17): Error: assertion violation

+ControlStructures.dfy(238,17): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    ControlStructures.dfy(197,3): anon62_LoopHead

+    ControlStructures.dfy(194,3): anon62_LoopHead

     (0,0): anon62_LoopBody

-    ControlStructures.dfy(197,3): anon63_Else

+    ControlStructures.dfy(194,3): anon63_Else

     (0,0): anon3

-    ControlStructures.dfy(197,3): anon64_Else

+    ControlStructures.dfy(194,3): anon64_Else

     (0,0): anon5

-    ControlStructures.dfy(201,5): anon65_LoopHead

+    ControlStructures.dfy(198,5): anon65_LoopHead

     (0,0): anon65_LoopBody

-    ControlStructures.dfy(201,5): anon66_Else

+    ControlStructures.dfy(198,5): anon66_Else

     (0,0): anon8

-    ControlStructures.dfy(201,5): anon67_Else

+    ControlStructures.dfy(198,5): anon67_Else

     (0,0): anon10

     (0,0): anon71_Then

-    ControlStructures.dfy(213,9): anon72_LoopHead

+    ControlStructures.dfy(210,9): anon72_LoopHead

     (0,0): anon72_LoopBody

-    ControlStructures.dfy(213,9): anon73_Else

+    ControlStructures.dfy(210,9): anon73_Else

     (0,0): anon20

-    ControlStructures.dfy(213,9): anon74_Else

+    ControlStructures.dfy(210,9): anon74_Else

     (0,0): anon22

     (0,0): anon75_Then

     (0,0): after_4

-    ControlStructures.dfy(224,7): anon77_LoopHead

+    ControlStructures.dfy(221,7): anon77_LoopHead

     (0,0): anon77_LoopBody

-    ControlStructures.dfy(224,7): anon78_Else

+    ControlStructures.dfy(221,7): anon78_Else

     (0,0): anon33

-    ControlStructures.dfy(224,7): anon79_Else

+    ControlStructures.dfy(221,7): anon79_Else

     (0,0): anon35

     (0,0): anon82_Then

     (0,0): anon85_Then

diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy
index 16fd7d87..b9ba5102 100644
--- a/Test/dafny0/Basics.dfy
+++ b/Test/dafny0/Basics.dfy
@@ -65,3 +65,56 @@ method ChallengeTruth(j: int, k: int)
   // but this is not equally true:

   assert j <= j + k != k + j + 1 < k+k+j <=/*this is the error*/ j+j+k < k+k+j+j == 2*k + 2*j == 2*(k+j);

 }

+

+// --------- multi assignments --------------------------------

+

+class Multi {

+  var x: int;

+  var y: int;

+}

+

+method TestMulti(m: Multi, p: Multi)

+  requires m != null && p != null;

+  modifies m, p;

+{

+  m.x := 10;

+  m.y := 12;

+  p.x := 20;

+  p.y := 22;

+  if (*) {

+    assert p.x == 20;

+    assert m.x == 10;  // error: m and p may be the same

+  }

+  var t, u;

+  u, m.x, t := 100, u + t + m.x, 200;

+  m.x := 0;

+  u, m.x, t := 200, u + t + m.x, 400;

+  assert m.x == 300;

+  if (p.x != 300) {

+    p.x, m.x := m.x, p.x;

+  }

+  assert p.x == 300;

+  if (*) {

+    p.x, m.y := 10, 10;

+    p.x, m.x := 8, 8;  // error: duplicate assignment (since m and p may be the same)

+  }

+

+  var a, b := new int[20], new int[30];

+  a[4], b[10], a[0], a[3], b[18] := 0, 1, 2, 3, 4;

+  a[4], b[b[18]] := 271, 272;

+  a[4], a[b[18]] := 273, 274;  // error: duplicate assignment (since b[18] is 4)

+}

+

+class MyBoxyClass<T> {

+  var f: T;

+}

+

+method TestBoxAssignment<T>(x: MyBoxyClass<int>, y: MyBoxyClass<T>, t: T)

+  requires x != null && y != null;

+  modifies x, y;

+{

+  y.f := t;

+  x.f := 15;

+  // all together now:

+  y.f, x.f := t, 15;  // error: duplicate assignment (if T==int and x==y)

+}

diff --git a/Test/dafny0/ControlStructures.dfy b/Test/dafny0/ControlStructures.dfy
index 5012e003..c46eee3a 100644
--- a/Test/dafny0/ControlStructures.dfy
+++ b/Test/dafny0/ControlStructures.dfy
@@ -96,8 +96,7 @@ method DutchFlag(A: array<int>, N: int, l: int, r: int) returns (result: int)
   var pv := A[l];

   var i := l;

   var j := r-1;

-  // swap A[l] and A[j]

-  var tmp := A[l]; A[l] := A[j]; A[j] := tmp;

+  A[l], A[j] := A[j], A[l];

 

   while (i < j)

     invariant l <= i && i <= j && j < r;

@@ -110,11 +109,9 @@ method DutchFlag(A: array<int>, N: int, l: int, r: int) returns (result: int)
       case pv <= A[j-1] =>

         j := j - 1;

       case A[j-1] < pv && pv < A[i] =>

-        // swap A[j-1] and A[i]

-        tmp := A[i]; A[i] := A[j-1]; A[j-1] := tmp;

+        A[j-1], A[i] := A[i], A[j-1];

         assert A[i] < pv && pv < A[j-1];

-        i := i + 1;

-        j := j - 1;

+        i, j := i + 1, j - 1;

     }

   }

   result := i;

diff --git a/Test/dafny1/MatrixFun.dfy b/Test/dafny1/MatrixFun.dfy
index 81b3f4c9..5c69ac50 100644
--- a/Test/dafny1/MatrixFun.dfy
+++ b/Test/dafny1/MatrixFun.dfy
@@ -24,9 +24,7 @@ method MirrorImage<T>(m: array2<T>)
       invariant (forall i,j :: a+1 <= i && i < m.Length0 && 0 <= j && j < m.Length1 ==>

                   m[i,j] == old(m[i,j]));

     {

-      var tmp := m[a, m.Length1-1-b];

-      m[a, m.Length1-1-b] := m[a, b];

-      m[a, b] := tmp;

+      m[a, m.Length1-1-b], m[a, b] := m[a, b], m[a, m.Length1-1-b];

       b := b + 1;

     }

     a := a + 1;

@@ -50,7 +48,7 @@ method Flip<T>(m: array2<T>)
     decreases N-a, N-b;

   {

     if (b < N) {

-      var tmp := m[a,b];  m[a,b] := m[b,a];  m[b,a] := tmp;

+      m[a,b], m[b,a] := m[b,a], m[a,b];

       b := b + 1;

     } else {

       a := a + 1;  b := a;

diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy
index 6e19ab8f..49f6b909 100644
--- a/Test/dafny1/PriorityQueue.dfy
+++ b/Test/dafny1/PriorityQueue.dfy
@@ -62,7 +62,7 @@ class PriorityQueue {
       if (a[i/2] <= a[i]) {

         return;

       }

-      var tmp := a[i];  a[i] := a[i/2];  a[i/2] := tmp;

+      a[i/2], a[i] := a[i], a[i/2];

       i := i / 2;

     }

   }

@@ -104,7 +104,7 @@ class PriorityQueue {
       if (a[i] <= a[smallestChild]) {

         return;

       }

-      var tmp := a[i];  a[i] := a[smallestChild];  a[smallestChild] := tmp;

+      a[smallestChild], a[i] := a[i], a[smallestChild];

       i := smallestChild;

       assert 1 <= i/2/2 ==> a[i/2/2] <= a[i];

     }

@@ -175,7 +175,7 @@ class PriorityQueue_Alternative {
       if (a[i/2] <= a[i]) {

         return;

       }

-      var tmp := a[i];  a[i] := a[i/2];  a[i/2] := tmp;

+      a[i/2], a[i] := a[i], a[i/2];

       i := i / 2;

     }

   }

@@ -213,7 +213,7 @@ class PriorityQueue_Alternative {
       if (a[i] <= a[smallestChild]) {

         return;

       }

-      var tmp := a[i];  a[i] := a[smallestChild];  a[smallestChild] := tmp;

+      a[smallestChild], a[i] := a[i], a[smallestChild];

       i := smallestChild;

       assert 1 <= i/2/2 ==> a[i/2/2] <= a[i];

     }