Added initial support for dirty while statements.

10 files changed, 405 insertions, 349 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 9d2cad2f..0c670062 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1120,6 +1120,11 @@ namespace Microsoft.Dafny {
           if (s.Body == null) {

             compiler.Error("a forall statement without a body cannot be compiled (line {0})", stmt.Tok.line);

           }

+        } else if (stmt is WhileStmt) {

+          var s = (WhileStmt)stmt;

+          if (s.Body == null) {

+            compiler.Error("a while statement without a body cannot be compiled (line {0})", stmt.Tok.line);

+          }

         }

       }

     }

@@ -1388,6 +1393,9 @@ namespace Microsoft.Dafny {
 

       } else if (stmt is WhileStmt) {

         WhileStmt s = (WhileStmt)stmt;

+        if (s.Body == null) {

+          return;

+        }

         if (s.Guard == null) {

           Indent(indent);

           wr.WriteLine("while (false) { }");

@@ -2515,7 +2523,7 @@ namespace Microsoft.Dafny {
             var rhsName = string.Format("_pat_let{0}_{1}", GetUniqueAstNumber(e), i);

             wr.Write("Dafny.Helpers.Let<");

             wr.Write(TypeName(e.RHSs[i].Type) + "," + TypeName(e.Body.Type));

-            wr.Write(">("); 

+            wr.Write(">(");

             TrExpr(e.RHSs[i]);

             wr.Write(", " + rhsName + " => ");

             neededCloseParens++;

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 18ac5e16..690f8403 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1407,6 +1407,7 @@ WhileStmt<out Statement/*!*/ stmt>
      IToken bodyStart = null, bodyEnd = null, endTok = Token.NoToken;

      List<GuardedAlternative> alternatives;

      stmt = dummyStmt;  // to please the compiler

+     bool isDirtyLoop = true;

   .)

   "while"                    (. x = t; .)

   (

@@ -1419,22 +1420,24 @@ WhileStmt<out Statement/*!*/ stmt>
     | "..."                      (. guardEllipsis = t; .)

     )

     LoopSpec<out invariants, out decreases, out mod, ref decAttrs, ref modAttrs>

-    ( BlockStmt<out body, out bodyStart, out bodyEnd>  (. endTok = body.EndTok; .)

-    | "..."                      (. bodyEllipsis = t; endTok = t; .)

-    )

+    [ BlockStmt<out body, out bodyStart, out bodyEnd>  (. endTok = body.EndTok; isDirtyLoop = false; .)

+    | "..."                      (. bodyEllipsis = t; endTok = t; isDirtyLoop = false; .)

+    ]

     (.

       if (guardEllipsis != null || bodyEllipsis != null) {

         if (mod != null) {

           SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");

         }

-        if (body == null) {

+        if (body == null && !isDirtyLoop) {

           body = new BlockStmt(x, endTok, new List<Statement>());

         }

         stmt = new WhileStmt(x, endTok, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(null, null), body);

         stmt = new SkeletonStatement(stmt, guardEllipsis, bodyEllipsis);

       } else {

         // The following statement protects against crashes in case of parsing errors

-        body = body ?? new BlockStmt(x, endTok, new List<Statement>());

+        if (body == null && !isDirtyLoop) {

+          body = new BlockStmt(x, endTok, new List<Statement>());

+        }

         stmt = new WhileStmt(x, endTok, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), body);

       }

     .)

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index fa7fde12..5b0e168e 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -714,7 +714,7 @@ namespace Microsoft.Dafny {
       s += Result.TypeName(context);

       return s;

     }

-   

+

     public override bool SupportsEquality {

       get {

         return false;

@@ -3995,10 +3995,6 @@ namespace Microsoft.Dafny {
   {

     public readonly Expression Guard;

     public readonly BlockStmt Body;

-    [ContractInvariantMethod]

-    void ObjectInvariant() {

-      Contract.Invariant(Body != null);

-    }

 

     public WhileStmt(IToken tok, IToken endTok, Expression guard,

                      List<MaybeFreeExpression> invariants, Specification<Expression> decreases, Specification<FrameExpression> mod,

@@ -4006,14 +4002,15 @@ namespace Microsoft.Dafny {
       : base(tok, endTok, invariants, decreases, mod) {

       Contract.Requires(tok != null);

       Contract.Requires(endTok != null);

-      Contract.Requires(body != null);

       this.Guard = guard;

       this.Body = body;

     }

 

     public override IEnumerable<Statement> SubStatements {

       get {

-        yield return Body;

+        if (Body != null) {

+          yield return Body;

+        }

       }

     }

     public override IEnumerable<Expression> SubExpressions {

@@ -5361,7 +5358,7 @@ namespace Microsoft.Dafny {
     public readonly Expression Obj;

     public readonly string MemberName;

     public MemberDecl Member;          // filled in by resolution, will be a Field or Function

-    public List<Type> TypeApplication; 

+    public List<Type> TypeApplication;

       // If it is a function, it must have all its polymorphic variables applied

 

     [ContractInvariantMethod]

@@ -5539,7 +5536,7 @@ namespace Microsoft.Dafny {
       }

     }

 

-    public ApplyExpr(IToken tok, IToken openParen, Expression receiver, List<Expression> args) 

+    public ApplyExpr(IToken tok, IToken openParen, Expression receiver, List<Expression> args)

       : base(tok)

     {

       OpenParen = openParen;

@@ -6206,7 +6203,7 @@ namespace Microsoft.Dafny {
       }

     }

     public String Refresh(String s, ref int counter) {

-      return s + "#" + counter++ + FullName; 

+      return s + "#" + counter++ + FullName;

     }

     public TypeParameter Refresh(TypeParameter p, ref int counter) {

       var cp = new TypeParameter(p.tok, counter++ + "#" + p.Name, p.EqualitySupport);

@@ -6312,13 +6309,13 @@ namespace Microsoft.Dafny {
     public readonly List<FrameExpression> Reads;

 

     public string MkName(string nm) {

-      return "$l" + lamUniques++ + "#" + nm; 

+      return "$l" + lamUniques++ + "#" + nm;

     }

 

     public LambdaExpr(IToken tok, bool oneShot, List<BoundVar> bvars, Expression requires, List<FrameExpression> reads, Expression body)

-      : base(tok, bvars, requires, body, null) 

+      : base(tok, bvars, requires, body, null)

     {

-      Contract.Requires(reads != null); 

+      Contract.Requires(reads != null);

       Reads = reads;

       OneShot = oneShot;

     }

@@ -6739,13 +6736,13 @@ namespace Microsoft.Dafny {
   public class TypeExpr : ParensExpression

   {

     public readonly Type T;

-    public TypeExpr(IToken tok, Expression e, Type t) 

+    public TypeExpr(IToken tok, Expression e, Type t)

       : base(tok, e)

     {

       Contract.Requires(t != null);

       T = t;

     }

-    

+

     public static Expression MaybeTypeExpr(Expression e, Type t) {

       if (t == null) {

         return e;

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index db32e726..f990f9ff 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -2115,6 +2115,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken bodyStart = null, bodyEnd = null, endTok = Token.NoToken;

 		List<GuardedAlternative> alternatives;

 		stmt = dummyStmt;  // to please the compiler

+		bool isDirtyLoop = true;

 		

 		Expect(87);

 		x = t; 

@@ -2131,29 +2132,33 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				guardEllipsis = t; 

 			}

 			LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);

-			if (la.kind == 15) {

-				BlockStmt(out body, out bodyStart, out bodyEnd);

-				endTok = body.EndTok; 

-			} else if (la.kind == 45) {

-				Get();

-				bodyEllipsis = t; endTok = t; 

-			} else SynErr(182);

+			if (la.kind == 15 || la.kind == 45) {

+				if (la.kind == 15) {

+					BlockStmt(out body, out bodyStart, out bodyEnd);

+					endTok = body.EndTok; isDirtyLoop = false; 

+				} else {

+					Get();

+					bodyEllipsis = t; endTok = t; isDirtyLoop = false; 

+				}

+			}

 			if (guardEllipsis != null || bodyEllipsis != null) {

 			 if (mod != null) {

 			   SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");

 			 }

-			 if (body == null) {

+			 if (body == null && !isDirtyLoop) {

 			   body = new BlockStmt(x, endTok, new List<Statement>());

 			 }

 			 stmt = new WhileStmt(x, endTok, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(null, null), body);

 			 stmt = new SkeletonStatement(stmt, guardEllipsis, bodyEllipsis);

 			} else {

 			 // The following statement protects against crashes in case of parsing errors

-			 body = body ?? new BlockStmt(x, endTok, new List<Statement>());

+			 if (body == null && !isDirtyLoop) {

+			   body = new BlockStmt(x, endTok, new List<Statement>());

+			 }

 			 stmt = new WhileStmt(x, endTok, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), body);

 			}

 			

-		} else SynErr(183);

+		} else SynErr(182);

 	}

 

 	void MatchStmt(out Statement/*!*/ s) {

@@ -2177,7 +2182,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(16);

 		} else if (StartOf(22)) {

 			if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); } 

-		} else SynErr(184);

+		} else SynErr(183);

 		s = new MatchStmt(x, t, e, cases, usesOptionalBrace); 

 	}

 

@@ -2203,7 +2208,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			x = t;

 			errors.Warning(t, "the 'parallel' keyword has been deprecated; the comprehension statement now uses the keyword 'forall' (and the parentheses around the bound variables are now optional)");

 			

-		} else SynErr(185);

+		} else SynErr(184);

 		if (la.kind == 17) {

 			Get();

 			usesOptionalParen = true; 

@@ -2221,7 +2226,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(18);

 		} else if (StartOf(23)) {

 			if (usesOptionalParen) { SemErr(t, "expecting close parenthesis"); } 

-		} else SynErr(186);

+		} else SynErr(185);

 		while (la.kind == 54 || la.kind == 55) {

 			isFree = false; 

 			if (la.kind == 54) {

@@ -2339,10 +2344,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		if (la.kind == 15) {

 			BlockStmt(out body, out bodyStart, out endTok);

 		} else if (la.kind == 10) {

-			while (!(la.kind == 0 || la.kind == 10)) {SynErr(187); Get();}

+			while (!(la.kind == 0 || la.kind == 10)) {SynErr(186); Get();}

 			Get();

 			endTok = t; 

-		} else SynErr(188);

+		} else SynErr(187);

 		s = new ModifyStmt(tok, endTok, mod, attrs, body);

 		if (ellipsisToken != null) {

 		 s = new SkeletonStatement(s, ellipsisToken, null);

@@ -2362,7 +2367,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 57) {

 			Get();

 			returnTok = t; isYield = true; 

-		} else SynErr(189);

+		} else SynErr(188);

 		if (StartOf(26)) {

 			Rhs(out r, null);

 			rhss = new List<AssignmentRhs>(); rhss.Add(r); 

@@ -2464,7 +2469,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (StartOf(17)) {

 			Expression(out e, false, true);

 			r = new ExprRhs(e); 

-		} else SynErr(190);

+		} else SynErr(189);

 		while (la.kind == 15) {

 			Attribute(ref attrs);

 		}

@@ -2486,7 +2491,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			while (la.kind == 69 || la.kind == 82) {

 				Suffix(ref e);

 			}

-		} else SynErr(191);

+		} else SynErr(190);

 	}

 

 	void Expressions(List<Expression/*!*/>/*!*/ args) {

@@ -2535,7 +2540,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (StartOf(17)) {

 			Expression(out ee, true, true);

 			e = ee; 

-		} else SynErr(192);

+		} else SynErr(191);

 	}

 

 	void LoopSpec(out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod, ref Attributes decAttrs, ref Attributes modAttrs) {

@@ -2551,7 +2556,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				OldSemi();

 				invariants.Add(invariant); 

 			} else if (la.kind == 56) {

-				while (!(la.kind == 0 || la.kind == 56)) {SynErr(193); Get();}

+				while (!(la.kind == 0 || la.kind == 56)) {SynErr(192); Get();}

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref decAttrs);

@@ -2559,7 +2564,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				DecreasesList(decreases, true);

 				OldSemi();

 			} else {

-				while (!(la.kind == 0 || la.kind == 53)) {SynErr(194); Get();}

+				while (!(la.kind == 0 || la.kind == 53)) {SynErr(193); Get();}

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref modAttrs);

@@ -2581,7 +2586,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void Invariant(out MaybeFreeExpression/*!*/ invariant) {

 		bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null; 

-		while (!(la.kind == 0 || la.kind == 54 || la.kind == 88)) {SynErr(195); Get();}

+		while (!(la.kind == 0 || la.kind == 54 || la.kind == 88)) {SynErr(194); Get();}

 		if (la.kind == 54) {

 			Get();

 			isFree = true;

@@ -2724,7 +2729,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			x = t;  binOp = BinaryExpr.Opcode.Exp; 

 			break;

 		}

-		default: SynErr(196); break;

+		default: SynErr(195); break;

 		}

 		if (k == null) {

 		 op = new Microsoft.Dafny.CalcStmt.BinaryCalcOp(binOp);

@@ -2761,7 +2766,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 104) {

 			Get();

-		} else SynErr(197);

+		} else SynErr(196);

 	}

 

 	void ImpliesOp() {

@@ -2769,7 +2774,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 106) {

 			Get();

-		} else SynErr(198);

+		} else SynErr(197);

 	}

 

 	void ExpliesOp() {

@@ -2777,7 +2782,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 108) {

 			Get();

-		} else SynErr(199);

+		} else SynErr(198);

 	}

 

 	void EquivExpression(out Expression e0, bool allowSemi, bool allowLambda) {

@@ -2962,7 +2967,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 110) {

 			Get();

-		} else SynErr(200);

+		} else SynErr(199);

 	}

 

 	void OrOp() {

@@ -2970,7 +2975,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 112) {

 			Get();

-		} else SynErr(201);

+		} else SynErr(200);

 	}

 

 	void Term(out Expression e0, bool allowSemi, bool allowLambda) {

@@ -3075,7 +3080,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			x = t;  op = BinaryExpr.Opcode.Ge; 

 			break;

 		}

-		default: SynErr(202); break;

+		default: SynErr(201); break;

 		}

 	}

 

@@ -3097,7 +3102,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 116) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Sub; 

-		} else SynErr(203);

+		} else SynErr(202);

 	}

 

 	void UnaryExpression(out Expression e, bool allowSemi, bool allowLambda) {

@@ -3155,7 +3160,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				MapComprehensionExpr(x, out e, allowSemi);

 			} else if (StartOf(32)) {

 				SemErr("map must be followed by literal in brackets or comprehension."); 

-			} else SynErr(204);

+			} else SynErr(203);

 			break;

 		}

 		case 2: case 3: case 4: case 6: case 7: case 9: case 17: case 61: case 62: case 120: case 121: case 122: case 123: case 124: case 125: {

@@ -3165,7 +3170,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			break;

 		}

-		default: SynErr(205); break;

+		default: SynErr(204); break;

 		}

 	}

 

@@ -3180,7 +3185,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 118) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Mod; 

-		} else SynErr(206);

+		} else SynErr(205);

 	}

 

 	void NegOp() {

@@ -3188,7 +3193,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 119) {

 			Get();

-		} else SynErr(207);

+		} else SynErr(206);

 	}

 

 	void EndlessExpression(out Expression e, bool allowSemi, bool allowLambda) {

@@ -3235,7 +3240,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			NamedExpr(out e, allowSemi, allowLambda);

 			break;

 		}

-		default: SynErr(208); break;

+		default: SynErr(207); break;

 		}

 	}

 

@@ -3377,7 +3382,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						multipleIndices.Add(ee);

 						

 					}

-				} else SynErr(209);

+				} else SynErr(208);

 			} else if (la.kind == 127) {

 				Get();

 				anyDots = true; 

@@ -3385,7 +3390,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Expression(out ee, true, true);

 					e1 = ee; 

 				}

-			} else SynErr(210);

+			} else SynErr(209);

 			if (multipleIndices != null) {

 			 e = new MultiSelectExpr(x, e, multipleIndices);

 			 // make sure an array class with this dimensionality exists

@@ -3426,7 +3431,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			

 			Expect(83);

-		} else SynErr(211);

+		} else SynErr(210);

 		ApplySuffix(ref e);

 	}

 

@@ -3463,7 +3468,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			e = new SeqDisplayExpr(x, elements); 

 			Expect(83);

-		} else SynErr(212);

+		} else SynErr(211);

 	}

 

 	void MultiSetExpr(out Expression e) {

@@ -3489,7 +3494,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(18);

 		} else if (StartOf(32)) {

 			SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); 

-		} else SynErr(213);

+		} else SynErr(212);

 	}

 

 	void MapDisplayExpr(IToken/*!*/ mapToken, out Expression e) {

@@ -3617,7 +3622,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			ParensExpression(out e, allowSemi, allowLambda);

 			break;

 		}

-		default: SynErr(214); break;

+		default: SynErr(213); break;

 		}

 	}

 

@@ -3646,7 +3651,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 n = BigInteger.Zero;

 			}

 			

-		} else SynErr(215);

+		} else SynErr(214);

 	}

 

 	void Dec(out Basetypes.BigDec d) {

@@ -3756,7 +3761,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 12) {

 			Get();

 			oneShot = true; 

-		} else SynErr(216);

+		} else SynErr(215);

 	}

 

 	void OptTypedExpr(out Expression e, out Type tt, bool allowSemi) {

@@ -3789,7 +3794,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 132) {

 			Get();

-		} else SynErr(217);

+		} else SynErr(216);

 	}

 

 	void MatchExpression(out Expression e, bool allowSemi, bool allowLambda) {

@@ -3812,7 +3817,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(16);

 		} else if (StartOf(32)) {

 			if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); } 

-		} else SynErr(218);

+		} else SynErr(217);

 		e = new MatchExpr(x, e, cases, usesOptionalBrace); 

 	}

 

@@ -3830,7 +3835,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 129 || la.kind == 130) {

 			Exists();

 			x = t; 

-		} else SynErr(219);

+		} else SynErr(218);

 		QuantifierDomain(out bvars, out attrs, out range);

 		QSep();

 		Expression(out body, allowSemi, allowLambda);

@@ -3878,7 +3883,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			AssumeStmt(out s);

 		} else if (la.kind == 95) {

 			CalcStmt(out s);

-		} else SynErr(220);

+		} else SynErr(219);

 	}

 

 	void LetExpr(out Expression e, bool allowSemi, bool allowLambda) {

@@ -3918,7 +3923,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 }

 			}

 			

-		} else SynErr(221);

+		} else SynErr(220);

 		Expression(out e, false, true);

 		letRHSs.Add(e); 

 		while (la.kind == 38) {

@@ -3969,7 +3974,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			IdentTypeOptional(out bv);

 			pat = new CasePattern(bv.tok, bv);

 			

-		} else SynErr(222);

+		} else SynErr(221);

 		if (pat == null) {

 		 pat = new CasePattern(t, "_ParseError", new List<CasePattern>());

 		}

@@ -4006,7 +4011,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 128) {

 			Get();

-		} else SynErr(223);

+		} else SynErr(222);

 	}

 

 	void Exists() {

@@ -4014,7 +4019,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 130) {

 			Get();

-		} else SynErr(224);

+		} else SynErr(223);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

@@ -4290,48 +4295,47 @@ public class Errors {
 			case 180: s = "invalid IfStmt"; break;

 			case 181: s = "invalid IfStmt"; break;

 			case 182: s = "invalid WhileStmt"; break;

-			case 183: s = "invalid WhileStmt"; break;

-			case 184: s = "invalid MatchStmt"; break;

+			case 183: s = "invalid MatchStmt"; break;

+			case 184: s = "invalid ForallStmt"; break;

 			case 185: s = "invalid ForallStmt"; break;

-			case 186: s = "invalid ForallStmt"; break;

-			case 187: s = "this symbol not expected in ModifyStmt"; break;

-			case 188: s = "invalid ModifyStmt"; break;

-			case 189: s = "invalid ReturnStmt"; break;

-			case 190: s = "invalid Rhs"; break;

-			case 191: s = "invalid Lhs"; break;

-			case 192: s = "invalid Guard"; break;

+			case 186: s = "this symbol not expected in ModifyStmt"; break;

+			case 187: s = "invalid ModifyStmt"; break;

+			case 188: s = "invalid ReturnStmt"; break;

+			case 189: s = "invalid Rhs"; break;

+			case 190: s = "invalid Lhs"; break;

+			case 191: s = "invalid Guard"; break;

+			case 192: s = "this symbol not expected in LoopSpec"; break;

 			case 193: s = "this symbol not expected in LoopSpec"; break;

-			case 194: s = "this symbol not expected in LoopSpec"; break;

-			case 195: s = "this symbol not expected in Invariant"; break;

-			case 196: s = "invalid CalcOp"; break;

-			case 197: s = "invalid EquivOp"; break;

-			case 198: s = "invalid ImpliesOp"; break;

-			case 199: s = "invalid ExpliesOp"; break;

-			case 200: s = "invalid AndOp"; break;

-			case 201: s = "invalid OrOp"; break;

-			case 202: s = "invalid RelOp"; break;

-			case 203: s = "invalid AddOp"; break;

+			case 194: s = "this symbol not expected in Invariant"; break;

+			case 195: s = "invalid CalcOp"; break;

+			case 196: s = "invalid EquivOp"; break;

+			case 197: s = "invalid ImpliesOp"; break;

+			case 198: s = "invalid ExpliesOp"; break;

+			case 199: s = "invalid AndOp"; break;

+			case 200: s = "invalid OrOp"; break;

+			case 201: s = "invalid RelOp"; break;

+			case 202: s = "invalid AddOp"; break;

+			case 203: s = "invalid UnaryExpression"; break;

 			case 204: s = "invalid UnaryExpression"; break;

-			case 205: s = "invalid UnaryExpression"; break;

-			case 206: s = "invalid MulOp"; break;

-			case 207: s = "invalid NegOp"; break;

-			case 208: s = "invalid EndlessExpression"; break;

+			case 205: s = "invalid MulOp"; break;

+			case 206: s = "invalid NegOp"; break;

+			case 207: s = "invalid EndlessExpression"; break;

+			case 208: s = "invalid Suffix"; break;

 			case 209: s = "invalid Suffix"; break;

 			case 210: s = "invalid Suffix"; break;

-			case 211: s = "invalid Suffix"; break;

-			case 212: s = "invalid DisplayExpr"; break;

-			case 213: s = "invalid MultiSetExpr"; break;

-			case 214: s = "invalid ConstAtomExpression"; break;

-			case 215: s = "invalid Nat"; break;

-			case 216: s = "invalid LambdaArrow"; break;

-			case 217: s = "invalid QSep"; break;

-			case 218: s = "invalid MatchExpression"; break;

-			case 219: s = "invalid QuantifierGuts"; break;

-			case 220: s = "invalid StmtInExpr"; break;

-			case 221: s = "invalid LetExpr"; break;

-			case 222: s = "invalid CasePattern"; break;

-			case 223: s = "invalid Forall"; break;

-			case 224: s = "invalid Exists"; break;

+			case 211: s = "invalid DisplayExpr"; break;

+			case 212: s = "invalid MultiSetExpr"; break;

+			case 213: s = "invalid ConstAtomExpression"; break;

+			case 214: s = "invalid Nat"; break;

+			case 215: s = "invalid LambdaArrow"; break;

+			case 216: s = "invalid QSep"; break;

+			case 217: s = "invalid MatchExpression"; break;

+			case 218: s = "invalid QuantifierGuts"; break;

+			case 219: s = "invalid StmtInExpr"; break;

+			case 220: s = "invalid LetExpr"; break;

+			case 221: s = "invalid CasePattern"; break;

+			case 222: s = "invalid Forall"; break;

+			case 223: s = "invalid Exists"; break;

 

 			default: s = "error " + n; break;

 		}

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 3b1c018c..9e569ef1 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -595,7 +595,7 @@ namespace Microsoft.Dafny {
       }

     }

 

-    internal void PrintDecreasesSpec(Specification<Expression> decs, int indent) {

+    internal void PrintDecreasesSpec(Specification<Expression> decs, int indent, bool newLine = true) {

       Contract.Requires(decs != null);

       if (printMode == DafnyOptions.PrintModes.NoGhost) { return; }

       if (decs.Expressions != null && decs.Expressions.Count != 0) {

@@ -607,11 +607,15 @@ namespace Microsoft.Dafny {
         }

         wr.Write(" ");

         PrintExpressionList(decs.Expressions, true);

-        wr.WriteLine(";");

+        if (newLine) {

+          wr.WriteLine(";");

+        } else {

+          wr.Write(";");

+        }

       }

     }

 

-    internal void PrintFrameSpecLine(string kind, List<FrameExpression/*!*/> ee, int indent, Attributes attrs) {

+    internal void PrintFrameSpecLine(string kind, List<FrameExpression/*!*/> ee, int indent, Attributes attrs, bool newLine = true) {

       Contract.Requires(kind != null);

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

       if (ee != null && ee.Count != 0) {

@@ -622,7 +626,11 @@ namespace Microsoft.Dafny {
         }

         wr.Write(" ");

         PrintFrameExpressionList(ee);

-        wr.WriteLine(";");

+        if (newLine) {

+          wr.WriteLine(";");

+        } else {

+          wr.Write(";");

+        }

       }

     }

 

@@ -1047,15 +1055,15 @@ namespace Microsoft.Dafny {
         wr.WriteLine();

       }

 

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

-      PrintDecreasesSpec(s.Decreases, indent + IndentAmount);

+      PrintSpec("invariant", s.Invariants, indent + IndentAmount, s.Body != null || omitBody || (s.Decreases.Expressions != null && s.Decreases.Expressions.Count != 0) || (s.Mod.Expressions != null && s.Mod.Expressions.Count != 0));

+      PrintDecreasesSpec(s.Decreases, indent + IndentAmount, s.Body != null || omitBody || (s.Mod.Expressions != null && s.Mod.Expressions.Count != 0));

       if (s.Mod.Expressions != null) {

-        PrintFrameSpecLine("modifies", s.Mod.Expressions, indent + IndentAmount, s.Mod.HasAttributes() ? s.Mod.Attributes : null);

+        PrintFrameSpecLine("modifies", s.Mod.Expressions, indent + IndentAmount, s.Mod.HasAttributes() ? s.Mod.Attributes : null, s.Body != null || omitBody);

       }

       Indent(indent);

       if (omitBody) {

         wr.WriteLine("...;");

-      } else {

+      } else if (s.Body != null) {

         PrintStatement(s.Body, indent);

       }

     }

@@ -1414,7 +1422,7 @@ namespace Microsoft.Dafny {
         var e = (ApplyExpr)expr;

         // determine if parens are needed

         int opBindingStrength = 0x70;

-        bool parensNeeded = 

+        bool parensNeeded =

           opBindingStrength < contextBindingStrength ||

           (fragileContext && opBindingStrength == contextBindingStrength);

 

@@ -1424,7 +1432,7 @@ namespace Microsoft.Dafny {
         wr.Write("(");

         PrintExpressionList(e.Args, false);

         wr.Write(")");

-        

+

         if (parensNeeded) { wr.Write(")"); }

 

       } else if (expr is FunctionCallExpr) {

@@ -1453,7 +1461,7 @@ namespace Microsoft.Dafny {
           PrintActualArguments(e.Args, e.Name);

         }

         if (parensNeeded) { wr.Write(")"); }

- 

+

       } else if (expr is OldExpr) {

         wr.Write("old(");

         PrintExpression(((OldExpr)expr).E, false);

@@ -1660,7 +1668,7 @@ namespace Microsoft.Dafny {
         bool parensNeeded = !isRightmost;

         if (parensNeeded) { wr.Write("("); }

         wr.Write(e is ForallExpr ? "forall" : "exists");

-        PrintTypeParams(e.TypeArgs); // new! 

+        PrintTypeParams(e.TypeArgs); // new!

         wr.Write(" ");

         PrintQuantifierDomain(e.BoundVars, e.Attributes, e.Range);

         wr.Write(" :: ");

@@ -1716,7 +1724,7 @@ namespace Microsoft.Dafny {
         wr.Write(" :: ");

         PrintExpression(e.Term, !parensNeeded && isFollowedBySemicolon);

         if (parensNeeded) { wr.Write(")"); }

-       

+

       } else if (expr is LambdaExpr) {

         var e = (LambdaExpr)expr;

         wr.Write("(");

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 818bdcc4..757995f2 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -151,7 +151,7 @@ namespace Microsoft.Dafny
     readonly Graph<ModuleDecl> dependencies = new Graph<ModuleDecl>();

     private ModuleSignature systemNameInfo = null;

     private bool useCompileSignatures = false;

-    private RefinementTransformer refinementTransformer = null; 

+    private RefinementTransformer refinementTransformer = null;

 

     public Resolver(Program prog) {

       Contract.Requires(prog != null);

@@ -502,17 +502,17 @@ namespace Microsoft.Dafny
         var obj = new IdentifierExpr(e.tok, oVar.Name) { Type = oVar.Type, Var = oVar };

         bvars.Add(oVar);

 

-        return 

+        return

           new SetComprehension(e.tok, bvars,

             new BinaryExpr(e.tok, BinaryExpr.Opcode.In, obj,

-              new ApplyExpr(e.tok, e.tok, e, bexprs) 

+              new ApplyExpr(e.tok, e.tok, e, bexprs)

               {

                 Type = new SetType(new ObjectType())

-              }) 

+              })

             {

               ResolvedOp = BinaryExpr.ResolvedOpcode.InSet,

               Type = Type.Bool

-            }, obj) 

+            }, obj)

           {

             Type = new SetType(new ObjectType())

           };

@@ -1212,7 +1212,7 @@ namespace Microsoft.Dafny
       int prevErrorCount = ErrorCount;

 

       // Resolve the meat of classes and iterators, the definitions of type synonyms, and the type parameters of all top-level type declarations

-      // First, resolve the newtype declarations and the constraint clauses, including filling in .ResolvedOp fields.  This is needed for the 

+      // First, resolve the newtype declarations and the constraint clauses, including filling in .ResolvedOp fields.  This is needed for the

       // resolution of the other declarations, because those other declarations may invoke DiscoverBounds, which looks at the .Constraint field

       // of any newtypes involved.  DiscoverBounds is called on quantifiers (but only in non-ghost contexts) and set comprehensions (in all

       // contexts).  The constraints of newtypes are ghost, so DiscoverBounds is not going to be called on any quantifiers they may contain.

@@ -1497,7 +1497,7 @@ namespace Microsoft.Dafny
                         if (InferRequiredEqualitySupport(tp, p.Type)) {

                           tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;

                           done = true;

-                          break; 

+                          break;

                         }

                       }

                       foreach (var p in m.Outs) {

@@ -2027,7 +2027,10 @@ namespace Microsoft.Dafny
         return status;

       } else if (stmt is WhileStmt) {

         var s = (WhileStmt)stmt;

-        var status = CheckTailRecursive(s.Body, enclosingMethod, ref tailCall, reportErrors);

+        var status = TailRecursionStatus.NotTailRecursive;

+        if (s.Body != null) {

+          status = CheckTailRecursive(s.Body, enclosingMethod, ref tailCall, reportErrors);

+        }

         if (status != TailRecursionStatus.CanBeFollowedByAnything) {

           if (status == TailRecursionStatus.NotTailRecursive) {

             // an error has already been reported

@@ -2295,7 +2298,10 @@ namespace Microsoft.Dafny
           if (s.Guard != null) {

             Visit(s.Guard, st);

           }

-          Visit(s.Body, st);

+          // don't recurse on the body, if it's a dirty loop

+          if (s.Body != null) {

+            Visit(s.Body, st);

+          }

           return false;

         } else if (stmt is AlternativeLoopStmt) {

           var s = (AlternativeLoopStmt)stmt;

@@ -2364,7 +2370,7 @@ namespace Microsoft.Dafny
                 Error(e.E0, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t0, TypeEqualityErrorMessageHint(t0));

               } else if (!t1.SupportsEquality) {

                 Error(e.E1, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t1, TypeEqualityErrorMessageHint(t1));

-              } 

+              }

               break;

             default:

               switch (e.ResolvedOp) {

@@ -3888,7 +3894,7 @@ namespace Microsoft.Dafny
                   // detect self-loops here, since they don't show up in the graph's SSC methods

                   Error(dd.tok, "recursive dependency involving a newtype: {0} -> {0}", dd.Name);

                 }

-              }                

+              }

               what = "newtype";

               t.ResolvedClass = dd;

             } else {

@@ -4750,13 +4756,15 @@ namespace Microsoft.Dafny
           }

         }

         s.IsGhost = bodyMustBeSpecOnly;

-        loopStack.Add(s);  // push

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

-          inSpecOnlyContext.Add(s, specContextOnly);

-        }

+        if (s.Body != null) {

+          loopStack.Add(s);  // push

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

+            inSpecOnlyContext.Add(s, specContextOnly);

+          }

 

-        ResolveStatement(s.Body, bodyMustBeSpecOnly, codeContext);

-        loopStack.RemoveAt(loopStack.Count - 1);  // pop

+          ResolveStatement(s.Body, bodyMustBeSpecOnly, codeContext);

+          loopStack.RemoveAt(loopStack.Count - 1);  // pop

+        }

 

       } else if (stmt is AlternativeLoopStmt) {

         var s = (AlternativeLoopStmt)stmt;

@@ -5111,7 +5119,6 @@ namespace Microsoft.Dafny
       var update = s as UpdateStmt;

 

       var lhsNameSet = new HashSet<string>();  // used to check for duplicate identifiers on the left (full duplication checking for references and the like is done during verification)

-      var i = 0;

       foreach (var lhs in s.Lhss) {

         var ec = ErrorCount;

         ResolveExpression(lhs, new ResolveOpts(codeContext, true));

@@ -5627,7 +5634,9 @@ namespace Microsoft.Dafny
 

       } else if (stmt is WhileStmt) {

         WhileStmt s = (WhileStmt)stmt;

-        CheckForallStatementBodyRestrictions(s.Body, kind);

+        if (s.Body != null) {

+          CheckForallStatementBodyRestrictions(s.Body, kind);

+        }

 

       } else if (stmt is AlternativeLoopStmt) {

         var s = (AlternativeLoopStmt)stmt;

@@ -5746,7 +5755,9 @@ namespace Microsoft.Dafny
         if (s.Mod.Expressions != null && s.Mod.Expressions.Count != 0) {

           Error(s.Mod.Expressions[0].tok, "a while statement used inside a hint is not allowed to have a modifies clause");

         }

-        CheckHintRestrictions(s.Body);

+        if (s.Body != null) {

+          CheckHintRestrictions(s.Body);

+        }

 

       } else if (stmt is AlternativeLoopStmt) {

         var s = (AlternativeLoopStmt)stmt;

@@ -5910,7 +5921,7 @@ namespace Microsoft.Dafny
         Contract.Assert(ctype.TypeArgs.Count == cd.TypeArgs.Count);  // follows from the fact that ctype was resolved

 #if TWO_SEARCHES

         MemberDecl member = cd.Members.Find(md => md.Name == memberName);

-        if (member == null && 

+        if (member == null &&

           (!classMembers.ContainsKey(cd) || !classMembers[cd].TryGetValue(memberName, out member))) {

 #else

         MemberDecl member;

@@ -6317,7 +6328,7 @@ namespace Microsoft.Dafny
         if (resolved == null) {

           // error has already been reported by ResolvePredicateOrField

         } else {

-          // the following will cause e.Obj to be resolved again, but that's still correct 

+          // the following will cause e.Obj to be resolved again, but that's still correct

           e.ResolvedExpression = resolved;

           ResolveExpression(e.ResolvedExpression, opts);

           e.Type = e.ResolvedExpression.Type;

@@ -6347,7 +6358,7 @@ namespace Microsoft.Dafny
           }

           foreach (var tp in fn.TypeArgs) {

             Type prox = new InferredTypeProxy();

-            subst[tp] = prox; 

+            subst[tp] = prox;

             e.TypeApplication.Add(prox);

           }

           e.Type = new ArrowType(fn.tok, fn.Formals.ConvertAll(f => SubstType(f.Type, subst)), SubstType(fn.ResultType, subst), builtIns.SystemModule);

@@ -6479,7 +6490,7 @@ namespace Microsoft.Dafny
                 foreach (Formal d in ctor.Formals) {

                   if (d == destructor.CorrespondingFormal) {

                     ctor_args.Add(e.Value);

-                  } else {                    

+                  } else {

                     ctor_args.Add(new ExprDotName(expr.tok, tmpVarIdExpr, d.Name));

                   }

                 }

@@ -7449,7 +7460,7 @@ namespace Microsoft.Dafny
       if (field != null) {

         if (field.Type.IsArrowType || field.Type.IsTypeParameter) {

           return new ApplyExpr(tok, openParen, new ExprDotName(tok, receiver, fn), args);

-        } 

+        }

       }

       return new FunctionCallExpr(tok, fn, receiver, openParen, args);

     }

@@ -7875,12 +7886,12 @@ namespace Microsoft.Dafny
             ResolveExpression(arg, opts);

           }

         }

-      } 

+      }

       return r;

     }

 

     /// <summary>

-    /// Resolves "obj . suffixName" to a member select expression, 

+    /// Resolves "obj . suffixName" to a member select expression,

     /// Expects "obj" already to have been resolved.

     /// On success, returns the result of the resolution--as an un-resolved expression.

     /// On failure, returns null (in which case an error has been reported to the user).

@@ -8380,7 +8391,7 @@ namespace Microsoft.Dafny
           s.UnionWith(t);

         }

         return s;

-       

+

       } else if (expr is LambdaExpr) {

         var e = (LambdaExpr)expr;

         var s = FreeVariables(e.Term);

@@ -8753,7 +8764,7 @@ namespace Microsoft.Dafny
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression

       }

 }

-    

+

 

     /// <summary>

     /// This method adds to "coConclusions" all copredicate calls and codatatype equalities that occur

diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index ca72e221..06493434 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -299,7 +299,7 @@ public class Scanner {
 	}

 

 //	[NotDelayed]

-	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() {

+	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler, bool useBaseName = false) : base() {

 	  Contract.Requires(fileName != null);

 	  Contract.Requires(errorHandler != null);

 		this.errorHandler = errorHandler;

@@ -308,7 +308,7 @@ public class Scanner {
 		try {

 			Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);

 			buffer = new Buffer(stream, false);

-			Filename = fileName;

+			Filename = useBaseName? GetBaseName(fileName): fileName;

 			Init();

 		} catch (IOException) {

 			throw new FatalError("Cannot open file " + fileName);

@@ -316,7 +316,7 @@ public class Scanner {
 	}

 

 //	[NotDelayed]

-	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() {

+	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName, bool useBaseName = false) : base() {

 	  Contract.Requires(s != null);

 	  Contract.Requires(errorHandler != null);

 	  Contract.Requires(fileName != null);

@@ -324,10 +324,14 @@ public class Scanner {
 		t = new Token(); // dummy because t is a non-null field

 		buffer = new Buffer(s, true);

 		this.errorHandler = errorHandler;

-		this.Filename = fileName;

+		this.Filename = useBaseName? GetBaseName(fileName) : fileName;

 		Init();

 	}

 

+    string GetBaseName(string fileName) {

+        return System.IO.Path.GetFileName(fileName); // Return basename

+    }

+

 	void Init() {

 		pos = -1; line = 1; col = 0;

 		oldEols = 0;

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 0a83499c..ecc2ff56 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -276,7 +276,7 @@ namespace Microsoft.Dafny {
           Bpl.Constant c = (Bpl.Constant)d;

           if (c.Name == "alloc") {

             allocField = c;

-          } 

+          }

         } else if (d is Bpl.GlobalVariable) {

           Bpl.GlobalVariable v = (Bpl.GlobalVariable)d;

           if (v.Name == "$Heap") {

@@ -373,7 +373,7 @@ namespace Microsoft.Dafny {
     public Bpl.Program Translate(Program p) {

       Contract.Requires(p != null);

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

-      

+

       program = p;

 

       if (sink == null || predef == null) {

@@ -473,7 +473,7 @@ namespace Microsoft.Dafny {
     }

 

     //adding TraitParent function and axioms

-    //if a class A extends trait J and B does not extned anything, then this method adds the followings to the sink: 

+    //if a class A extends trait J and B does not extned anything, then this method adds the followings to the sink:

     //   const unique NoTraitAtAll: ClassName;

     //   function TraitParent(ClassName): ClassName;

     //   axiom TraitParent(class.A) == class.J;

@@ -618,7 +618,7 @@ namespace Microsoft.Dafny {
         int i;

 

         // Add:  function #dt.ctor(tyVars, paramTypes) returns (DatatypeType);

-        

+

         List<Bpl.Variable> argTypes = new List<Bpl.Variable>();

         foreach (Formal arg in ctor.Formals) {

           Bpl.Variable a = new Bpl.Formal(arg.tok, new Bpl.TypedIdent(arg.tok, Bpl.TypedIdent.NoName, TrType(arg.Type)), true);

@@ -642,7 +642,7 @@ namespace Microsoft.Dafny {
           sink.AddTopLevelDeclaration(cid);

 

           {

-            // Add:  axiom (forall params :: DatatypeCtorId(#dt.ctor(params)) == ##dt.ctor);       

+            // Add:  axiom (forall params :: DatatypeCtorId(#dt.ctor(params)) == ##dt.ctor);

             CreateBoundVariables(ctor.Formals, out bvs, out args);

             Bpl.Expr lhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);

             lhs = FunctionCall(ctor.tok, BuiltinFunction.DatatypeCtorId, null, lhs);

@@ -668,8 +668,8 @@ namespace Microsoft.Dafny {
           }

 

         }

-        

-        

+

+

         {

           // Add:  axiom (forall d: DatatypeType :: dt.ctor?(d) ==> (exists params :: d == #dt.ctor(params));

           CreateBoundVariables(ctor.Formals, out bvs, out args);

@@ -688,11 +688,11 @@ namespace Microsoft.Dafny {
           /*

             (forall x0 : C0, ..., xn : Cn, G : Ty •

               { $Is(C(x0,...,xn), T(G)) }

-              $Is(C(x0,...,xn), T(G)) <==> 

+              $Is(C(x0,...,xn), T(G)) <==>

               $Is[Box](x0, C0(G)) && ... && $Is[Box](xn, Cn(G)));

             (forall x0 : C0, ..., xn : Cn, G : Ty •

                 { $IsAlloc(C(G, x0,...,xn), T(G)) }

-                $IsAlloc(C(G, x0,...,xn), T(G)) ==> 

+                $IsAlloc(C(G, x0,...,xn), T(G)) ==>

                     $IsAlloc[Box](x0, C0(G)) && ... && $IsAlloc[Box](xn, Cn(G)));

           */

           List<Bpl.Expr> tyexprs;

@@ -737,14 +737,14 @@ namespace Microsoft.Dafny {
           foreach (Bpl.Expr arg in args) {

             litargs.Add(Lit(arg));

           }

-          Bpl.Expr lhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, litargs);                 

+          Bpl.Expr lhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, litargs);

           Bpl.Expr rhs = Lit(FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args), predef.DatatypeType);

           Bpl.Expr q = BplForall(bvs, BplTrigger(lhs), Bpl.Expr.Eq(lhs, rhs));

           sink.AddTopLevelDeclaration(new Bpl.Axiom(ctor.tok, q, "Constructor literal"));

-        }         

+        }

 

         // Injectivity axioms for normal arguments

-        i = 0; 

+        i = 0;

         foreach (Formal arg in ctor.Formals) {

           // function ##dt.ctor#i(DatatypeType) returns (Ti);

           var sf = ctor.Destructors[i];

@@ -752,7 +752,7 @@ namespace Microsoft.Dafny {
           fn = GetReadonlyField(sf);

           sink.AddTopLevelDeclaration(fn);

           // axiom (forall params :: ##dt.ctor#i(#dt.ctor(params)) == params_i);

-          CreateBoundVariables(ctor.Formals, out bvs, out args);         

+          CreateBoundVariables(ctor.Formals, out bvs, out args);

           var inner = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);

           var outer = FunctionCall(ctor.tok, fn.Name, TrType(arg.Type), inner);

           var q = BplForall(bvs, BplTrigger(inner), Bpl.Expr.Eq(outer, args[i]));

@@ -792,7 +792,7 @@ namespace Microsoft.Dafny {
               q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs)));

               sink.AddTopLevelDeclaration(new Bpl.Axiom(ctor.tok, q));

               // axiom (forall params, SeqRank(arg) < DtRank(#dt.ctor(params)));

-              CreateBoundVariables(ctor.Formals, out bvs, out args);             

+              CreateBoundVariables(ctor.Formals, out bvs, out args);

               lhs = FunctionCall(ctor.tok, BuiltinFunction.SeqRank, null, args[i]);

               rhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);

               rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);

@@ -829,7 +829,7 @@ namespace Microsoft.Dafny {
             }

           }

 

-          i++;          

+          i++;

         }

       }

 

@@ -905,8 +905,8 @@ namespace Microsoft.Dafny {
         };

 

         Action<bool, Action<Tuple<List<Type>, List<Type>>, List<Bpl.Variable>, List<Bpl.Expr>, List<Bpl.Expr>, Bpl.Variable, Bpl.Expr, Bpl.Expr, Bpl.Expr, Bpl.Expr, Bpl.Expr>> CoAxHelper = (add_k, K) => {

-          Func<string, List<TypeParameter>> renew = s => 

-            Map(codecl.TypeArgs, tp => 

+          Func<string, List<TypeParameter>> renew = s =>

+            Map(codecl.TypeArgs, tp =>

               new TypeParameter(tp.tok, tp.Name + "#" + s, tp.PositionalIndex, tp.Parent));

           List<TypeParameter> typaramsL = renew("l"), typaramsR = renew("r");

           List<Bpl.Expr> lexprs; var lvars = MkTyParamBinders(typaramsL, out lexprs);

@@ -924,9 +924,9 @@ namespace Microsoft.Dafny {
           } else {

             kVar = null; k = null; kGtZero = Bpl.Expr.True;

           }

-          var ly = BplBoundVar("ly", predef.LayerType, vars); 

+          var ly = BplBoundVar("ly", predef.LayerType, vars);

           var d0 = BplBoundVar("d0", predef.DatatypeType, vars);

-          var d1 = BplBoundVar("d1", predef.DatatypeType, vars); 

+          var d1 = BplBoundVar("d1", predef.DatatypeType, vars);

 

           K(tyargs, vars, lexprs, rexprs, kVar, k, kGtZero, ly, d0, d1);

         };

@@ -950,8 +950,8 @@ namespace Microsoft.Dafny {
             sink.AddTopLevelDeclaration(fn);

           }

 

-          // axiom (forall G0,...,Gn : Ty, k: int, ly : Layer, d0, d1: DatatypeType :: 

-          //  { Eq(G0, .., Gn, S(ly), k, d0, d1) } 

+          // axiom (forall G0,...,Gn : Ty, k: int, ly : Layer, d0, d1: DatatypeType ::

+          //  { Eq(G0, .., Gn, S(ly), k, d0, d1) }

           //  Is(d0, T(G0, .., Gn)) && Is(d1, T(G0, ... Gn)) ==>

           //  (Eq(G0, .., Gn, S(ly), k, d0, d1)

           //    <==>

@@ -969,8 +969,8 @@ namespace Microsoft.Dafny {
             sink.AddTopLevelDeclaration(new Bpl.Axiom(dt.tok, ax, "Layered co-equality axiom"));

           });

 

-          // axiom (forall G0,...,Gn : Ty, k: int, ly : Layer, d0, d1: DatatypeType :: 

-          //  { Eq(G0, .., Gn, S(ly), k, d0, d1) } 

+          // axiom (forall G0,...,Gn : Ty, k: int, ly : Layer, d0, d1: DatatypeType ::

+          //  { Eq(G0, .., Gn, S(ly), k, d0, d1) }

           //    0 < k ==>

           //      (Eq(G0, .., Gn, S(ly), k, d0, d1) <==>

           //       Eq(G0, .., Gn, ly, k, d0, d))

@@ -1059,7 +1059,7 @@ namespace Microsoft.Dafny {
       // produce with conjucts=false (default):

       //   (A.Nil? && B.Nil?) ||

       //   (A.Cons? && B.Cons? && A.head == B.head && Equal(k, A.tail, B.tail))

-      // 

+      //

       // with conjuncts=true:

       //   (A.Nil? ==> B.Nil?) &&

       //   (A.Cons? ==> (B.Cons? && A.head == B.head && Equal(k, A.tail, B.tail)))

@@ -1081,7 +1081,7 @@ namespace Microsoft.Dafny {
             var lexprs = Map(ty.TypeArgs, tt => Resolver.SubstType(tt, lsu));

             var rexprs = Map(ty.TypeArgs, tt => Resolver.SubstType(tt, rsu));

             q = CoEqualCall(codecl, lexprs, rexprs, k, l, a, b);

-          } else { 

+          } else {

             // ordinary equality; let the usual translation machinery figure out the translation

             var equal = new BinaryExpr(tok, BinaryExpr.Opcode.Eq, new BoogieWrapper(a, ty), new BoogieWrapper(b, ty));

             equal.ResolvedOp = Resolver.ResolveOp(equal.Op, ty);  // resolve here

@@ -1093,7 +1093,7 @@ namespace Microsoft.Dafny {
         if (conjuncts) {

           yield return Bpl.Expr.Binary(new NestedToken(tok, ctor.tok), BinaryOperator.Opcode.Imp, aq, BplAnd(bq, chunk));

         } else {

-          yield return BplAnd(BplAnd(aq, bq), BplImp(BplAnd(aq, bq), chunk));  

+          yield return BplAnd(BplAnd(aq, bq), BplImp(BplAnd(aq, bq), chunk));

         }

       }

     }

@@ -1121,7 +1121,7 @@ namespace Microsoft.Dafny {
         tok = A.tok;

       }

       List<Bpl.Expr> args = Concat(largs, rargs);

-      if (k != null) { 

+      if (k != null) {

         args.Add(k);

       }

       args.AddRange(new List<Bpl.Expr> { l, A, B });

@@ -1296,7 +1296,7 @@ namespace Microsoft.Dafny {
           var implement_intr = new Bpl.Function(c.tok, "implements$" + c.Name, new List<Variable> { arg_ref }, res);

           sink.AddTopLevelDeclaration(implement_intr);

       }

-      //this adds: axiom implements$J(class.C); 

+      //this adds: axiom implements$J(class.C);

       else if (c is ClassDecl)

       {

           if (c.Trait != null)

@@ -1312,7 +1312,7 @@ namespace Microsoft.Dafny {
               sink.AddTopLevelDeclaration(implements_axiom);

           }

       }

-       

+

       foreach (MemberDecl member in c.Members) {

         currentDeclaration = member;

         if (member is Field) {

@@ -1405,7 +1405,7 @@ namespace Microsoft.Dafny {
       if (f.Body != null && !IsOpaqueFunction(f)) {

         AddFunctionAxiom(f, FunctionAxiomVisibility.IntraModuleOnly, f.Body.Resolved);

         AddFunctionAxiom(f, FunctionAxiomVisibility.ForeignModuleOnly, f.Body.Resolved);

-      }  

+      }

       // for body-less functions, at least generate its #requires function

       if (f.Body == null) {

         var b = FunctionAxiom(f, FunctionAxiomVisibility.ForeignModuleOnly, null, null);

@@ -1562,7 +1562,7 @@ namespace Microsoft.Dafny {
       validCall.Function = iter.Member_Valid;  // resolve here

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

 

-      validCall.TypeArgumentSubstitutions = new Dictionary<TypeParameter, Type>();  

+      validCall.TypeArgumentSubstitutions = new Dictionary<TypeParameter, Type>();

       foreach (var p in iter.TypeArgs) {

         validCall.TypeArgumentSubstitutions[p] = new UserDefinedType(p);

       } // resolved here.

@@ -1871,8 +1871,8 @@ namespace Microsoft.Dafny {
       // the axiom.  Moreover, leaving it out does not introduce any soundness problem, because the Dafny

       // allocation statement changes only an allocation bit and then re-assumes $IsGoodHeap; so if it is

       // sound after that, then it would also have been sound just before the allocation.

-      //      

-      List<Bpl.Expr> tyargs;      

+      //

+      List<Bpl.Expr> tyargs;

       var formals = MkTyParamBinders(GetTypeParams(f), out tyargs);

       var args = new List<Bpl.Expr>();

       Bpl.BoundVariable layer;

@@ -1921,7 +1921,7 @@ namespace Microsoft.Dafny {
           var ly = new Bpl.IdentifierExpr(f.tok, layer);

           funcArgs.Add(FunctionCall(f.tok, BuiltinFunction.LayerSucc, null, ly));

         }

-        funcArgs.AddRange(args);        

+        funcArgs.AddRange(args);

         funcAppl = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(funcID), funcArgs);

       }

 

@@ -2016,7 +2016,7 @@ namespace Microsoft.Dafny {
       // where GOOD_PARAMETERS means:

       //   $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types &&

       //   Pre($Heap,formals)

-      // 

+      //

       // NOTE: this is lifted out to a #requires function for intra module calls,

       //       and used in the function pseudo-handles for top level functions.

       //       For body-less functions, this is emitted when body is null.

@@ -2041,8 +2041,8 @@ namespace Microsoft.Dafny {
 

       // quantify over the type arguments, and add them first to the arguments

       List<Bpl.Expr> args = new List<Bpl.Expr>();

-      List<Bpl.Expr> tyargs;      

-      var formals = MkTyParamBinders(GetTypeParams(f), out tyargs);          

+      List<Bpl.Expr> tyargs;

+      var formals = MkTyParamBinders(GetTypeParams(f), out tyargs);

 

       Bpl.BoundVariable layer;

       if (f.IsRecursive) {

@@ -2105,16 +2105,16 @@ namespace Microsoft.Dafny {
 

       // Add the precondition function and its axiom (which is equivalent to the ante)

       if (body == null || (visibility == FunctionAxiomVisibility.IntraModuleOnly && lits == null)) {

-        var precondF = new Bpl.Function(f.tok, 

-          RequiresName(f), new List<Bpl.TypeVariable>(), 

-          formals.ConvertAll(v => (Bpl.Variable)BplFormalVar(null, v.TypedIdent.Type, true)), 

+        var precondF = new Bpl.Function(f.tok,

+          RequiresName(f), new List<Bpl.TypeVariable>(),

+          formals.ConvertAll(v => (Bpl.Variable)BplFormalVar(null, v.TypedIdent.Type, true)),

           BplFormalVar(null, Bpl.Type.Bool, false));

         sink.AddTopLevelDeclaration(precondF);

-        var appl = FunctionCall(f.tok, RequiresName(f), Bpl.Type.Bool, 

+        var appl = FunctionCall(f.tok, RequiresName(f), Bpl.Type.Bool,

           formals.ConvertAll(x => (Bpl.Expr)(new Bpl.IdentifierExpr(f.tok, x))));

         sink.AddTopLevelDeclaration(new Axiom(f.tok, BplForall(formals, BplTrigger(appl), Bpl.Expr.Eq(appl, ante))));

         // you could use it to check that it always works, but it makes VSI-Benchmarks/b3.dfy time out:

-        // ante = appl; 

+        // ante = appl;

         if (body == null) {

           return null;

         }

@@ -2195,8 +2195,8 @@ namespace Microsoft.Dafny {
     Expression PrefixSubstitution(PrefixPredicate pp, Expression body) {

       Contract.Requires(pp != null);

 

-      var typeMap = Util.Dict<TypeParameter,Type>(pp.Co.TypeArgs, Map(pp.TypeArgs, x => new UserDefinedType(x))); 

-      

+      var typeMap = Util.Dict<TypeParameter,Type>(pp.Co.TypeArgs, Map(pp.TypeArgs, x => new UserDefinedType(x)));

+

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

       for (int i = 0; i < pp.Co.Formals.Count; i++) {

         var replacement = pp.Formals[i + 1];  // the +1 is to skip pp's _k parameter

@@ -2294,7 +2294,7 @@ namespace Microsoft.Dafny {
       var tok = pp.tok;

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

 

-      List<Bpl.Expr> tyexprs; 

+      List<Bpl.Expr> tyexprs;

       var tyvars = MkTyParamBinders(pp.TypeArgs, out tyexprs);

 

       var bvs = new List<Variable>(tyvars);

@@ -2356,9 +2356,9 @@ namespace Microsoft.Dafny {
           kWhere = wh;

         } else {

           bvs.Add(bv);

-          if (wh != null) { 

+          if (wh != null) {

             // add well-typedness conjunct to antecedent

-            ante = Bpl.Expr.And(ante, wh); 

+            ante = Bpl.Expr.And(ante, wh);

           }

         }

       }

@@ -2375,7 +2375,7 @@ namespace Microsoft.Dafny {
       var allK = new Bpl.ForallExpr(tok, new List<Variable> { k }, tr, BplImp(kWhere, prefixAppl));

       tr = new Bpl.Trigger(tok, true, new List<Bpl.Expr> { coAppl });

       var allS = new Bpl.ForallExpr(tok, bvs, tr, BplImp(BplAnd(ante, coAppl), allK));

-      sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, Bpl.Expr.Imp(activation, allS), 

+      sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, Bpl.Expr.Imp(activation, allS),

         "1st prefix predicate axiom for " + pp.FullSanitizedName));

 

       // forall args :: { P(args) } args-have-appropriate-values && (forall k :: 0 ATMOST k ==> P#[k](args)) ==> P(args)

@@ -2406,7 +2406,7 @@ namespace Microsoft.Dafny {
     ///           ==> $IsAlloc(h[o, f], TT(PP), h))

     ///       && $Is(h[o, f], TT(PP), h);

     /// <summary>

-    /// This can be optimised later to: 

+    /// This can be optimised later to:

     ///     axiom (forall o: ref, h: Heap ::

     ///         { h[o, f] }

     ///         $IsHeap(h) && o != null && Tag(dtype(o)) = TagClass

@@ -2446,7 +2446,7 @@ namespace Microsoft.Dafny {
       List<Bpl.Expr> tyexprs;

       var tyvars = MkTyParamBinders(GetTypeParams(c), out tyexprs);

 

-      Bpl.Expr o_ty = ClassTyCon(c, tyexprs); 

+      Bpl.Expr o_ty = ClassTyCon(c, tyexprs);

 

       // Bpl.Expr is_o      = MkIs(o, o_ty);         // $Is(o, ..)

       // Changed to use dtype(o) == o_ty instead:

@@ -2458,7 +2458,7 @@ namespace Microsoft.Dafny {
       Bpl.Expr is_hf, isalloc_hf;

 

       if (is_array) {

-        is_hf = MkIs(oDotF, tyexprs[0], true);              

+        is_hf = MkIs(oDotF, tyexprs[0], true);

         isalloc_hf = MkIsAlloc(oDotF, tyexprs[0], h, true);

       } else {

         is_hf = MkIs(oDotF, f.Type);              // $Is(h[o, f], ..)

@@ -2497,7 +2497,7 @@ namespace Microsoft.Dafny {
         tr = new Bpl.Trigger(c.tok, true, t_es);

       }

       Bpl.Expr ax = BplForall(Concat(Concat(tyvars, ixvars), new List<Variable> { hVar, oVar }), tr, body);

-      sink.AddTopLevelDeclaration(new Bpl.Axiom(c.tok, ax, 

+      sink.AddTopLevelDeclaration(new Bpl.Axiom(c.tok, ax,

         c + "." + f + ": Allocation axiom"));

     }

 

@@ -2593,7 +2593,7 @@ namespace Microsoft.Dafny {
         return expr;

       }

     }

-    

+

     void AddMethodImpl(Method m, Bpl.Procedure proc, bool wellformednessProc)

     {

       Contract.Requires(m != null);

@@ -2616,7 +2616,7 @@ namespace Microsoft.Dafny {
       List<Variable> localVariables = new List<Variable>();

       GenerateImplPrelude(m, wellformednessProc, inParams, outParams, builder, localVariables);

 

-      Bpl.StmtList stmts;      

+      Bpl.StmtList stmts;

       if (!wellformednessProc) {

         if (3 <= DafnyOptions.O.Induction && m.IsGhost && m.Mod.Expressions.Count == 0 && m.Outs.Count == 0 && !(m is CoLemma)) {

           var posts = new List<Expression>();

@@ -2661,8 +2661,8 @@ namespace Microsoft.Dafny {
               } else {

                 substMap.Add(iv, ie);

               }

-            }            

-             

+            }

+

 

             // Generate a CallStmt for the recursive call

             Expression recursiveCallReceiver;

@@ -3551,7 +3551,7 @@ namespace Microsoft.Dafny {
                           ExpressionTranslator /*!*/ etran,

                           Bpl.StmtListBuilder /*!*/ builder,

                           string errorMessage,

-                          Bpl.QKeyValue kv) 

+                          Bpl.QKeyValue kv)

     {

       CheckFrameSubset(tok, calleeFrame, receiverReplacement, substMap, etran,

         (t, e, s, q) => builder.Add(Assert(t, e, s, q)), errorMessage, kv);

@@ -3559,7 +3559,7 @@ namespace Microsoft.Dafny {
 

     void CheckFrameSubset(IToken tok, List<FrameExpression> calleeFrame,

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

-                          ExpressionTranslator/*!*/ etran, 

+                          ExpressionTranslator/*!*/ etran,

                           Action<IToken, Bpl.Expr, string, Bpl.QKeyValue> MakeAssert,

                           string errorMessage,

                           Bpl.QKeyValue kv)

@@ -3692,10 +3692,10 @@ namespace Microsoft.Dafny {
         sink.AddTopLevelDeclaration(new Bpl.Axiom(f.tok, ax));

       } else {

 #else

-        // This is the general case                

+        // This is the general case

         Bpl.Expr h0; var h0Var = BplBoundVar("$h0", predef.HeapType, out h0);

-        Bpl.Expr h1; var h1Var = BplBoundVar("$h1", predef.HeapType, out h1);          

-      

+        Bpl.Expr h1; var h1Var = BplBoundVar("$h1", predef.HeapType, out h1);

+

         var etran0 = new ExpressionTranslator(this, predef, h0);

         var etran1 = new ExpressionTranslator(this, predef, h1);

 

@@ -3705,7 +3705,7 @@ namespace Microsoft.Dafny {
 

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

         Bpl.Expr o; var oVar = BplBoundVar("$o", predef.RefType, out o);

-        Bpl.Expr field; var fieldVar = BplBoundVar("$f", predef.FieldName(f.tok, alpha), out field);        

+        Bpl.Expr field; var fieldVar = BplBoundVar("$f", predef.FieldName(f.tok, alpha), out field);

         Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null);

         Bpl.Expr oNotNullAlloced = Bpl.Expr.And(oNotNull, Bpl.Expr.And(etran0.IsAlloced(f.tok, o), etran1.IsAlloced(f.tok, o)));

         Bpl.Expr unchanged = Bpl.Expr.Eq(ReadHeap(f.tok, h0, o, field), ReadHeap(f.tok, h1, o, field));

@@ -3722,7 +3722,7 @@ namespace Microsoft.Dafny {
         var f0argsCanCall = new List<Bpl.Expr>(tyexprs);

         var f1argsCanCall = new List<Bpl.Expr>(tyexprs);

         if (f.IsRecursive) {

-          Bpl.Expr s; var sV = BplBoundVar("$ly", predef.LayerType, out s);          

+          Bpl.Expr s; var sV = BplBoundVar("$ly", predef.LayerType, out s);

           bvars.Add(sV);

           f0args.Add(s); f1args.Add(s);  // but don't add to f0argsCanCall or f1argsCanCall

         }

@@ -3755,14 +3755,14 @@ namespace Microsoft.Dafny {
         }

         var canCall = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName + "#canCall", Bpl.Type.Bool));

         wellFormed = Bpl.Expr.And(wellFormed, Bpl.Expr.And(

-          Bpl.Expr.Or(new Bpl.NAryExpr(f.tok, canCall, f0argsCanCall), fwf0), 

+          Bpl.Expr.Or(new Bpl.NAryExpr(f.tok, canCall, f0argsCanCall), fwf0),

           Bpl.Expr.Or(new Bpl.NAryExpr(f.tok, canCall, f1argsCanCall), fwf1)));

-      

+

         /*

         DR: I conjecture that this should be enough,

             as the requires is preserved when the frame is:

 

-        wellFormed = Bpl.Expr.And(wellFormed, 

+        wellFormed = Bpl.Expr.And(wellFormed,

           Bpl.Expr.Or(new Bpl.NAryExpr(f.tok, canCall, f0argsCanCall), fwf0));

         */

 

@@ -3987,8 +3987,8 @@ namespace Microsoft.Dafny {
         Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, funcID, args);

 

         DefineFrame(f.tok, f.Reads, bodyCheckBuilder

-                   , new List<Variable>() /* dummy local variable list, since frame axiom variable (and its definition) 

-                                           * is already added. The only reason why we add the frame axiom definition 

+                   , new List<Variable>() /* dummy local variable list, since frame axiom variable (and its definition)

+                                           * is already added. The only reason why we add the frame axiom definition

                                            * again is to make boogie gives the same trace as before the change that

                                            * makes reads clauses also guard the requires */

                    , null);

@@ -4000,11 +4000,11 @@ namespace Microsoft.Dafny {
       builder.Add(new Bpl.IfCmd(f.tok, null, postCheckBuilder.Collect(f.tok), null, bodyCheckBuilder.Collect(f.tok)));

 

       // var b$reads_guards_requires#0 : bool

-      locals.AddRange(wfo.Locals);                                  

+      locals.AddRange(wfo.Locals);

       // This ugly way seems to be the way to add things at the start of a builder:

       StmtList sl = builder.Collect(f.tok);

       // b$reads_guards_requires#0 := true   ...

-      sl.BigBlocks[0].simpleCmds.InsertRange(0, wfo.AssignLocals); 

+      sl.BigBlocks[0].simpleCmds.InsertRange(0, wfo.AssignLocals);

 

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

         typeParams, Concat(typeInParams, implInParams), new List<Variable>(),

@@ -4205,7 +4205,7 @@ namespace Microsoft.Dafny {
       } else if (expr is ApplyExpr) {

         ApplyExpr e = (ApplyExpr)expr;

         return BplAnd(

-          Cons(CanCallAssumption(e.Function, etran), 

+          Cons(CanCallAssumption(e.Function, etran),

           e.Args.ConvertAll(ee => CanCallAssumption(ee, etran))));

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

@@ -4701,8 +4701,8 @@ namespace Microsoft.Dafny {
 

         var args = Concat(

           Map(tt.TypeArgs, TypeToTy),

-          Cons(etran.TrExpr(e.Function), 

-          Cons(etran.HeapExpr, 

+          Cons(etran.TrExpr(e.Function),

+          Cons(etran.HeapExpr,

           e.Args.ConvertAll(arg => TrArg(arg)))));

 

         // check precond

@@ -4715,7 +4715,7 @@ namespace Microsoft.Dafny {
             FunctionCall(e.tok, Reads(arity), TrType(objset), args),

             objset);

           var reads = new FrameExpression(e.tok, wrap, null);

-          CheckFrameSubset(expr.tok, new List<FrameExpression>{ reads }, null, null, 

+          CheckFrameSubset(expr.tok, new List<FrameExpression>{ reads }, null, null,

             etran, options.AssertSink(this, builder), "insufficient reads clause to invoke function", options.AssertKv);

         }

 

@@ -4863,7 +4863,7 @@ namespace Microsoft.Dafny {
           // Cannot use the datatype's formals, so we substitute the inferred type args:

           var su = new Dictionary<TypeParameter, Type>();

           foreach (var p in dtv.Ctor.EnclosingDatatype.TypeArgs.Zip(dtv.InferredTypeArgs)) {

-            su[p.Item1] = p.Item2;            

+            su[p.Item1] = p.Item2;

           }

           Type ty = Resolver.SubstType(formal.Type, su);

           CheckSubrange(arg.tok, etran.TrExpr(arg), ty, builder);

@@ -5049,7 +5049,7 @@ namespace Microsoft.Dafny {
 

             // new options now contains the delayed reads checks

             locals.AddRange(newOptions.Locals);

-            // assign locals to true, but at a scope above 

+            // assign locals to true, but at a scope above

             Contract.Assert(newBuilder != builder);

             foreach (var a in newOptions.AssignLocals) {

               builder.Add(a);

@@ -5306,7 +5306,7 @@ namespace Microsoft.Dafny {
         var args = new List<Bpl.Expr>();

         var vars = MkTyParamBinders(GetTypeParams(f), out args);

         var formals = MkTyParamFormals(GetTypeParams(f), false);

-        var tyargs = new List<Bpl.Expr>(); 

+        var tyargs = new List<Bpl.Expr>();

         foreach (var fm in f.Formals) {

           tyargs.Add(TypeToTy(fm.Type));

         }

@@ -5356,7 +5356,7 @@ namespace Microsoft.Dafny {
         int arity = f.Formals.Count;

 

         {

-          // Apply(Ty.., F#Handle( Ty1, ..., TyN, Layer, self), Heap, arg1, ..., argN) 

+          // Apply(Ty.., F#Handle( Ty1, ..., TyN, Layer, self), Heap, arg1, ..., argN)

           //   = [Box] F(Ty1, .., TyN, Layer, Heap, self, [Unbox] arg1, .., [Unbox] argN)

 

           var fhandle = FunctionCall(f.tok, name, predef.HandleType, SnocSelf(args));

@@ -5369,7 +5369,7 @@ namespace Microsoft.Dafny {
         }

 

         {

-          // Requires(Ty.., F#Handle( Ty1, ..., TyN, Layer, self), Heap, arg1, ..., argN) 

+          // Requires(Ty.., F#Handle( Ty1, ..., TyN, Layer, self), Heap, arg1, ..., argN)

           //   = F#Requires(Ty1, .., TyN, Layer, Heap, self, [Unbox] arg1, .., [Unbox] argN)

           //   || Scramble(...)

 

@@ -5389,7 +5389,7 @@ namespace Microsoft.Dafny {
         }

 

         {

-          // Reads(Ty.., F#Handle( Ty1, ..., TyN, Layer, self), Heap, arg1, ..., argN)[Box(o)] 

+          // Reads(Ty.., F#Handle( Ty1, ..., TyN, Layer, self), Heap, arg1, ..., argN)[Box(o)]

           //   =  $Frame_F(args...)[o]

           // //  && Scramble(...)

 

@@ -5439,7 +5439,7 @@ namespace Microsoft.Dafny {
         // function HandleN([Heap, Box, ..., Box] Box, [Heap, Box, ..., Box] Bool) : HandleType

         var res = BplFormalVar(null, predef.HandleType, true);

         var arg = new List<Bpl.Variable> {

-          BplFormalVar(null, apply_ty, true), 

+          BplFormalVar(null, apply_ty, true),

           BplFormalVar(null, requires_ty, true),

           BplFormalVar(null, reads_ty, true)

         };

@@ -5463,11 +5463,11 @@ namespace Microsoft.Dafny {
       SelectorFunction(Reads(arity), objset_ty);

 

       {

-        // forall t1, .., tN+1 : Ty, p: [Heap, Box, ..., Box] Box, heap : Heap, b1, ..., bN : Box 

+        // forall t1, .., tN+1 : Ty, p: [Heap, Box, ..., Box] Box, heap : Heap, b1, ..., bN : Box

         //      :: RequriesN(...) ==> ApplyN(t1, .. tN+1, HandleN(h, r, rd), heap, b1, ..., bN) = h[heap, b1, ..., bN]

         //

         // no precondition for these, but:

-        // for requires, we add: RequiresN(...) <== r[heap, b1, ..., bN] 

+        // for requires, we add: RequiresN(...) <== r[heap, b1, ..., bN]

         // for reads, we could:  ReadsN(...)[bx] ==> rd[heap, b1, ..., bN][bx] , but we don't

         Action<string, Bpl.Type, string, Bpl.Type, string, Bpl.Type> SelectorSemantics = (selector, selectorTy, selectorVar, selectorVarTy, precond, precondTy) => {

           Contract.Assert((precond == null) == (precondTy == null));

@@ -5511,11 +5511,11 @@ namespace Microsoft.Dafny {
         SelectorSemantics(Requires(arity), Bpl.Type.Bool, "r", requires_ty, null, null);

         SelectorSemantics(Reads(arity), objset_ty, "rd", reads_ty, null, null);

 

-        // function {:inline true} 

-        //   FuncN._requires(G...G G: Ty, H:Heap, f:Handle, x ... x :Box): bool 

+        // function {:inline true}

+        //   FuncN._requires(G...G G: Ty, H:Heap, f:Handle, x ... x :Box): bool

         //   { RequiresN(f, H, x...x) }

-        // function {:inline true} 

-        //   FuncN._requires#canCall(G...G G: Ty, H:Heap, f:Handle, x ... x :Box): bool 

+        // function {:inline true}

+        //   FuncN._requires#canCall(G...G G: Ty, H:Heap, f:Handle, x ... x :Box): bool

         //   { true }

         // + similar for Reads

         Action<string, Function> UserSelectorFunction = (fname, f) => {

@@ -5552,15 +5552,15 @@ namespace Microsoft.Dafny {
             HeapSucc(h0, h1) && GoodHeap(h0) && GoodHeap(h1)

             && Is&IsAllocBox(bxI, tI, h0)              // in h0, not hN

             && Is&IsAlloc(f, Func(t1,..,tN, tN+1), h0) // in h0, not hN

-            && 

+            &&

             (forall o : ref::

-                 o != null && h0[o, alloc] && h1[o, alloc] && 

+                 o != null && h0[o, alloc] && h1[o, alloc] &&

                  Reads(h,hN,bxs)[Box(o)]             // for hN in h0 and h1

               ==> h0[o,field] == h1[o,field])

-          ==>  Reads(..h0..) == Reads(..h1..) 

+          ==>  Reads(..h0..) == Reads(..h1..)

            AND Requires(f,h0,bxs) == Requires(f,h1,bxs) // which is needed for the next

            AND  Apply(f,h0,bxs) == Apply(f,h0,bxs)

-        

+

          */

         {

           var bvars = new List<Bpl.Variable>();

@@ -5579,9 +5579,9 @@ namespace Microsoft.Dafny {
 

           var isness = BplAnd(

             Snoc(Map(Enumerable.Range(0, arity), i =>

-              BplAnd(MkIs(boxes[i], types[i], true), 

+              BplAnd(MkIs(boxes[i], types[i], true),

                      MkIsAlloc(boxes[i], types[i], h0, true))),

-            BplAnd(MkIs(f, ClassTyCon(ad, types)), 

+            BplAnd(MkIs(f, ClassTyCon(ad, types)),

                    MkIsAlloc(f, ClassTyCon(ad, types), h0))));

 

           Action<Bpl.Expr, string> AddFrameForFunction = (hN, fname) => {

@@ -5614,7 +5614,7 @@ namespace Microsoft.Dafny {
                   Bpl.Expr.Eq(fn(h0), fn(h1))))));

           };

 

-          AddFrameForFunction(h0, Reads(ad.Arity)); 

+          AddFrameForFunction(h0, Reads(ad.Arity));

           AddFrameForFunction(h1, Reads(ad.Arity));

           AddFrameForFunction(h0, Requires(ad.Arity));

           AddFrameForFunction(h1, Requires(ad.Arity));

@@ -5627,10 +5627,10 @@ namespace Microsoft.Dafny {
 

           forall t0..tN+1 : Ty, h : Heap, f : Handle, bx1 .. bxN : Box,

             GoodHeap(h)

-            && Is&IsAllocBox(bxI, tI, h)              

-            && Is&IsAlloc(f, Func(t1,..,tN, tN+1), h) 

+            && Is&IsAllocBox(bxI, tI, h)

+            && Is&IsAlloc(f, Func(t1,..,tN, tN+1), h)

           ==> Is&IsAllocBox(Apply(f,h0,bxs)))

-        

+

          */

         {

           var bvars = new List<Bpl.Variable>();

@@ -5645,9 +5645,9 @@ namespace Microsoft.Dafny {
 

           var isness = BplAnd(

             Snoc(Map(Enumerable.Range(0, arity), i =>

-              BplAnd(MkIs(boxes[i], types[i], true), 

+              BplAnd(MkIs(boxes[i], types[i], true),

                      MkIsAlloc(boxes[i], types[i], h, true))),

-            BplAnd(MkIs(f, ClassTyCon(ad, types)), 

+            BplAnd(MkIs(f, ClassTyCon(ad, types)),

                    MkIsAlloc(f, ClassTyCon(ad, types), h))));

 

           var applied = FunctionCall(tok, Apply(ad.Arity), predef.BoxType, Concat(types, Cons(f, Cons<Bpl.Expr>(h, boxes))));

@@ -5690,7 +5690,7 @@ namespace Microsoft.Dafny {
       };

 

       // Create the Tag and calling Tag on this type constructor

-      /* 

+      /*

          const unique TagList: TyTag;

          axiom (forall t0: Ty :: { List(t0) } Tag(List(t0)) == TagList);

       */

@@ -5705,7 +5705,7 @@ namespace Microsoft.Dafny {
       });

 

       // Create the injectivity axiom and its function

-      /* 

+      /*

          function List_0(Ty) : Ty;

          axiom (forall t0: Ty :: { List(t0) } List_0(List(t0)) == t0);

       */

@@ -5724,8 +5724,8 @@ namespace Microsoft.Dafny {
 

       // Boxing axiom (important for the properties of unbox)

       /*

-         axiom (forall T: Ty, bx: Box :: 

-           { $IsBox(bx, List(T)) } 

+         axiom (forall T: Ty, bx: Box ::

+           { $IsBox(bx, List(T)) }

            $IsBox(bx, List(T))

               ==> $Box($Unbox(bx): DatatypeType) == bx

                && $Is($Unbox(bx): DatatypeType, List(T)));

@@ -5745,7 +5745,7 @@ namespace Microsoft.Dafny {
       });

 

       return name;

-    }      

+    }

 

     Bpl.Constant GetClass(TopLevelDecl cl)

     {

@@ -5806,17 +5806,17 @@ namespace Microsoft.Dafny {
       return fc;

     }

 

-    

+

     Bpl.Function GetReadonlyField(Field f)

     {

       Contract.Requires(f != null && !f.IsMutable);

       Contract.Requires(sink != null && predef != null);

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

-      

+

       Bpl.Function ff;

-      if (fieldFunctions.TryGetValue(f, out ff)) {        

+      if (fieldFunctions.TryGetValue(f, out ff)) {

         Contract.Assert(ff != null);

-      } else {        

+      } else {

         if (f.EnclosingClass is ArrayClassDecl && f.Name == "Length") { // link directly to the function in the prelude.

           fieldFunctions.Add(f, predef.ArrayLength);

           return predef.ArrayLength;

@@ -5945,7 +5945,7 @@ namespace Microsoft.Dafny {
     /// <summary>

     /// This method is expected to be called at most once for each parameter combination, and in particular

     /// at most once for each value of "kind".

-    /// </summary>    

+    /// </summary>

     Bpl.Procedure AddMethod(Method m, MethodTranslationKind kind)

     {

       Contract.Requires(m != null);

@@ -5963,7 +5963,7 @@ namespace Microsoft.Dafny {
       List<Variable> inParams, outParams;

       GenerateMethodParameters(m.tok, m, kind, etran, out inParams, out outParams);

 

-      var req = new List<Bpl.Requires>();    

+      var req = new List<Bpl.Requires>();

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

       var ens = new List<Bpl.Ensures>();

       // FREE PRECONDITIONS

@@ -6348,7 +6348,7 @@ namespace Microsoft.Dafny {
     private void GenerateMethodParametersChoose(IToken tok, IMethodCodeContext m, MethodTranslationKind kind, bool includeReceiver, bool includeInParams, bool includeOutParams,

       ExpressionTranslator etran, out List<Variable> inParams, out List<Variable> outParams) {

       inParams = new List<Bpl.Variable>();

-      outParams = new List<Variable>();      

+      outParams = new List<Variable>();

       // Add type parameters first, always!

       inParams.AddRange(MkTyParamFormals(GetTypeParams(m)));

       if (includeReceiver) {

@@ -6358,8 +6358,8 @@ namespace Microsoft.Dafny {
           etran.GoodRef(tok, new Bpl.IdentifierExpr(tok, "this", predef.RefType), receiverType));

         Bpl.Formal thVar = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "this", predef.RefType, wh), true);

         inParams.Add(thVar);

-      }      

-      if (includeInParams) {        

+      }

+      if (includeInParams) {

         foreach (Formal p in m.Ins) {

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

           Bpl.Expr wh = GetExtendedWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.AssignUniqueName(currentDeclaration), varType), p.Type, etran);

@@ -7023,9 +7023,11 @@ namespace Microsoft.Dafny {
       } else if (stmt is WhileStmt) {

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

         var s = (WhileStmt)stmt;

-        TrLoop(s, s.Guard,

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

-          builder, locals, etran);

+        BodyTranslator bodyTr = null;

+        if (s.Body != null) {

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

+        }

+        TrLoop(s, s.Guard, bodyTr, builder, locals, etran);

 

       } else if (stmt is AlternativeLoopStmt) {

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

@@ -8138,7 +8140,6 @@ namespace Microsoft.Dafny {
     void TrLoop(LoopStmt s, Expression Guard, BodyTranslator bodyTr,

                 Bpl.StmtListBuilder builder, List<Variable> locals, ExpressionTranslator etran) {

       Contract.Requires(s != null);

-      Contract.Requires(bodyTr != null);

       Contract.Requires(builder != null);

       Contract.Requires(locals != null);

       Contract.Requires(etran != null);

@@ -8253,31 +8254,36 @@ namespace Microsoft.Dafny {
       guardBreak.Add(new Bpl.BreakCmd(s.Tok, null));

       loopBodyBuilder.Add(new Bpl.IfCmd(s.Tok, guard, guardBreak.Collect(s.Tok), null, null));

 

-      // termination checking

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

-        // omit termination checking for this loop

-        bodyTr(loopBodyBuilder, updatedFrameEtran);

-      } else {

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

-        // time for the actual loop body

-        bodyTr(loopBodyBuilder, updatedFrameEtran);

-        // check definedness of decreases expressions

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

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

-        var decrs = new List<Expr>();

-        foreach (Expression e in theDecreases) {

-          toks.Add(e.tok);

-          types.Add(e.Type.NormalizeExpand());

-          decrs.Add(etran.TrExpr(e));

-        }

-        Bpl.Expr decrCheck = DecreasesCheck(toks, types, types, decrs, oldBfs, loopBodyBuilder, " at end of loop iteration", false, false);

-        string msg;

-        if (s.InferredDecreases) {

-          msg = "cannot prove termination; try supplying a decreases clause for the loop";

+      if (bodyTr != null) {

+        // termination checking

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

+          // omit termination checking for this loop

+          bodyTr(loopBodyBuilder, updatedFrameEtran);

         } else {

-          msg = "decreases expression might not decrease";

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

+          // time for the actual loop body

+          bodyTr(loopBodyBuilder, updatedFrameEtran);

+          // check definedness of decreases expressions

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

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

+          var decrs = new List<Expr>();

+          foreach (Expression e in theDecreases) {

+            toks.Add(e.tok);

+            types.Add(e.Type.NormalizeExpand());

+            decrs.Add(etran.TrExpr(e));

+          }

+          Bpl.Expr decrCheck = DecreasesCheck(toks, types, types, decrs, oldBfs, loopBodyBuilder, " at end of loop iteration", false, false);

+          string msg;

+          if (s.InferredDecreases) {

+            msg = "cannot prove termination; try supplying a decreases clause for the loop";

+          } else {

+            msg = "decreases expression might not decrease";

+          }

+          loopBodyBuilder.Add(Assert(s.Tok, decrCheck, msg));

         }

-        loopBodyBuilder.Add(Assert(s.Tok, decrCheck, msg));

+      } else {

+        loopBodyBuilder.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));

+        // todo(maria): havoc stuff

       }

       // Finally, assume the well-formedness of the invariant (which has been checked once and for all above), so that the check

       // of invariant-maintenance can use the appropriate canCall predicates.

@@ -8474,7 +8480,7 @@ namespace Microsoft.Dafny {
       ins.AddRange(trTypeArgs(tySubst, tyArgs));

 

       // Translate receiver argument, if any

-      Expression receiver = bReceiver == null ? dafnyReceiver : new BoogieWrapper(bReceiver, dafnyReceiver.Type);      

+      Expression receiver = bReceiver == null ? dafnyReceiver : new BoogieWrapper(bReceiver, dafnyReceiver.Type);

       if (!method.IsStatic) {

         if (bReceiver == null && !(dafnyReceiver is ThisExpr)) {

           CheckNonNull(dafnyReceiver.tok, dafnyReceiver, builder, etran, null);

@@ -8511,7 +8517,7 @@ namespace Microsoft.Dafny {
           }

           TrStmt_CheckWellformed(actual, builder, locals, etran, true);

           builder.Add(new CommentCmd("ProcessCallStmt: CheckSubrange"));

-          // Check the subrange without boxing 

+          // Check the subrange without boxing

           var beforeBox = etran.TrExpr(actual);

           CheckSubrange(actual.tok, beforeBox, Resolver.SubstType(formal.Type, tySubst), builder);

           bActual = CondApplyBox(actual.tok, beforeBox, actual.Type, formal.Type);

@@ -8937,9 +8943,9 @@ namespace Microsoft.Dafny {
     }

 

     /// <summary>

-    /// Therefore, these properties are applied to method in-parameters. 

+    /// Therefore, these properties are applied to method in-parameters.

     /// For now, this only allows you to case split on incoming data type values.

-    /// This used to add IsGood[Multi]Set_Extendend, but that is always 

+    /// This used to add IsGood[Multi]Set_Extendend, but that is always

     /// added for sets & multisets now in the prelude.

     /// </summary>

     Bpl.Expr GetExtendedWhereClause(IToken tok, Bpl.Expr x, Type type, ExpressionTranslator etran) {

@@ -8975,9 +8981,9 @@ namespace Microsoft.Dafny {
       } else if (type is SeqType) {

         return FunctionCall(Token.NoToken, "TSeq", predef.Ty, TypeToTy(((CollectionType)type).Arg));

       } else if (type is MapType) {

-        return FunctionCall(Token.NoToken, "TMap", predef.Ty, 

+        return FunctionCall(Token.NoToken, "TMap", predef.Ty,

           TypeToTy(((MapType)type).Domain),

-          TypeToTy(((MapType)type).Range)); 

+          TypeToTy(((MapType)type).Range));

       } else if (type is BoolType) {

         return new Bpl.IdentifierExpr(Token.NoToken, "TBool", predef.Ty);

       } else if (type is CharType) {

@@ -8997,7 +9003,7 @@ namespace Microsoft.Dafny {
       } else if (type is UserDefinedType) {

         // Classes, (co-)datatypes

         var args = type.TypeArgs.ConvertAll(TypeToTy);

-        return ClassTyCon(((UserDefinedType)type), args);      

+        return ClassTyCon(((UserDefinedType)type), args);

       } else if (type is ParamTypeProxy) {

         return trTypeParam(((ParamTypeProxy)type).orig, null);

       } else {

@@ -9014,7 +9020,7 @@ namespace Microsoft.Dafny {
         return "#$" + x.Name;

       }

     }

-   

+

     Bpl.Expr trTypeParam(TypeParameter x, List<Bpl.Expr> tyArguments) {

       Contract.Requires(x != null);

       var nm = nameTypeParam(x);

@@ -9043,8 +9049,8 @@ namespace Microsoft.Dafny {
       if (d is ClassDecl) {

         return Concat(GetTypeParams(d.Module), d.TypeArgs);

       } else if (d is DatatypeDecl) {

-        return Concat(GetTypeParams(d.Module), d.TypeArgs);      

-      } else if (d is ModuleDefinition) {       

+        return Concat(GetTypeParams(d.Module), d.TypeArgs);

+      } else if (d is ModuleDefinition) {

         return new List<TypeParameter>();

       } else {

         Contract.Assert(false);

@@ -9060,7 +9066,7 @@ namespace Microsoft.Dafny {
       }

     }

 

-    // Boxes, if necessary 

+    // Boxes, if necessary

     Bpl.Expr MkIs(Bpl.Expr x, Type t) {

       return MkIs(x, TypeToTy(t), ModeledAsBoxType(t));

     }

@@ -9496,7 +9502,7 @@ namespace Microsoft.Dafny {
 

         TrStmt_CheckWellformed(e.Expr, builder, locals, etran, true);

 

-        Bpl.Expr bRhs = etran.TrExpr(e.Expr);        

+        Bpl.Expr bRhs = etran.TrExpr(e.Expr);

         CheckSubrange(tok, bRhs, checkSubrangeType, builder);

         bRhs = CondApplyBox(tok, bRhs, e.Expr.Type, lhsType);

 

@@ -9592,7 +9598,7 @@ namespace Microsoft.Dafny {
       if (tp.NormalizeExpand() is NatType) {

         return MkIs(bRhs, tp);

       } else {

-        return Bpl.Expr.True; 

+        return Bpl.Expr.True;

       }

 

     }

@@ -9766,7 +9772,7 @@ namespace Microsoft.Dafny {
       public readonly bool UsesHeap;

       public readonly bool UsesOldHeap;

       public readonly Type ThisType;  // null if 'this' is not used

-      public LetSuchThatExprInfo(IToken tok, int uniqueLetId, 

+      public LetSuchThatExprInfo(IToken tok, int uniqueLetId,

       List<IVariable> freeVariables, List<TypeParameter> freeTypeVars,

       bool usesHeap, bool usesOldHeap, Type thisType, Declaration currentDeclaration) {

         Tok = tok;

@@ -9793,7 +9799,7 @@ namespace Microsoft.Dafny {
         Tok = template.Tok;

         LetId = template.LetId;  // reuse the ID, which ensures we get the same $let functions

         FTVs = template.FTVs;

-        FTV_Types = template.FTV_Types.ConvertAll(t => Resolver.SubstType(t, typeMap)); 

+        FTV_Types = template.FTV_Types.ConvertAll(t => Resolver.SubstType(t, typeMap));

         FVs = template.FVs;

         FV_Exprs = template.FV_Exprs.ConvertAll(e => translator.Substitute(e, null, substMap, typeMap));

         UsesHeap = template.UsesHeap;

@@ -9933,7 +9939,7 @@ namespace Microsoft.Dafny {
       public readonly string FunctionName;

       public readonly bool UsesHeap;

       public readonly bool UsesOldHeap;

-      public readonly List<Type> TyArgs; // Note: also has a bunch of type arguments 

+      public readonly List<Type> TyArgs; // Note: also has a bunch of type arguments

       public readonly List<Expression> Args;

       public BoogieFunctionCall(IToken tok, string functionName, bool usesHeap, bool usesOldHeap, List<Expression> args, List<Type> tyArgs)

         : base(tok)

@@ -9964,7 +9970,7 @@ namespace Microsoft.Dafny {
       public readonly string This;

       public readonly string modifiesFrame; // the name of the context's frame variable.

       readonly Function applyLimited_CurrentFunction;

-      public readonly Bpl.Expr layerInterCluster;     

+      public readonly Bpl.Expr layerInterCluster;

       public readonly Bpl.Expr layerIntraCluster = null;  // a value of null says to do the same as for inter-cluster calls

       public int Statistics_CustomLayerFunctionCount = 0;

       public readonly bool ProducingCoCertificates = false;

@@ -10066,7 +10072,7 @@ namespace Microsoft.Dafny {
         Contract.Requires(thisVar != null);

       }

 

-      public ExpressionTranslator(ExpressionTranslator etran, Bpl.Expr heap) 

+      public ExpressionTranslator(ExpressionTranslator etran, Bpl.Expr heap)

         : this(etran.translator, etran.predef, heap, etran.This, etran.applyLimited_CurrentFunction, etran.layerInterCluster, etran.layerIntraCluster, etran.modifiesFrame)

       {

         Contract.Requires(etran != null);

@@ -10098,7 +10104,7 @@ namespace Microsoft.Dafny {
         }

       }

 

-      public ExpressionTranslator WithLayer(Bpl.Expr layerArgument) 

+      public ExpressionTranslator WithLayer(Bpl.Expr layerArgument)

       {

         Contract.Requires(layerArgument != null);

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

@@ -10490,7 +10496,7 @@ namespace Microsoft.Dafny {
 

           Func<Expression, Bpl.Expr> TrArg = arg => translator.BoxIfUnboxed(TrExpr(arg), arg.Type);

 

-          var applied = translator.FunctionCall(expr.tok, translator.Apply(arity), predef.BoxType, 

+          var applied = translator.FunctionCall(expr.tok, translator.Apply(arity), predef.BoxType,

             Concat(Map(tt.TypeArgs,translator.TypeToTy),

             Cons(TrExpr(e.Function), Cons(HeapExpr, e.Args.ConvertAll(arg => TrArg(arg))))));

 

@@ -10773,7 +10779,7 @@ namespace Microsoft.Dafny {
                   return translator.FunctionCall(expr.tok, "INTERNAL_mul_boogie", Bpl.Type.Int, e0, e1);

                 }

               }

-            

+

             case BinaryExpr.ResolvedOpcode.Div:

               if (isReal) {

                 typ = Bpl.Type.Real;

@@ -10971,7 +10977,7 @@ namespace Microsoft.Dafny {
           if (Attributes.ContainsBool(e.Attributes, "layerQuantifier", ref _scratch)) {

             // If this is a layer quantifier, quantify over layers here, and use $LS(ly) layers in the translation of the body

             var ly = BplBoundVar(e.Refresh("$ly", ref translator.otherTmpVarCount), predef.LayerType, bvars);

-            Expr layer = translator.LayerSucc(ly); 

+            Expr layer = translator.LayerSucc(ly);

             bodyEtran = new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layer, layer, modifiesFrame);

           }

           if (Attributes.ContainsBool(e.Attributes, "heapQuantifier", ref _scratch)) {

@@ -10995,7 +11001,7 @@ namespace Microsoft.Dafny {
                 tt.Add(bodyEtran.TrExpr(arg));

               }

               tr = new Bpl.Trigger(expr.tok, true, tt, tr);

-            } 

+            }

           }

           if (e.Range != null) {

             antecedent = BplAnd(antecedent, bodyEtran.TrExpr(e.Range));

@@ -11131,8 +11137,8 @@ namespace Microsoft.Dafny {
 

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

         Bpl.Expr consequent = translator.InRWClause(e.tok, o, null, e.Reads.ConvertAll(su.SubstFrameExpr), et, null, null);

-        Bpl.Expr rdbody = 

-          new Bpl.LambdaExpr(e.tok, new List<TypeVariable>(), rdvars, null, 

+        Bpl.Expr rdbody =

+          new Bpl.LambdaExpr(e.tok, new List<TypeVariable>(), rdvars, null,

             BplImp(ante, consequent));

 

         return translator.Lit(

@@ -11141,8 +11147,8 @@ namespace Microsoft.Dafny {
               translator.FunctionCall(e.tok, translator.Handle(e.BoundVars.Count), predef.BoxType,

                 new Bpl.LambdaExpr(e.tok, new List<TypeVariable>(), bvars, null, ebody),

                 new Bpl.LambdaExpr(e.tok, new List<TypeVariable>(), bvars, null, reqbody),

-                new Bpl.LambdaExpr(e.tok, new List<TypeVariable>(), bvars, null, rdbody))), 

-            layerIntraCluster ?? layerInterCluster), 

+                new Bpl.LambdaExpr(e.tok, new List<TypeVariable>(), bvars, null, rdbody))),

+            layerIntraCluster ?? layerInterCluster),

           predef.HandleType);

       }

 

@@ -11253,12 +11259,12 @@ namespace Microsoft.Dafny {
 

         List<Bpl.Expr> args = new List<Bpl.Expr>();

 

-        // first add type arguments        

+        // first add type arguments

         var tyParams = GetTypeParams(e.Function);

         var tySubst = e.TypeArgumentSubstitutions;

         Contract.Assert(tyParams.Count == tySubst.Count);

         args.AddRange(translator.trTypeArgs(tySubst, tyParams));

-        

+

         if (layerArgument != null) {

           args.Add(layerArgument);

         }

@@ -11438,7 +11444,7 @@ namespace Microsoft.Dafny {
       // --------------- help routines ---------------

 

       public Bpl.Expr IsAlloced(IToken tok, Bpl.Expr e) {

-        return translator.IsAlloced(tok, HeapExpr, e);        

+        return translator.IsAlloced(tok, HeapExpr, e);

       }

 

       public Bpl.Expr GoodRef(IToken tok, Bpl.Expr e, Type type) {

@@ -11456,7 +11462,7 @@ namespace Microsoft.Dafny {
         Contract.Requires(e != null);

         Contract.Requires(ty != null);

 

-        Bpl.Expr tr_ty = translator.TypeToTy(ty); 

+        Bpl.Expr tr_ty = translator.TypeToTy(ty);

 

         Bpl.Expr alloc = IsAlloced(tok, e);

         if (isNew) {

@@ -11475,7 +11481,7 @@ namespace Microsoft.Dafny {
       LayerSucc,

       CharFromInt,

       CharToInt,

-      

+

       Is, IsBox,

       IsAlloc, IsAllocBox,

 

@@ -12042,12 +12048,12 @@ namespace Microsoft.Dafny {
     }

 

     Bpl.Trigger TrTrigger(ExpressionTranslator etran, Attributes attribs, IToken tok, Dictionary<IVariable, Expression> substMap = null)

-    {      

+    {

       Bpl.Trigger tr = null;

       for (Attributes aa = attribs; aa != null; aa = aa.Prev) {

         if (aa.Name == "trigger") {

           List<Bpl.Expr> tt = new List<Bpl.Expr>();

-          foreach (var arg in aa.Args) {            

+          foreach (var arg in aa.Args) {

             if (substMap == null) {

               tt.Add(etran.TrExpr(arg));

             } else {

@@ -12163,8 +12169,8 @@ namespace Microsoft.Dafny {
           var A2 = etran2.TrExpr(e.E1);

           var B2 = etran2.TrExpr(e.E2);

           var needsTokenAdjust = TrSplitNeedsTokenAdjustment(expr);

-          // Dan: dafny4/Circ.dfy needs this one to be 2+, rather than 1+ 

-          Bpl.Expr layer = LayerSucc(etran.layerInterCluster, 2); 

+          // Dan: dafny4/Circ.dfy needs this one to be 2+, rather than 1+

+          Bpl.Expr layer = LayerSucc(etran.layerInterCluster, 2);

           foreach (var c in CoPrefixEquality(needsTokenAdjust ? new ForceCheckToken(expr.tok) : expr.tok, codecl, e1type.TypeArgs, e2type.TypeArgs, kMinusOne, layer, A2, B2, true)) {

             var p = Bpl.Expr.Binary(c.tok, BinaryOperator.Opcode.Or, prefixEqK, Bpl.Expr.Imp(kPos, c));

             splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, p));

@@ -12284,7 +12290,7 @@ namespace Microsoft.Dafny {
             }

 

             // body

-            var trBody = etran.TrExpr(typeSpecializedBody); 

+            var trBody = etran.TrExpr(typeSpecializedBody);

             trBody = CondApplyUnbox(trBody.tok, trBody, typeSpecializedResultType, expr.Type);

             // F#canCall(args) && F(args) && (b0 && b1 && b2)

             var fr = Bpl.Expr.And(canCall, BplAnd(fargs, trBody));

@@ -12294,8 +12300,8 @@ namespace Microsoft.Dafny {
           }

         }

 

-      } else if (((position && expr is ForallExpr) || (!position && expr is ExistsExpr)) 

-          /* NB: only for type arg less quantifiers for now: */ 

+      } else if (((position && expr is ForallExpr) || (!position && expr is ExistsExpr))

+          /* NB: only for type arg less quantifiers for now: */

              && ((QuantifierExpr)expr).TypeArgs.Count == 0) {

         var e = (QuantifierExpr)expr;

         var inductionVariables = ApplyInduction(e);

@@ -12377,7 +12383,7 @@ namespace Microsoft.Dafny {
             Bpl.Expr q;

             if (position) {

               if (Attributes.Contains(e.Attributes, "trigger")) {

-                Bpl.Trigger tr = TrTrigger(etran, e.Attributes, expr.tok);               

+                Bpl.Trigger tr = TrTrigger(etran, e.Attributes, expr.tok);

                 q = new Bpl.ForallExpr(kase.tok, bvars, tr, Bpl.Expr.Imp(ante, bdy));

               } else {

                 q = new Bpl.ForallExpr(kase.tok, bvars, Bpl.Expr.Imp(ante, bdy));

@@ -12820,7 +12826,7 @@ namespace Microsoft.Dafny {
     }

 

     static void ComputeFreeTypeVariables(Type ty, ISet<TypeParameter> fvs) {

-      // Add type parameters, unless they are abstract type declarations: they are in scope 

+      // Add type parameters, unless they are abstract type declarations: they are in scope

       if (ty.IsTypeParameter && ! ty.AsTypeParameter.IsAbstractTypeDeclaration) {

         fvs.Add(ty.AsTypeParameter);

       }

@@ -13087,7 +13093,7 @@ namespace Microsoft.Dafny {
             DatatypeValue newDtv = new DatatypeValue(dtv.tok, dtv.DatatypeName, dtv.MemberName, newArgs);

             newDtv.Ctor = dtv.Ctor;  // resolve on the fly (and set newDtv.Type below, at end)

             newDtv.InferredTypeArgs = Map(dtv.InferredTypeArgs, tt => Resolver.SubstType(tt, typeMap));

-                                     // ^ Set the correct type arguments to the constructor 

+                                     // ^ Set the correct type arguments to the constructor

             newExpr = newDtv;

           }

 

@@ -13473,7 +13479,7 @@ namespace Microsoft.Dafny {
           var s = (CallStmt)stmt;

           var rr = new CallStmt(s.Tok, s.EndTok, s.Lhs.ConvertAll(Substitute), Substitute(s.Receiver), s.MethodName, s.Args.ConvertAll(Substitute));

           rr.Method = s.Method;

-          rr.TypeArgumentSubstitutions = new Dictionary<TypeParameter, Type>(); 

+          rr.TypeArgumentSubstitutions = new Dictionary<TypeParameter, Type>();

           foreach (var p in s.TypeArgumentSubstitutions) {

             rr.TypeArgumentSubstitutions[p.Key] = Resolver.SubstType(p.Value, typeMap);

           }

@@ -13778,7 +13784,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(b != null);

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

 

-      if (a == Bpl.Expr.True) { 

+      if (a == Bpl.Expr.True) {

         return b;

       } else if (b == Bpl.Expr.True) {

         return a;

@@ -13812,7 +13818,7 @@ namespace Microsoft.Dafny {
     }

 

     /// <summary>

-    /// lhs should be a Bpl.IdentifierExpr. 

+    /// lhs should be a Bpl.IdentifierExpr.

     /// Creates lhs := rhs;

     /// </summary>

     static Bpl.Cmd BplSimplestAssign(Bpl.Expr lhs, Bpl.Expr rhs) {

@@ -13845,13 +13851,13 @@ namespace Microsoft.Dafny {
     }

 

     /* This function allows you to replace, for example:

-       

+

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

            Bpl.IdentifierExpr i = new Bpl.IdentifierExpr(e.tok, iVar);

-      

+

        with:

 

-           Bpl.Expr i; var iVar = BplBoundVar("$i", Bpl.Type.Int, out i); 

+           Bpl.Expr i; var iVar = BplBoundVar("$i", Bpl.Type.Int, out i);

     */

     static Bpl.BoundVariable BplBoundVar(string name, Bpl.Type ty, out Bpl.Expr e) {

       Contract.Requires(ty != null);

@@ -13925,7 +13931,7 @@ namespace Microsoft.Dafny {
     // Utilities for lists and dicts...

 

     static List<A> Singleton<A>(A x) {

-      return Util.Singleton(x); 

+      return Util.Singleton(x);

     }

 

     static List<A> Cons<A>(A x, List<A> xs) {

@@ -13933,7 +13939,7 @@ namespace Microsoft.Dafny {
     }

 

     static List<A> Snoc<A>(List<A> xs, A x) {

-      return Util.Snoc(xs, x); 

+      return Util.Snoc(xs, x);

     }

 

     static List<A> Concat<A>(List<A> xs, List<A> ys) {

@@ -13941,9 +13947,9 @@ namespace Microsoft.Dafny {
     }

 

     static List<B> Map<A,B>(IEnumerable<A> xs, Func<A,B> f) {

-      return Util.Map(xs, f); 

+      return Util.Map(xs, f);

     }

-    

+

     public static void MapM<A>(IEnumerable<A> xs, Action<A> K)

     {

       Contract.Requires(xs != null);

diff --git a/Test/dafny0/DirtyLoops.dfy b/Test/dafny0/DirtyLoops.dfy
index 6a49e733..5d356f0a 100644
--- a/Test/dafny0/DirtyLoops.dfy
+++ b/Test/dafny0/DirtyLoops.dfy
@@ -1,6 +1,21 @@
 // RUN: %dafny /compile:0 /dprint:"%t.dprint.dfy" "%s" > "%t"; %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t"

 // RUN: %diff "%s.expect" "%t"

 

-method M(S: set<int>) {

+method M0(S: set<int>) {

   forall s | s in S ensures s < 0;

 }

+

+method M1(x: int)

+{

+  var i := x;

+  while (0 < i)

+    invariant i <= x;

+}

+

+method M2(x: int)

+{

+  var i := x;

+  while (0 < i)

+    invariant i <= x;

+    decreases i;

+}

diff --git a/Test/dafny0/DirtyLoops.dfy.expect b/Test/dafny0/DirtyLoops.dfy.expect
index 5c12e1ef..060f3287 100644
--- a/Test/dafny0/DirtyLoops.dfy.expect
+++ b/Test/dafny0/DirtyLoops.dfy.expect
@@ -1,4 +1,4 @@
 

-Dafny program verifier finished with 2 verified, 0 errors

+Dafny program verifier finished with 6 verified, 0 errors

 

 Dafny program verifier finished with 0 verified, 0 errors