Dafny: changed iterator body to resolve to implicit fields rather than to the formal in- and yield-parameters

6 files changed, 164 insertions, 196 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 277cb282..fb47f020 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1163,8 +1163,8 @@ namespace Microsoft.Dafny {
   {

     public readonly List<Formal> Ins;

     public readonly List<Formal> Outs;

-    public readonly List<Formal> OutsHistory;  // these are the 'xs' variables

-    public readonly List<Formal> ExtraVars;  // _reads, _modifies, _new

+    public readonly List<Field> OutsFields;

+    public readonly List<Field> OutsHistoryFields;  // these are the 'xs' variables

     public readonly List<Field> DecreasesFields;  // filled in during resolution

     public readonly Specification<FrameExpression> Reads;

     public readonly Specification<FrameExpression> Modifies;

@@ -1214,18 +1214,8 @@ namespace Microsoft.Dafny {
       Body = body;

       SignatureIsOmitted = signatureIsOmitted;

 

-      OutsHistory = new List<Formal>();

-      foreach (var p in Outs) {

-        var tp = p.Type;

-        if (tp.IsSubrangeType) {

-          tp = new IntType();  // because SeqType(NatType) is now allowed (despite the fact that the history variable is readonly, which is unfortunate)

-        }

-        OutsHistory.Add(new Formal(p.tok, p.Name + "s", new SeqType(tp), false, true));

-      }

-      ExtraVars = new List<Formal>();

-      ExtraVars.Add(new Formal(tok, "_reads", new SetType(new ObjectType()), true, true));

-      ExtraVars.Add(new Formal(tok, "_modifies", new SetType(new ObjectType()), true, true));

-      ExtraVars.Add(new Formal(tok, "_new", new SetType(new ObjectType()), false, true));

+      OutsFields = new List<Field>();

+      OutsHistoryFields = new List<Field>();

       DecreasesFields = new List<Field>();

     }

 

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 8f005368..dc49013d 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -520,30 +520,36 @@ namespace Microsoft.Dafny
             if (members.ContainsKey(p.Name)) {

               Error(p, "Name of yield-parameter is used by another member of the iterator: {0}", p.Name);

             } else {

-              var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", p.IsGhost, true, false, p.Type, null);

+              var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", p.IsGhost, true, true, p.Type, null);

               field.EnclosingClass = iter;  // resolve here

+              iter.OutsFields.Add(field);

               members.Add(p.Name, field);

               iter.Members.Add(field);

             }

           }

-          var yieldHistoryVariables = new List<MemberDecl>();

-          foreach (var p in iter.OutsHistory) {

-            if (members.ContainsKey(p.Name)) {

+          foreach (var p in iter.Outs) {

+            var nm = p.Name + "s";

+            if (members.ContainsKey(nm)) {

               Error(p.tok, "Name of implicit yield-history variable '{0}' is already used by another member of the iterator", p.Name);

             } else {

-              var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", true, true, false, p.Type, null);

+              var tp = new SeqType(p.Type.IsSubrangeType ? new IntType() : p.Type);

+              var field = new SpecialField(p.tok, nm, nm, "", "", true, true, false, tp, null);

               field.EnclosingClass = iter;  // resolve here

-              yieldHistoryVariables.Add(field);  // just record this field for now (until all parameters have been added as members)

+              iter.OutsHistoryFields.Add(field);  // for now, just record this field (until all parameters have been added as members)

             }

           }

-          // now that already-used 'xs' names have been checked for, add these yield-history variables

-          yieldHistoryVariables.ForEach(f => {

+          // now that already-used 'ys' names have been checked for, add these yield-history variables

+          iter.OutsHistoryFields.ForEach(f => {

             members.Add(f.Name, f);

             iter.Members.Add(f);

           });

           // add the additional special variables as fields

-          foreach (var p in iter.ExtraVars) {

-            var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", p.IsGhost, !p.InParam, false, p.Type, null);

+          foreach (var p in new List<Tuple<string, bool>>() {

+            new Tuple<string, bool>("_reads", false),

+            new Tuple<string, bool>("_modifies", false),

+            new Tuple<string, bool>("_new", true) })

+          {

+            var field = new SpecialField(iter.tok, p.Item1, p.Item1, "", "", true, p.Item2, p.Item2, new SetType(new ObjectType()), null);

             field.EnclosingClass = iter;  // resolve here

             members.Add(field.Name, field);

             iter.Members.Add(field);

@@ -562,9 +568,9 @@ namespace Microsoft.Dafny
             var nm = "_decreases" + i;

             var field = new SpecialField(p.tok, nm, nm, "", "", true, false, false, new InferredTypeProxy(), null);

             field.EnclosingClass = iter;  // resolve here

+            iter.DecreasesFields.Add(field);

             members.Add(field.Name, field);

             iter.Members.Add(field);

-            iter.DecreasesFields.Add(field);

             i++;

           }

 

@@ -2516,25 +2522,12 @@ namespace Microsoft.Dafny
         Error(iter, "iterator signature can be omitted only in refining methods");

       }

       var defaultTypeArguments = iter.TypeArgs.Count == 0 ? iter.TypeArgs : null;

-      // resolve in-parameters

-      foreach (Formal p in iter.Ins) {

-        if (!scope.Push(p.Name, p)) {

-          Error(p, "Duplicate parameter name: {0}", p.Name);

-        }

+      // resolve the types of the parameters

+      foreach (var p in iter.Ins.Concat(iter.Outs)) {

         ResolveType(p.tok, p.Type, defaultTypeArguments, true);

       }

-      // resolve yield-parameters

-      foreach (Formal p in iter.Outs) {

-        if (!scope.Push(p.Name, p)) {

-          Error(p, "Duplicate parameter name: {0}", p.Name);

-        }

-        ResolveType(p.tok, p.Type, defaultTypeArguments, true);

-      }

-      // resolve yield-history variables

-      foreach (Formal p in iter.OutsHistory) {

-        if (!scope.Push(p.Name, p)) {

-          Error(p, "Name conflict with yield-history variable: {0}", p.Name);

-        }

+      // resolve the types of the added fields (in case some of these types would cause the addition of default type arguments)

+      foreach (var p in iter.OutsHistoryFields) {

         ResolveType(p.tok, p.Type, defaultTypeArguments, true);

       }

       scope.PopMarker();

@@ -2545,6 +2538,8 @@ namespace Microsoft.Dafny
     /// </summary>

     void ResolveIterator(IteratorDecl iter) {

       Contract.Requires(iter != null);

+      Contract.Requires(currentClass == null);

+      Contract.Ensures(currentClass == null);

 

       var initialErrorCount = ErrorCount;

 

@@ -2554,6 +2549,20 @@ namespace Microsoft.Dafny
       iter.Ins.ForEach(p => scope.Push(p.Name, p));

 

       // Start resolving specification...

+      // we start with the decreases clause, because the _decreases<n> fields were only given type proxies before; we'll know

+      // the types only after resolving the decreases clause (and it may be that some of resolution has already seen uses of

+      // these fields; so, with no further ado, here we go

+      Contract.Assert(iter.Decreases.Expressions.Count == iter.DecreasesFields.Count);

+      for (int i = 0; i < iter.Decreases.Expressions.Count; i++) {

+        var e = iter.Decreases.Expressions[i];

+        ResolveExpression(e, false);

+        // any type is fine, but associate this type with the corresponding _decreases<n> field

+        var d = iter.DecreasesFields[i];

+        if (!UnifyTypes(d.Type, e.Type)) {

+          // bummer, there was a use--and a bad use--of the field before, so this won't be the best of error messages

+          Error(e, "type of field {0} is {1}, but has been constrained elsewhere to be of type {2}", d.Name, e.Type, d.Type);

+        }

+      }

       foreach (FrameExpression fe in iter.Reads.Expressions) {

         ResolveFrameExpression(fe, "reads");

       }

@@ -2567,19 +2576,14 @@ namespace Microsoft.Dafny
           Error(e.E, "Precondition must be a boolean (got {0})", e.E.Type);

         }

       }

-      Contract.Assert(iter.Decreases.Expressions.Count == iter.DecreasesFields.Count);

-      for (int i = 0; i < iter.Decreases.Expressions.Count; i++) {

-        var e = iter.Decreases.Expressions[i];

-        ResolveExpression(e, false);

-        // any type is fine, but associate this type with the corresponding _decreases<n> field

-        var d = iter.DecreasesFields[i];

-        if (!UnifyTypes(d.Type, e.Type)) {

-          Error(e, "type of field {0} is {1}, but has been constrained elsewhere to be of type {2}", d.Name, e.Type, d.Type);

-        }

-      }

 

-      // Now add the yield-history variables to the scope

-      iter.OutsHistory.ForEach(p => scope.Push(p.Name, p));

+      scope.PopMarker();  // for the in-parameters

+

+      // We resolve the rest of the specification in an instance context.  So mentions of the in- or yield-parameters

+      // get resolved as field dereferences (with an implicit "this")

+      scope.PushMarker();

+      currentClass = iter;

+      Contract.Assert(scope.AllowInstance);

 

       foreach (MaybeFreeExpression e in iter.YieldRequires) {

         ResolveExpression(e.E, false);

@@ -2588,29 +2592,23 @@ namespace Microsoft.Dafny
           Error(e.E, "Yield precondition must be a boolean (got {0})", e.E.Type);

         }

       }

-      foreach (MaybeFreeExpression e in iter.Ensures) {

+      foreach (MaybeFreeExpression e in iter.YieldEnsures) {

         ResolveExpression(e.E, true);

         Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression

         if (!UnifyTypes(e.E.Type, Type.Bool)) {

-          Error(e.E, "Postcondition must be a boolean (got {0})", e.E.Type);

+          Error(e.E, "Yield postcondition must be a boolean (got {0})", e.E.Type);

         }

       }

-

-      // Finally, add the yield-parameters and extra variables to the scope

-      scope.PushMarker();  // make the yield-parameters appear in the same scope as the outer-most locals of the body (since this is what is done for methods)

-      iter.Outs.ForEach(p => scope.Push(p.Name, p));

-      iter.ExtraVars.ForEach(p => scope.Push(p.Name, p));

-

-      ResolveAttributes(iter.Attributes, false);

-

-      foreach (MaybeFreeExpression e in iter.YieldEnsures) {

+      foreach (MaybeFreeExpression e in iter.Ensures) {

         ResolveExpression(e.E, true);

         Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression

         if (!UnifyTypes(e.E.Type, Type.Bool)) {

-          Error(e.E, "Yield postcondition must be a boolean (got {0})", e.E.Type);

+          Error(e.E, "Postcondition must be a boolean (got {0})", e.E.Type);

         }

       }

 

+      ResolveAttributes(iter.Attributes, false);

+

       var postSpecErrorCount = ErrorCount;

 

       // Resolve body

@@ -2618,8 +2616,8 @@ namespace Microsoft.Dafny
         ResolveBlockStatement(iter.Body, false, iter);

       }

 

-      scope.PopMarker();  // for the yield-parameters, extra variables, and outermost-level locals

-      scope.PopMarker();  // for the in-parameters and yield-history variables

+      currentClass = null;

+      scope.PopMarker();  // pop off the AllowInstance setting

 

       if (postSpecErrorCount == initialErrorCount) {

         CreateIteratorMethodSpecs(iter);

@@ -2630,10 +2628,7 @@ namespace Microsoft.Dafny
     /// Assumes the specification of the iterator itself has been successfully resolved.

     /// </summary>

     void CreateIteratorMethodSpecs(IteratorDecl iter) {

-      if (iter.Outs.Count != iter.OutsHistory.Count) {

-        // something must have gone wrong during registration, so don't worry about filling in the specs

-        return;

-      }

+      Contract.Requires(iter != null);

 

       // ---------- here comes the constructor ----------

       // same requires clause as the iterator itself

@@ -2646,7 +2641,7 @@ namespace Microsoft.Dafny
         ens.Add(new MaybeFreeExpression(new BinaryExpr(p.tok, BinaryExpr.Opcode.Eq,

           new FieldSelectExpr(p.tok, new ThisExpr(p.tok), p.Name), new IdentifierExpr(p.tok, p.Name))));

       }

-      foreach (var p in iter.OutsHistory) {

+      foreach (var p in iter.OutsHistoryFields) {

         // ensures this.ys == [];

         ens.Add(new MaybeFreeExpression(new BinaryExpr(p.tok, BinaryExpr.Opcode.Eq,

           new FieldSelectExpr(p.tok, new ThisExpr(p.tok), p.Name), new SeqDisplayExpr(p.tok, new List<Expression>()))));

@@ -2695,7 +2690,6 @@ namespace Microsoft.Dafny
           new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), iter.DecreasesFields[i].Name),

           new OldExpr(iter.tok, p))));

       }

-      

 

       // ---------- here comes predicate Valid() ----------

       var reads = iter.Member_Valid.Reads;

@@ -2704,50 +2698,31 @@ namespace Microsoft.Dafny
       reads.Add(new FrameExpression(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"), null));  // reads this._new;

 

       // ---------- here comes method MoveNext() ----------

-      // Build a substitution from the formals/variables to the corresponding fields.  Note, because these substitutions

-      // will be applied to an already resolved expression, the recursive idempotent Resolve operation on these method

-      // specifications may not reach down to these new parts.  Hence, these must be resolved right away (and they had better

-      // produce the same types as the subexpression they are replacing).

-      var substMap = new Dictionary<IVariable, Expression>();

-      foreach (var p in iter.Ins.Concat(iter.Outs.Concat(iter.OutsHistory.Concat(iter.ExtraVars)))) {

-        var f = (Field)iter.Members.Find(member => member is Field && member.Name == p.Name);

-        if (f == null) {

-          // something must have gone wrong during registration, so don't worry about adding this parameter to the substitution map

-        } else {

-          var th = new ThisExpr(p.tok);

-          th.Type = GetThisType(p.tok, iter);  // resolve here

-          var pe = new FieldSelectExpr(p.tok, th, p.Name);

-          pe.Field = f; pe.Type = p.Type;  // resolve here

-          substMap.Add(p, pe);

-        }

-      }

-      var subst = new Translator.Substituter(null, substMap);

       // requires this.Valid();

       var req = iter.Member_MoveNext.Req;

       req.Add(new MaybeFreeExpression(new FunctionCallExpr(iter.tok, "Valid", new ThisExpr(iter.tok), iter.tok, new List<Expression>())));

-      // requires YieldRequires[subst];

-      foreach (var yp in iter.YieldRequires) {

-        req.Add(new MaybeFreeExpression(subst.Substitute(yp.E), yp.IsFree, subst.SubstAttributes(yp.Attributes)));

-      }

+      // requires YieldRequires;

+      req.AddRange(iter.YieldRequires);

       // modifies this, this._modifies, this._new;

-      iter.Member_MoveNext.Mod.Expressions.Add(new FrameExpression(iter.tok, new ThisExpr(iter.tok), null));

-      iter.Member_MoveNext.Mod.Expressions.Add(new FrameExpression(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_modifies"), null));

-      iter.Member_MoveNext.Mod.Expressions.Add(new FrameExpression(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"), null));

-      // ensures more ==> this.Valid();

-      ens = iter.Member_MoveNext.Ens;

-      ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Imp,

-        new IdentifierExpr(iter.tok, "more"),

-        new FunctionCallExpr(iter.tok, "Valid", new ThisExpr(iter.tok), iter.tok, new List<Expression>()))));

+      var mod = iter.Member_MoveNext.Mod.Expressions;

+      mod.Add(new FrameExpression(iter.tok, new ThisExpr(iter.tok), null));

+      mod.Add(new FrameExpression(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_modifies"), null));

+      mod.Add(new FrameExpression(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"), null));

       // ensures fresh(_new - old(_new));

+      ens = iter.Member_MoveNext.Ens;

       ens.Add(new MaybeFreeExpression(new FreshExpr(iter.tok,

         new BinaryExpr(iter.tok, BinaryExpr.Opcode.Sub,

           new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"),

           new OldExpr(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"))))));

+      // ensures more ==> this.Valid();

+      ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Imp,

+        new IdentifierExpr(iter.tok, "more"),

+        new FunctionCallExpr(iter.tok, "Valid", new ThisExpr(iter.tok), iter.tok, new List<Expression>()))));

       // ensures this.ys == if more then old(this.ys) + [this.y] else old(this.ys);

-      Contract.Assert(iter.Outs.Count == iter.OutsHistory.Count);

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

-        var y = iter.Outs[i];

-        var ys = iter.OutsHistory[i];

+      Contract.Assert(iter.OutsFields.Count == iter.OutsHistoryFields.Count);

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

+        var y = iter.OutsFields[i];

+        var ys = iter.OutsHistoryFields[i];

         var ite = new ITEExpr(iter.tok, new IdentifierExpr(iter.tok, "more"),

           new BinaryExpr(iter.tok, BinaryExpr.Opcode.Add,

             new OldExpr(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name)),

@@ -2756,17 +2731,17 @@ namespace Microsoft.Dafny
         var eq = new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name), ite);

         ens.Add(new MaybeFreeExpression(eq));

       }

-      // ensures more ==> YieldEnsures[subst];

+      // ensures more ==> YieldEnsures;

       foreach (var ye in iter.YieldEnsures) {

-        ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Imp,

-          new IdentifierExpr(iter.tok, "more"), subst.Substitute(ye.E)),

+        ens.Add(new MaybeFreeExpression(

+          new BinaryExpr(iter.tok, BinaryExpr.Opcode.Imp, new IdentifierExpr(iter.tok, "more"), ye.E),

           ye.IsFree));

       }

-      // ensures !more ==> Ensures[subst];

+      // ensures !more ==> Ensures;

       foreach (var e in iter.Ensures) {

         ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Imp,

           new UnaryExpr(iter.tok, UnaryExpr.Opcode.Not, new IdentifierExpr(iter.tok, "more")),

-          subst.Substitute(e.E)),

+          e.E),

           e.IsFree));

       }

       // decreases this._decreases0, this._decreases1, ...;

@@ -2775,7 +2750,7 @@ namespace Microsoft.Dafny
         var p = iter.Decreases.Expressions[i];

         iter.Member_MoveNext.Decreases.Expressions.Add(new FieldSelectExpr(p.tok, new ThisExpr(p.tok), iter.DecreasesFields[i].Name));

       }

-      iter.Member_MoveNext.Decreases.Attributes = subst.SubstAttributes(iter.Decreases.Attributes);

+      iter.Member_MoveNext.Decreases.Attributes = iter.Decreases.Attributes;

     }

 

     /// <summary>

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index bb998e1b..a65da1ca 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -715,7 +715,7 @@ namespace Microsoft.Dafny {
       ExpressionTranslator etran = new ExpressionTranslator(this, predef, iter.tok);

 

       Bpl.VariableSeq inParams, outParams;

-      GenerateMethodParameters(iter.tok, iter, etran, out inParams, out outParams);

+      GenerateMethodParametersChoose(iter.tok, iter, true, true, false, etran, out inParams, out outParams);

 

       var req = new Bpl.RequiresSeq();

       var mod = new Bpl.IdentifierExprSeq();

@@ -787,25 +787,12 @@ namespace Microsoft.Dafny {
 

       Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(iter.TypeArgs);

       Bpl.VariableSeq inParams = Bpl.Formal.StripWhereClauses(proc.InParams);

-      Bpl.VariableSeq outParams = Bpl.Formal.StripWhereClauses(proc.OutParams);

+      Contract.Assert(1 <= inParams.Length);  // there should at least be a receiver parameter

+      Contract.Assert(proc.OutParams.Length == 0);

 

       var builder = new Bpl.StmtListBuilder();

       var etran = new ExpressionTranslator(this, predef, iter.tok);

       var localVariables = new Bpl.VariableSeq();

-      GenerateIteratorImplPrelude(iter, inParams, outParams, builder, localVariables);

-

-      foreach (var p in iter.OutsHistory) {

-        // var ys: seq<...>;

-        // TODO: should this variable have a 'where' clause?

-        localVariables.Add(new Bpl.LocalVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type))));

-      }

-      foreach (var p in iter.ExtraVars) {

-        // var extra: T;

-        // TODO: should this variable have a 'where' clause?

-        localVariables.Add(new Bpl.LocalVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type))));

-      }

-

-

 

       Bpl.StmtList stmts;

       // check well-formedness of the preconditions, and then assume each one of them

@@ -813,18 +800,23 @@ namespace Microsoft.Dafny {
         CheckWellformed(p.E, new WFOptions(), localVariables, builder, etran);

         builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));

       }

+      // check well-formedness of the decreases clauses

+      foreach (var p in iter.Decreases.Expressions) {

+        CheckWellformed(p, new WFOptions(), localVariables, builder, etran);

+      }

       // Note: the reads and modifies clauses are not checked for well-formedness (is that sound?), because it used to

       // be that the syntax was not rich enough for programmers to specify modifies clauses and always being

       // absolutely well-defined.

-      // check well-formedness of the decreases clauses

-      foreach (var p in iter.Decreases.Expressions)

-      {

-        CheckWellformed(p, new WFOptions(), localVariables, builder, etran);

+

+      // Next, we assume about this.* whatever we said that the iterator constructor promises

+      foreach (var p in iter.Member_Init.Ens) {

+        builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));

       }

 

-      // play havoc with the heap according to the modifies clause and inverse of the reads clause

-      // TODO: something like: builder.Add(new Bpl.HavocCmd(m.tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr)));

+      // play havoc with the heap, except at the locations prescribed by (this._reads - this._modifies)

+      builder.Add(new Bpl.HavocCmd(iter.tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr)));

       // assume the usual two-state boilerplate information

+      // TODO: the following line does not do exactly what we want:

       foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(iter.tok, iter.Modifies.Expressions/*TODO: should this also include the Reads clause?*/, etran.Old, etran, etran.Old))

       {

         if (tri.IsFree) {

@@ -832,23 +824,22 @@ namespace Microsoft.Dafny {
         }

       }

 

-      // also play havoc with the out parameters

-      if (outParams.Length != 0) {  // don't create an empty havoc statement

-        Bpl.IdentifierExprSeq outH = new Bpl.IdentifierExprSeq();

-        foreach (Bpl.Variable b in outParams) {

-          Contract.Assert(b != null);

-          outH.Add(new Bpl.IdentifierExpr(b.tok, b));

-        }

-        builder.Add(new Bpl.HavocCmd(iter.tok, outH));

-      }

+      // assume the automatic yield-requires precondition (which is always well-formed):  this.Valid()

+      var th = new ThisExpr(iter.tok);

+      th.Type = Resolver.GetThisType(iter.tok, iter);  // resolve here

+      var validCall = new FunctionCallExpr(iter.tok, "Valid", th, iter.tok, new List<Expression>());

+      validCall.Function = iter.Member_Valid;  // resolve here

+      validCall.Type = Type.Bool;  // resolve here

+      builder.Add(new Bpl.AssumeCmd(iter.tok, etran.TrExpr(validCall)));

 

-      // check wellformedness of yield requires

+      // check well-formedness of the user-defined part of the yield-requires

       foreach (var p in iter.YieldRequires) {

         CheckWellformed(p.E, new WFOptions(), localVariables, builder, etran);

         builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));

       }

 

-      // TODO: do another havoc

+      // simulate a modifies this, this._modifies, this._new;

+      // TODO

 

       // check wellformedness of postconditions

       var yeBuilder = new Bpl.StmtListBuilder();

@@ -868,7 +859,7 @@ namespace Microsoft.Dafny {
       QKeyValue kv = etran.TrAttributes(iter.Attributes, null);

 

       Bpl.Implementation impl = new Bpl.Implementation(iter.tok, proc.Name,

-        typeParams, inParams, outParams,

+        typeParams, inParams, new VariableSeq(),

         localVariables, stmts, kv);

       sink.TopLevelDeclarations.Add(impl);

 

@@ -892,27 +883,24 @@ namespace Microsoft.Dafny {
 

       Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(iter.TypeArgs);

       Bpl.VariableSeq inParams = Bpl.Formal.StripWhereClauses(proc.InParams);

-      Bpl.VariableSeq outParams = Bpl.Formal.StripWhereClauses(proc.OutParams);

+      Contract.Assert(1 <= inParams.Length);  // there should at least be a receiver parameter

+      Contract.Assert(proc.OutParams.Length == 0);

 

       Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, iter.tok);

       Bpl.VariableSeq localVariables = new Bpl.VariableSeq();

-      GenerateIteratorImplPrelude(iter, inParams, outParams, builder, localVariables);

+      GenerateIteratorImplPrelude(iter, inParams, new VariableSeq(), builder, localVariables);

+

       // add locals for the yield-history variables and the extra variables

-      foreach (var p in iter.OutsHistory) {

-        // var ys: seq<...>;

-        // TODO: should this variable have a 'where' clause?

-        localVariables.Add(new Bpl.LocalVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type))));

-        // ys := [];

-        var ys = etran.TrVar(p.tok, p);

-        builder.Add(Bpl.Cmd.SimpleAssign(p.tok, ys, FunctionCall(p.tok, BuiltinFunction.SeqEmpty, predef.BoxType)));

-      }

-      foreach (var p in iter.ExtraVars) {

-        // var extra: T;

-        // TODO: should this variable have a 'where' clause?

-        localVariables.Add(new Bpl.LocalVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type))));

-      }

-      // also add the _yieldCount variable, and assume its initial value to be 0

+      // Assume the precondition and postconditions of the iterator constructor method

+      foreach (var p in iter.Member_Init.Req) {

+        builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));

+      }

+      foreach (var p in iter.Member_Init.Ens) {

+        // these postconditions are two-state predicates, but that's okay, because we haven't changed anything yet

+        builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));

+      }

+      // add the _yieldCount variable, and assume its initial value to be 0

       yieldCountVariable = new Bpl.LocalVariable(iter.tok, new Bpl.TypedIdent(iter.tok, "_yieldCount", Bpl.Type.Int));

       yieldCountVariable.TypedIdent.WhereExpr = YieldCountAssumption(iter, etran);  // by doing this after setting "yieldCountVariable", the variable can be used by YieldCountAssumption

       localVariables.Add(yieldCountVariable);

@@ -930,7 +918,7 @@ namespace Microsoft.Dafny {
       QKeyValue kv = etran.TrAttributes(iter.Attributes, null);

 

       Bpl.Implementation impl = new Bpl.Implementation(iter.tok, proc.Name,

-        typeParams, inParams, outParams,

+        typeParams, inParams, new VariableSeq(),

         localVariables, stmts, kv);

       sink.TopLevelDeclarations.Add(impl);

 

@@ -947,11 +935,13 @@ namespace Microsoft.Dafny {
       Contract.Requires(etran != null);

       Contract.Requires(yieldCountVariable != null);

       Bpl.Expr wh = Bpl.Expr.True;

-      foreach (var ys in iter.OutsHistory) {

-        // add the conjunct:  _yieldCount == |ys|

+      foreach (var ys in iter.OutsHistoryFields) {

+        // add the conjunct:  _yieldCount == |this.ys|

         wh = Bpl.Expr.And(wh, Bpl.Expr.Eq(new Bpl.IdentifierExpr(iter.tok, yieldCountVariable),

-          FunctionCall(iter.tok, BuiltinFunction.SeqLength, null, etran.TrVar(iter.tok, ys))));

-

+          FunctionCall(iter.tok, BuiltinFunction.SeqLength, null,

+          ExpressionTranslator.ReadHeap(iter.tok, etran.HeapExpr,

+            new Bpl.IdentifierExpr(iter.tok, etran.This, predef.RefType),

+            new Bpl.IdentifierExpr(iter.tok, GetField(ys))))));

       }

       return wh;

     }

@@ -3718,9 +3708,14 @@ namespace Microsoft.Dafny {
     }

 

     private void GenerateMethodParameters(IToken tok, ICodeContext m, ExpressionTranslator etran, out Bpl.VariableSeq inParams, out Bpl.VariableSeq outParams) {

+      GenerateMethodParametersChoose(tok, m, !m.IsStatic, true, true, etran, out inParams, out outParams);

+    }

+

+    private void GenerateMethodParametersChoose(IToken tok, ICodeContext m, bool includeReceiver, bool includeInParams, bool includeOutParams,

+      ExpressionTranslator etran, out Bpl.VariableSeq inParams, out Bpl.VariableSeq outParams) {

       inParams = new Bpl.VariableSeq();

       outParams = new Bpl.VariableSeq();

-      if (!m.IsStatic) {

+      if (includeReceiver) {

         var receiverType = m is MemberDecl ? Resolver.GetReceiverType(tok, (MemberDecl)m) : Resolver.GetThisType(tok, (IteratorDecl)m);

         Bpl.Expr wh = Bpl.Expr.And(

           Bpl.Expr.Neq(new Bpl.IdentifierExpr(tok, "this", predef.RefType), predef.Null),

@@ -3728,19 +3723,24 @@ namespace Microsoft.Dafny {
         Bpl.Formal thVar = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "this", predef.RefType, wh), true);

         inParams.Add(thVar);

       }

-      foreach (Formal p in m.Ins) {

-        Bpl.Type varType = TrType(p.Type);

-        Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);

-        inParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), true));

+      if (includeInParams) {

+        foreach (Formal p in m.Ins) {

+          Bpl.Type varType = TrType(p.Type);

+          Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);

+          inParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), true));

+        }

       }

-      foreach (Formal p in m.Outs) {

-        Bpl.Type varType = TrType(p.Type);

-        Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);

-        outParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), false));

+      if (includeOutParams) {

+        foreach (Formal p in m.Outs) {

+          Bpl.Type varType = TrType(p.Type);

+          Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);

+          outParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), false));

+        }

       }

     }

 

-    class BoilerplateTriple {  // a triple that is now a quintuple

+    class BoilerplateTriple

+    {  // a triple that is now a quintuple

       [ContractInvariantMethod]

       void ObjectInvariant() {

         Contract.Invariant(tok != null);

@@ -4103,21 +4103,24 @@ namespace Microsoft.Dafny {
         AddComment(builder, s, "yield statement");

         Contract.Assert(codeContext is IteratorDecl);

         var iter = (IteratorDecl)codeContext;

-        // ys := ys + [y];

-        Contract.Assert(iter.Outs.Count == iter.OutsHistory.Count);

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

-          var y = iter.Outs[i];

-          var dafnyY = new IdentifierExpr(s.Tok, y.Name);

-          dafnyY.Var = y; dafnyY.Type = y.Type;  // resolve here

-          var ys = iter.OutsHistory[i];

-          var dafnyYs = new IdentifierExpr(s.Tok, ys.Name);

-          dafnyYs.Var = ys; dafnyYs.Type = ys.Type;  // resolve here

+        // this.ys := this.ys + [this.y];

+        var th = new ThisExpr(iter.tok);

+        th.Type = Resolver.GetThisType(iter.tok, iter);  // resolve here

+        Contract.Assert(iter.OutsFields.Count == iter.OutsHistoryFields.Count);

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

+          var y = iter.OutsFields[i];

+          var dafnyY = new FieldSelectExpr(s.Tok, th, y.Name);

+          dafnyY.Field = y; dafnyY.Type = y.Type;  // resolve here

+          var ys = iter.OutsHistoryFields[i];

+          var dafnyYs = new FieldSelectExpr(s.Tok, th, ys.Name);

+          dafnyYs.Field = ys; dafnyYs.Type = ys.Type;  // resolve here

           var dafnySingletonY = new SeqDisplayExpr(s.Tok, new List<Expression>() { dafnyY });

           dafnySingletonY.Type = ys.Type;  // resolve here

           var rhs = new BinaryExpr(s.Tok, BinaryExpr.Opcode.Add, dafnyYs, dafnySingletonY);

           rhs.ResolvedOp = BinaryExpr.ResolvedOpcode.Concat;

           rhs.Type = ys.Type;  // resolve here

-          var cmd = Bpl.Cmd.SimpleAssign(s.Tok, etran.TrVar(s.Tok, ys), etran.TrExpr(rhs));

+          var cmd = Bpl.Cmd.SimpleAssign(s.Tok, (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr,

+            ExpressionTranslator.UpdateHeap(s.Tok, etran.HeapExpr, etran.TrExpr(th), new Bpl.IdentifierExpr(s.Tok, GetField(ys)), etran.TrExpr(rhs)));

           builder.Add(cmd);

         }

         // yieldCount := yieldCount + 1;  assume yieldCount == |ys|;

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index ecde4fb1..358a64bf 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1617,15 +1617,13 @@ TailCalls.dfy(64,12): Error: 'decreases *' is allowed only on tail-recursive met
 

 -------------------- IteratorResolution.dfy --------------------

 IteratorResolution.dfy(59,11): Error: LHS of assignment does not denote a mutable field

-IteratorResolution.dfy(60,11): Error: LHS of assignment does not denote a mutable field

 IteratorResolution.dfy(64,18): Error: arguments must have the same type (got _T0 and int)

 IteratorResolution.dfy(76,19): Error: RHS (of type bool) not assignable to LHS (of type int)

 IteratorResolution.dfy(79,13): Error: when allocating an object of type 'GenericIteratorResult', one of its constructor methods must be called

 IteratorResolution.dfy(83,15): Error: logical negation expects a boolean argument (instead got int)

 IteratorResolution.dfy(17,11): Error: LHS of assignment does not denote a mutable field

-IteratorResolution.dfy(18,11): Error: LHS of assignment does not denote a mutable field

 IteratorResolution.dfy(19,12): Error: LHS of assignment does not denote a mutable field

-9 resolution/type errors detected in IteratorResolution.dfy

+7 resolution/type errors detected in IteratorResolution.dfy

 

 -------------------- Iterators.dfy --------------------

 Iterators.dfy(36,14): Error BP5002: A precondition for this call might not hold.

diff --git a/Test/dafny0/IteratorResolution.dfy b/Test/dafny0/IteratorResolution.dfy
index dca4cb93..68fec344 100644
--- a/Test/dafny0/IteratorResolution.dfy
+++ b/Test/dafny0/IteratorResolution.dfy
@@ -15,7 +15,7 @@ module Mx {
   method IteratorUser() {

     var iter := new ExampleIterator.ExampleIterator(15);

     iter.k := 12;  // error: not allowed to assign to iterator's in-parameters

-    iter.x := 12;  // error: not allowed to assign to iterator's yield-parameters

+    iter.x := 12;  // note, not allowed to assign to iterator's yield-parameters (except via 'this')

     iter.xs := [];  // error: not allowed to assign to iterator's yield-history variables

     var j := 0;

     while (j < 100) {

@@ -57,7 +57,7 @@ module Mx {
       requires g0.u;

     {

       g0.t := true;  // error: not allowed to assign to .t

-      g0.u := true;  // error: not allowed to assign to .u

+      g0.u := true;  // note, not allowed to assign to iterator's yield-parameters (except via 'this'), but this is checked by the verifier

       var g1 := new GenericIterator.GenericIterator(20);

       assert g1.u < 200;  // .u is an integer

 

diff --git a/Test/dafny0/Iterators.dfy b/Test/dafny0/Iterators.dfy
index 680c2812..3f06e445 100644
--- a/Test/dafny0/Iterators.dfy
+++ b/Test/dafny0/Iterators.dfy
@@ -91,10 +91,11 @@ method TestIterA()
 iterator IterB(c: Cell)

   requires c != null;

   modifies c;

-  yield ensures c.data == old(c.data);  // error: cannot prove this without a reads clause

+  yield ensures c.data == old(c.data);

   ensures true;

 {

   if (*) { yield; }

+  if (*) { yield; }  // error: cannot prove the yield-ensures clause here (needs a reads clause)

   c.data := *;

 }

 

@@ -117,10 +118,11 @@ iterator IterC(c: Cell)
   requires c != null;

   modifies c;

   reads c;

-  yield ensures c.data == old(c.data);  // error: cannot prove this without a reads clause

+  yield ensures c.data == old(c.data);

   ensures true;

 {

   if (*) { yield; }

+  if (*) { yield; }  // this time, all is fine, because the iterator has an appropriate reads clause

   c.data := *;

 }