Initial modifies on loops implementation. Still some errors remaining.

6 files changed, 151 insertions, 68 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index e117ad67..033bc239 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -843,7 +843,7 @@ WhileStmt<out Statement/*!*/ stmt>
      Expression guard;

      List<MaybeFreeExpression/*!*/> invariants = new List<MaybeFreeExpression/*!*/>();

      List<Expression/*!*/> decreases = new List<Expression/*!*/>();

-     List<FrameExpression/*!*/> mod = new List<FrameExpression/*!*/>();

+     List<FrameExpression/*!*/> mod = null;

      Statement/*!*/ body;

      IToken bodyStart, bodyEnd;

      List<GuardedAlternative> alternatives;

@@ -866,7 +866,7 @@ LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*
 = (. bool isFree;  Expression/*!*/ e; FrameExpression/*!*/ fe;

      invariants = new List<MaybeFreeExpression/*!*/>();

      decreases = new List<Expression/*!*/>();

-     mod = new List<FrameExpression/*!*/>();

+     mod = null;

   .)

   {                         (. isFree = false; .)

     [ "free"                (. isFree = true; .)

@@ -875,7 +875,8 @@ LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*
     Expression<out e>       (. invariants.Add(new MaybeFreeExpression(e, isFree)); .)

     ";"

   | "decreases" DecreasesList<decreases, true> ";"

-  | "modifies" [ FrameExpression<out fe>                     (. mod.Add(fe); .)

+  | "modifies" (. mod = mod ?? new List<FrameExpression>(); .)

+               [ FrameExpression<out fe>                     (. mod.Add(fe); .)

                  { "," FrameExpression<out fe>               (. mod.Add(fe); .)

                  }

                ] ";"

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index dc925519..0fd83011 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1661,11 +1661,12 @@ namespace Microsoft.Dafny {
     public readonly List<MaybeFreeExpression/*!*/>/*!*/ Invariants;

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

     public readonly List<FrameExpression/*!*/>/*!*/ Mod;

+    public readonly bool explictModifies;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullElements(Invariants));

       Contract.Invariant(cce.NonNullElements(Decreases));

-      Contract.Invariant(cce.NonNullElements(Mod));

+      Contract.Invariant(Mod == null || cce.NonNullElements(Mod));

     }

     public LoopStmt(IToken tok, List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/>/*!*/ mod)

     : base(tok) 

@@ -1673,7 +1674,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(tok != null);

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

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

-      Contract.Requires(cce.NonNullElements(mod));

+      Contract.Requires(mod == null || cce.NonNullElements(mod));

 

       this.Invariants = invariants;

       this.Decreases = decreases;

@@ -1691,7 +1692,7 @@ namespace Microsoft.Dafny {
     }

 

     public WhileStmt(IToken tok, Expression guard,

-                     List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/>/*!*/ mod,

+                     List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/> mod,

                      Statement/*!*/ body)

       : base(tok, invariants, decreases, mod) {

       Contract.Requires(tok != null);

@@ -1709,7 +1710,7 @@ namespace Microsoft.Dafny {
       Contract.Invariant(Alternatives != null);

     }

     public AlternativeLoopStmt(IToken tok,

-                               List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/>/*!*/ mod,

+                               List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/> mod,

                                List<GuardedAlternative> alternatives)

       : base(tok, invariants, decreases, mod) {

       Contract.Requires(tok != null);

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index d11e8f08..b77f5e65 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1189,7 +1189,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expression guard;

 		List<MaybeFreeExpression/*!*/> invariants = new List<MaybeFreeExpression/*!*/>();

 		List<Expression/*!*/> decreases = new List<Expression/*!*/>();

-		List<FrameExpression/*!*/> mod = new List<FrameExpression/*!*/>();

+		List<FrameExpression/*!*/> mod = null;

 		Statement/*!*/ body;

 		IToken bodyStart, bodyEnd;

 		List<GuardedAlternative> alternatives;

@@ -1393,7 +1393,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		bool isFree;  Expression/*!*/ e; FrameExpression/*!*/ fe;

 		invariants = new List<MaybeFreeExpression/*!*/>();

 		decreases = new List<Expression/*!*/>();

-		mod = new List<FrameExpression/*!*/>();

+		mod = null;

 		

 		while (StartOf(13)) {

 			if (la.kind == 29 || la.kind == 59) {

@@ -1412,6 +1412,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 				Expect(17);

 			} else {

 				Get();

+				mod = mod ?? new List<FrameExpression>(); 

 				if (StartOf(8)) {

 					FrameExpression(out fe);

 					mod.Add(fe); 

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index a8970f05..9970d61a 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -507,6 +507,10 @@ namespace Microsoft.Dafny {
 

         PrintSpec("invariant", s.Invariants, indent + IndentAmount);

         PrintSpecLine("decreases", s.Decreases, indent + IndentAmount);

+        if (s.Mod != null)

+        {

+            PrintFrameSpecLine("modifies", s.Mod, indent + IndentAmount);

+        }

         Indent(indent);

         PrintStatement(s.Body, indent);

 

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 17309836..c0bf4392 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1512,6 +1512,11 @@ namespace Microsoft.Dafny {
           }

           // any type is fine

         }

+        if(s.Mod != null) {

+          foreach (FrameExpression fe in s.Mod) {

+            ResolveFrameExpression(fe, "modifies");

+          }

+        }

         s.IsGhost = bodyMustBeSpecOnly;

         loopStack.Add(s);  // push

         if (s.Labels == null) {  // otherwise, "s" is already in "inSpecOnlyContext" map

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 07e328a0..b517dd90 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1003,7 +1003,7 @@ namespace Microsoft.Dafny {
         // play havoc with the heap according to the modifies clause

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

         // assume the usual two-state boilerplate information

-        foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, currentMethod, etran.Old, etran)) {

+        foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, currentMethod.Mod, etran.Old, etran, etran.Old)) {

           if (tri.IsFree) {

             builder.Add(new Bpl.AssumeCmd(m.tok, tri.Expr));

           }

@@ -1049,7 +1049,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(predef != null);

     

       // set up the information used to verify the method's modifies clause

-      DefineFrame(m.tok, m.Mod, builder, localVariables);

+      DefineFrame(m.tok, m.Mod, builder, localVariables, null);

     }

 

     Bpl.Cmd CaptureState(IToken tok, string/*?*/ additionalInfo) {

@@ -1065,7 +1065,8 @@ namespace Microsoft.Dafny {
       return CaptureState(tok, null);

     }

     

-    void DefineFrame(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ frameClause, Bpl.StmtListBuilder/*!*/ builder, Bpl.VariableSeq/*!*/ localVariables){

+      //^^^ this caputres the frame, it looks like.

+    void DefineFrame(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ frameClause, Bpl.StmtListBuilder/*!*/ builder, Bpl.VariableSeq/*!*/ localVariables, string name){

       Contract.Requires(tok != null);

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

       Contract.Requires(builder != null);

@@ -1074,9 +1075,9 @@ namespace Microsoft.Dafny {
     

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

       // Declare a local variable $_Frame: <alpha>[ref, Field alpha]bool

-      Bpl.IdentifierExpr theFrame = etran.TheFrame(tok);  // this is a throw-away expression, used only to extract the name and type of the $_Frame variable

+      Bpl.IdentifierExpr theFrame = etran.TheFrame(tok);  // this is a throw-away expression, used only to extract the type of the $_Frame variable

       Contract.Assert(theFrame.Type != null);  // follows from the postcondition of TheFrame

-      Bpl.LocalVariable frame = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, theFrame.Name, theFrame.Type));

+      Bpl.LocalVariable frame = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, name ?? theFrame.Name, theFrame.Type));

       localVariables.Add(frame);

       // $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: $o != null && $Heap[$o,alloc] ==> ($o,$f) in Modifies/Reads-Clause);

       Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "alpha");

@@ -1099,14 +1100,14 @@ namespace Microsoft.Dafny {
     {

       Contract.Requires(tok != null);

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

-      Contract.Requires(receiverReplacement != null);

-      Contract.Requires(cce.NonNullDictionaryAndValues(substMap));

+      Contract.Requires((receiverReplacement == null) == (substMap == null));

+      Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap));

       Contract.Requires(etran != null);

       Contract.Requires(builder != null);

       Contract.Requires(errorMessage != null);

       Contract.Requires(predef != null);

 

-      // emit: assert (forall<alpha> o: ref, f: Field alpha :: o != null && $Heap[o,alloc] && (o,f) in calleeFrame ==> $_Frame[o,f]);

+      // emit: assert (forall<alpha> o: ref, f: Field alpha :: o != null && $Heap[o,alloc] && (o,f) in subFrame ==> $_Frame[o,f]);

       Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "alpha");

       Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType));

       Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(tok, oVar);

@@ -1230,7 +1231,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(f != null);

       Contract.Requires(etran != null);

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

-      Contract.Requires(cce.NonNullDictionaryAndValues(substMap));

+      Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap));

       Contract.Requires(predef != null);

       Contract.Requires((receiverReplacement == null) == (substMap == null));

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

@@ -1241,8 +1242,8 @@ namespace Microsoft.Dafny {
       Bpl.Expr disjunction = null;

       foreach (FrameExpression rwComponent in rw) {

         Expression e = rwComponent.E;

-        if (substMap != null) {

-          Contract.Assert(receiverReplacement != null);

+        if (receiverReplacement != null) {

+          Contract.Assert(substMap != null);

           e = Substitute(e, receiverReplacement, substMap);

         }

         Bpl.Expr disjunct;

@@ -1355,7 +1356,7 @@ namespace Microsoft.Dafny {
         }

         Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, funcID, args);

 

-        DefineFrame(f.tok, f.Reads, bodyCheckBuilder, locals);

+        DefineFrame(f.tok, f.Reads, bodyCheckBuilder, locals, null);

         CheckWellformedWithResult(f.Body, new WFOptions(f, null, true), funcAppl, f.ResultType, locals, bodyCheckBuilder, etran);

 

         // check that postconditions hold

@@ -2539,7 +2540,7 @@ namespace Microsoft.Dafny {
           }

           comment = null;

         }

-        if (!skipEnsures) foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m, etran.Old, etran)) {

+        if (!skipEnsures) foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod, etran.Old, etran, etran.Old)) {

           ens.Add(Ensures(tri.tok, tri.IsFree, tri.Expr, tri.ErrorMessage, tri.Comment));

         }

       }

@@ -2766,15 +2767,15 @@ namespace Microsoft.Dafny {
     

     /// <summary>

     /// There are 3 states of interest when generating two-state boilerplate:

-    ///  S0. the beginning of the method, which is where the modifies clause is interpreted

+    ///  S0. the beginning of the method or loop, which is where the modifies clause is interpreted

     ///  S1. the pre-state of the two-state interval

     ///  S2. the post-state of the two-state interval

-    /// This method assumes that etranPre denotes S1, etran denotes S2, and that etran.Old denotes S0.

+    /// This method assumes that etranPre denotes S1, etran denotes S2, and that etranMod denotes S0.

     /// </summary>

-    List<BoilerplateTriple/*!*/>/*!*/ GetTwoStateBoilerplate(IToken/*!*/ tok, Method/*!*/ method, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran)

+    List<BoilerplateTriple/*!*/>/*!*/ GetTwoStateBoilerplate(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ modifiesClause, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran, ExpressionTranslator/*!*/ etranMod)

     {

       Contract.Requires(tok != null);

-      Contract.Requires(method != null);

+      Contract.Requires(modifiesClause != null);

       Contract.Requires(etranPre != null);

       Contract.Requires(etran != null);

       Contract.Ensures(cce.NonNullElements(Contract.Result<List<BoilerplateTriple>>()));

@@ -2782,7 +2783,7 @@ namespace Microsoft.Dafny {
       List<BoilerplateTriple> boilerplate = new List<BoilerplateTriple>();

       

       // the frame condition, which is free since it is checked with every heap update and call

-      boilerplate.Add(new BoilerplateTriple(tok, true, FrameCondition(tok, method.Mod, etranPre, etran), null, "frame condition"));

+      boilerplate.Add(new BoilerplateTriple(tok, true, FrameCondition(tok, modifiesClause, etranPre, etran, etranMod), null, "frame condition"));

 

       // HeapSucc(S1, S2)

       Bpl.Expr heapSucc = FunctionCall(tok, BuiltinFunction.HeapSucc, null, etranPre.HeapExpr, etran.HeapExpr);

@@ -2792,13 +2793,16 @@ namespace Microsoft.Dafny {
     }

     

     /// <summary>

-    /// There are 3 states of interest when generating a freame condition:

-    ///  S0. the beginning of the method, which is where the modifies clause is interpreted

+    /// There are 3 states of interest when generating a frame condition:

+    ///  S0. the beginning of the method/loop, which is where the modifies clause is interpreted

     ///  S1. the pre-state of the two-state interval

     ///  S2. the post-state of the two-state interval

-    /// This method assumes that etranPre denotes S1, etran denotes S2, and that etran.Old denotes S0.

+    /// This method assumes that etranPre denotes S1, etran denotes S2, and that etranMod denotes S0.

     /// </summary>

-    Bpl.Expr/*!*/ FrameCondition(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ modifiesClause, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran)

+    /// ^^^ this appears to say that the heap has not changed outside the modifies clause.

+    /// the post state would come after a while loop, and the pre state before. also, S0 would be the 

+    /// same as S1 for while loops.

+    Bpl.Expr/*!*/ FrameCondition(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ modifiesClause, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran, ExpressionTranslator/*!*/ etranMod)

      {

       Contract.Requires(tok != null);

       Contract.Requires(etran != null);

@@ -2820,15 +2824,43 @@ namespace Microsoft.Dafny {
 

       Bpl.Expr heapOF = ExpressionTranslator.ReadHeap(tok, etran.HeapExpr, o, f);

       Bpl.Expr preHeapOF = ExpressionTranslator.ReadHeap(tok, etranPre.HeapExpr, o, f);

-      Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etran.Old.IsAlloced(tok, o));

+      Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etranMod.IsAlloced(tok, o));

       Bpl.Expr consequent = Bpl.Expr.Eq(heapOF, preHeapOF);

       

-      consequent = Bpl.Expr.Or(consequent, InRWClause(tok, o, f, modifiesClause, etran.Old, null, null));

+      consequent = Bpl.Expr.Or(consequent, InRWClause(tok, o, f, modifiesClause, etranMod, null, null));

       

       Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(heapOF));

       return new Bpl.ForallExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, tr, Bpl.Expr.Imp(ante, consequent));

     }

-    

+    Bpl.Expr/*!*/ FrameConditionUsingDefinedFrame(IToken/*!*/ tok, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran, ExpressionTranslator/*!*/ etranMod)

+    {

+      Contract.Requires(tok != null);

+      Contract.Requires(etran != null);

+      Contract.Requires(etranPre != null);

+      Contract.Requires(predef != null);

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

+

+      // generate:

+      //  (forall<alpha> o: ref, f: Field alpha :: { $Heap[o,f] }

+      //      o != null && old($Heap)[o,alloc] ==>

+      //        $Heap[o,f] == PreHeap[o,f] ||

+      //        $_Frame[o,f])

+      Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "alpha");

+      Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType));

+      Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(tok, oVar);

+      Bpl.BoundVariable fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", predef.FieldName(tok, alpha)));

+      Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(tok, fVar);

+

+      Bpl.Expr heapOF = ExpressionTranslator.ReadHeap(tok, etran.HeapExpr, o, f);

+      Bpl.Expr preHeapOF = ExpressionTranslator.ReadHeap(tok, etranPre.HeapExpr, o, f);

+      Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etranPre.IsAlloced(tok, o));

+      Bpl.Expr consequent = Bpl.Expr.Eq(heapOF, preHeapOF);

+      //^^^

+      consequent = Bpl.Expr.Or(consequent, Bpl.Expr.SelectTok(tok, etranMod.TheFrame(tok), o, f));

+

+      Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(heapOF));

+      return new Bpl.ForallExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, tr, Bpl.Expr.Imp(ante, consequent));

+    }    

     // ----- Type ---------------------------------------------------------------------------------

     

     Bpl.Type TrType(Type type)

@@ -3116,20 +3148,20 @@ namespace Microsoft.Dafny {
         var elseCase = Assert(s.Tok, Bpl.Expr.False, "alternative cases fail to cover all possibilties");

         TrAlternatives(s.Alternatives, elseCase, null, builder, locals, etran);

 

-      } else if (stmt is WhileStmt) {

+      } else if (stmt is WhileStmt) { //^^^ While statement, needs checks.

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

         var s = (WhileStmt)stmt;

         TrLoop(s, s.Guard,

-          delegate(Bpl.StmtListBuilder bld) { TrStmt(s.Body, bld, locals, etran); },

+          delegate(Bpl.StmtListBuilder bld, ExpressionTranslator e) { TrStmt(s.Body, bld, locals, e); },

           builder, locals, etran);

 

-      } else if (stmt is AlternativeLoopStmt) {

+      } else if (stmt is AlternativeLoopStmt) { // ^^^ same thing.

         AddComment(builder, stmt, "alternative loop statement");

         var s = (AlternativeLoopStmt)stmt;

         var tru = new LiteralExpr(s.Tok, true);

         tru.Type = Type.Bool;  // resolve here

         TrLoop(s, tru,

-          delegate(Bpl.StmtListBuilder bld) { TrAlternatives(s.Alternatives, null, new Bpl.BreakCmd(s.Tok, null), bld, locals, etran); },

+          delegate(Bpl.StmtListBuilder bld, ExpressionTranslator e) { TrAlternatives(s.Alternatives, null, new Bpl.BreakCmd(s.Tok, null), bld, locals, e); },

           builder, locals, etran);

 

       } else if (stmt is ForeachStmt) {

@@ -3322,8 +3354,9 @@ namespace Microsoft.Dafny {
       }

     }

 

-    delegate void BodyTranslator(Bpl.StmtListBuilder builder);

+    delegate void BodyTranslator(Bpl.StmtListBuilder builder, ExpressionTranslator etran);

 

+    // ^^^ this needs to be updated to insert the appropriate checks, generate frame variables, etc.

     void TrLoop(LoopStmt s, Expression Guard, BodyTranslator bodyTr,

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

       Contract.Requires(s != null);

@@ -3343,6 +3376,17 @@ namespace Microsoft.Dafny {
       locals.Add(preLoopHeapVar);

       Bpl.IdentifierExpr preLoopHeap = new Bpl.IdentifierExpr(s.Tok, preLoopHeapVar);

       ExpressionTranslator etranPreLoop = new ExpressionTranslator(this, predef, preLoopHeap);

+      ExpressionTranslator updatedFrameEtran;

+      string loopFrameName = "#_Frame#" + loopId;

+      if(s.Mod != null)

+        updatedFrameEtran = new ExpressionTranslator(etran, loopFrameName);

+      else

+        updatedFrameEtran = etran;

+

+      if (s.Mod != null) { // check that the modifies is a strict subset

+          CheckFrameSubset(s.Tok, s.Mod, null, null, etran, builder, "loop modifies clause may violate context's modifies clause", null);

+          DefineFrame(s.Tok, s.Mod, builder, locals, loopFrameName);

+      }

       builder.Add(Bpl.Cmd.SimpleAssign(s.Tok, preLoopHeap, etran.HeapExpr));

 

       List<Bpl.Expr> initDecr = null;

@@ -3390,14 +3434,19 @@ namespace Microsoft.Dafny {
         TrStmt_CheckWellformed(e, invDefinednessBuilder, locals, etran, true);

       }

       // include boilerplate invariants

-      foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(s.Tok, currentMethod, etranPreLoop, etran)) {

-        if (tri.IsFree) {

-          invariants.Add(new Bpl.AssumeCmd(s.Tok, tri.Expr));

-        } else {

-          Contract.Assert(tri.ErrorMessage != null);  // follows from BoilerplateTriple invariant

-          invariants.Add(Assert(s.Tok, tri.Expr, tri.ErrorMessage));

-        }

+      foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(s.Tok, currentMethod.Mod, etranPreLoop, etran, etran.Old))

+      {

+          if (tri.IsFree) {

+              invariants.Add(new Bpl.AssumeCmd(s.Tok, tri.Expr));

+          }

+          else {

+              Contract.Assert(tri.ErrorMessage != null);  // follows from BoilerplateTriple invariant

+              invariants.Add(Assert(s.Tok, tri.Expr, tri.ErrorMessage));

+          }

       }

+      //^^^ add a free invariant which says that the heap hasn't changed outside of the modifies clause.

+      invariants.Add(new Bpl.AssumeCmd(s.Tok, FrameConditionUsingDefinedFrame(s.Tok, etranPreLoop, etran, updatedFrameEtran)));

+      

       // include a free invariant that says that all completed iterations so far have only decreased the termination metric

       if (initDecr != null) {

         List<IToken> toks = new List<IToken>();

@@ -3430,11 +3479,11 @@ namespace Microsoft.Dafny {
       // termination checking

       if (Contract.Exists(theDecreases, e => e is WildcardExpr)) {

         // omit termination checking for this loop

-        bodyTr(loopBodyBuilder);

+        bodyTr(loopBodyBuilder, updatedFrameEtran);//^^^ !! this needs to be the translator with the captured frame.

       } else {

         List<Bpl.Expr> oldBfs = RecordDecreasesValue(theDecreases, loopBodyBuilder, locals, etran, "$decr" + loopId + "$");

         // time for the actual loop body

-        bodyTr(loopBodyBuilder);

+        bodyTr(loopBodyBuilder, updatedFrameEtran);//^^^ !! this needs to be the translator with the captured frame.

         // check definedness of decreases expressions

         List<IToken> toks = new List<IToken>();

         List<Type> types = new List<Type>();

@@ -3585,8 +3634,8 @@ namespace Microsoft.Dafny {
         ins.Add(param);

       }

 

-      // Check modifies clause

-      CheckFrameSubset(tok, method.Mod, receiver, substMap, etran, builder, "call may violate caller's modifies clause", null);

+      // Check modifies clause of a subcall is a subset of the current frame.

+      CheckFrameSubset(tok, method.Mod, receiver, substMap, etran, builder, "call may violate context's modifies clause", null);

 

       // Check termination

       ModuleDecl module = cce.NonNull(method.EnclosingClass).Module;

@@ -4132,8 +4181,9 @@ namespace Microsoft.Dafny {
           var obj = SaveInTemp(etran.TrExpr(fse.Obj), rhsCanAffectPreviouslyKnownExpressions,

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

           prevObj[i] = obj;

+          // ^^^ this is where LHS are checked.

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

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

 

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

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

@@ -4163,8 +4213,9 @@ namespace Microsoft.Dafny {
             "$index" + i, predef.FieldName(tok, predef.BoxType), builder, locals);

           prevObj[i] = obj;

           prevIndex[i] = fieldName;

+            // ^^^ this may not need to be changed.

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

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

 

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

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

@@ -4195,7 +4246,7 @@ namespace Microsoft.Dafny {
             "$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"));

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

 

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

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

@@ -4376,6 +4427,7 @@ namespace Microsoft.Dafny {
       public readonly PredefinedDecls predef;

       public readonly Translator translator;

       public readonly string This;

+      public readonly string modifiesFrame = "$_Frame"; // the name of the context's frame variable.

       readonly Function applyLimited_CurrentFunction;

       readonly int layerOffset = 0;

       public int Statistics_FunctionCount = 0;

@@ -4420,18 +4472,34 @@ namespace Microsoft.Dafny {
         this.HeapExpr = heap;

         this.This = thisVar;

       }

-      

-      ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, Function applyLimited_CurrentFunction, int layerOffset) {

-        Contract.Requires(translator != null);

-        Contract.Requires(predef != null);

-        Contract.Requires(heap != null);

-        Contract.Requires(applyLimited_CurrentFunction != null);

-        this.translator = translator;

-        this.predef = predef;

-        this.HeapExpr = heap;

-        this.applyLimited_CurrentFunction = applyLimited_CurrentFunction;

-        this.This = "this";

-        this.layerOffset = layerOffset;

+

+      ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, Function applyLimited_CurrentFunction, int layerOffset)

+      {

+          Contract.Requires(translator != null);

+          Contract.Requires(predef != null);

+          Contract.Requires(heap != null);

+          Contract.Requires(applyLimited_CurrentFunction != null);

+          this.translator = translator;

+          this.predef = predef;

+          this.HeapExpr = heap;

+          this.applyLimited_CurrentFunction = applyLimited_CurrentFunction;

+          this.This = "this";

+          this.layerOffset = layerOffset;

+      }

+      //^^^ this needs to be checked.

+      public ExpressionTranslator(ExpressionTranslator etran, string modifiesFrame)

+      {

+          Contract.Requires(etran != null);

+          Contract.Requires(modifiesFrame != null);

+          this.translator = etran.translator;

+          this.HeapExpr = etran.HeapExpr;

+          this.predef = etran.predef;

+          this.This = etran.This;

+          this.applyLimited_CurrentFunction = etran.applyLimited_CurrentFunction;

+          this.layerOffset = etran.layerOffset;

+          this.Statistics_FunctionCount = etran.Statistics_FunctionCount;

+          this.oldEtran = etran.oldEtran;

+          this.modifiesFrame = modifiesFrame;

       }

 

       ExpressionTranslator oldEtran;

@@ -4476,7 +4544,7 @@ namespace Microsoft.Dafny {
         Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "beta");

         Bpl.Type fieldAlpha = predef.FieldName(tok, alpha);

         Bpl.Type ty = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.TypeSeq(predef.RefType, fieldAlpha), Bpl.Type.Bool);

-        return new Bpl.IdentifierExpr(tok, "$_Frame", ty);

+        return new Bpl.IdentifierExpr(tok, this.modifiesFrame ?? "$_Frame", ty);

       }

 

       public Bpl.IdentifierExpr Tick() {

@@ -5941,11 +6009,12 @@ namespace Microsoft.Dafny {
 

     static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {

       Contract.Requires(expr != null);

+      Contract.Requires(receiverReplacement != null);

       Contract.Requires(cce.NonNullDictionaryAndValues(substMap));

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

 

       Expression newExpr = null;  // set to non-null value only if substitution has any effect; if non-null, newExpr will be resolved at end

-      

+

       if (expr is LiteralExpr || expr is WildcardExpr || expr is BoogieWrapper) {

         // nothing to substitute

       } else if (expr is ThisExpr) {

@@ -6103,8 +6172,10 @@ namespace Microsoft.Dafny {
     static List<Expression/*!*/>/*!*/ SubstituteExprList(List<Expression/*!*/>/*!*/ elist,

                                                  Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {

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

-      Contract.Requires(cce.NonNullDictionaryAndValues(substMap));

+      Contract.Requires((receiverReplacement == null) == (substMap == null));

+      Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap));

       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Expression>>()));

+      

       List<Expression> newElist = null;  // initialized lazily

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

       {cce.LoopInvariant(  newElist == null || newElist.Count == i);