Dafny: added let expressions (syntax: "var x := E0; E1")

Dafny: firmed up semantics of assert/assume expressions (the condition is now good for all program control paths that pass through the expression)
Dafny: various implementation clean-ups

12 files changed, 524 insertions, 194 deletions

diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index de863e39..d0e0cb0e 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -1667,6 +1667,17 @@ namespace Microsoft.Dafny {
           wr.Write(")");

         }

 

+      } else if (expr is LetExpr) {

+        var e = (LetExpr)expr;

+        // Since there are no OldExpr's in an expression to be compiled, we can just do a regular substitution

+        // without having to worry about old-capture.

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

+        Contract.Assert(e.Vars.Count == e.RHSs.Count);  // checked by resolution

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

+          substMap.Add(e.Vars[i], e.RHSs[i]);

+        }

+        TrExpr(Translator.Substitute(e.Body, null, substMap));

+

       } else if (expr is QuantifierExpr) {

         var e = (QuantifierExpr)expr;

         Contract.Assert(e.Bounds != null);  // for non-ghost quantifiers, the resolver would have insisted on finding bounds

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 8a9108f0..2eaaca7f 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -716,7 +716,7 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall>
 VarDeclStatement<.out Statement/*!*/ s.>

 = (. IToken x = null, assignTok = null;  bool isGhost = false;

      VarDecl/*!*/ d;

-     AssignmentRhs r;  Expression lhs0;

+     AssignmentRhs r;  IdentifierExpr lhs0;

      List<VarDecl> lhss = new List<VarDecl>();

      List<AssignmentRhs> rhss = new List<AssignmentRhs>();

   .)

@@ -727,7 +727,10 @@ VarDeclStatement<.out Statement/*!*/ s.>
   { ","

     LocalIdentTypeOptional<out d, isGhost>  (. lhss.Add(d); .)

   }

-  [ ":="                           (. assignTok = t;  lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name); .)

+  [ ":="                           (. assignTok = t;

+                                      lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);

+                                      lhs0.Var = lhss[0];  lhs0.Type = lhss[0].OptionalType;  // resolve here

+                                   .)

     Rhs<out r, lhs0>               (. rhss.Add(r); .)

     { "," Rhs<out r, lhs0>         (. rhss.Add(r); .)

     }

@@ -1204,20 +1207,34 @@ EndlessExpression<out Expression e>
 = (. IToken/*!*/ x;

      Expression e0, e1;

      e = dummyExpr;

+     BoundVar d;

+     List<BoundVar> letVars;  List<Expression> letRHSs;

   .)

-  ( "if"                                 (. x = t; .)

+  ( "if"                            (. x = t; .)

     Expression<out e>

     "then" Expression<out e0>

-    "else" Expression<out e1>            (. e = new ITEExpr(x, e, e0, e1); .)

+    "else" Expression<out e1>       (. e = new ITEExpr(x, e, e0, e1); .)

   | MatchExpression<out e>

   | QuantifierGuts<out e>

   | ComprehensionExpr<out e>

-  | "assert"                             (. x = t; .)

+  | "assert"                        (. x = t; .)

     Expression<out e0> ";"

-    Expression<out e1>                   (. e = new AssertExpr(x, e0, e1); .)

-  | "assume"                             (. x = t; .)

+    Expression<out e1>              (. e = new AssertExpr(x, e0, e1); .)

+  | "assume"                        (. x = t; .)

     Expression<out e0> ";"

-    Expression<out e1>                   (. e = new AssumeExpr(x, e0, e1); .)

+    Expression<out e1>              (. e = new AssumeExpr(x, e0, e1); .)

+  | "var"                           (. x = t;

+                                       letVars = new List<BoundVar>();

+                                       letRHSs = new List<Expression>(); .)

+    IdentTypeOptional<out d>        (. letVars.Add(d); .)

+    { "," IdentTypeOptional<out d>  (. letVars.Add(d); .)

+    }

+    ":="

+    Expression<out e>               (. letRHSs.Add(e); .)

+    { "," Expression<out e>         (. letRHSs.Add(e); .)

+    }

+    ";"

+    Expression<out e>               (. e = new LetExpr(x, letVars, letRHSs, e); .)

   )

   .

 MatchExpression<out Expression/*!*/ e>

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index e07c6f1d..8272736c 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -2593,6 +2593,27 @@ namespace Microsoft.Dafny {
     }

   }

 

+  public class LetExpr : Expression

+  {

+    public readonly List<BoundVar> Vars;

+    public readonly List<Expression> RHSs;

+    public readonly Expression Body;

+    public LetExpr(IToken tok, List<BoundVar> vars, List<Expression> rhss, Expression body)

+      : base(tok) {

+      Vars = vars;

+      RHSs = rhss;

+      Body = body;

+    }

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        foreach (var rhs in RHSs) {

+          yield return rhs;

+        }

+        yield return Body;

+      }

+    }

+  }

+

   /// <summary>

   /// A ComprehensionExpr has the form:

   ///   BINDER x Attributes | Range(x) :: Term(x)

diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index 0dc30e8a..583fcc61 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -23,7 +23,7 @@ public class Parser {
 	const bool T = true;

 	const bool x = false;

 	const int minErrDist = 2;

-

+	

 	public Scanner/*!*/ scanner;

 	public Errors/*!*/  errors;

 

@@ -134,10 +134,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (errDist >= minErrDist) errors.SemErr(t, msg);

 		errDist = 0;

 	}

-

-	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {

-	  Contract.Requires(tok != null);

-	  Contract.Requires(msg != null);

+	

+    public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {

+      Contract.Requires(tok != null);

+      Contract.Requires(msg != null);

 	  errors.SemErr(tok, msg);

 	}

 

@@ -150,15 +150,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			la = t;

 		}

 	}

-

+	

 	void Expect (int n) {

 		if (la.kind==n) Get(); else { SynErr(n); }

 	}

-

+	

 	bool StartOf (int s) {

 		return set[s, la.kind];

 	}

-

+	

 	void ExpectWeak (int n, int follow) {

 		if (la.kind == n) Get();

 		else {

@@ -182,7 +182,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		}

 	}

 

-

+	

 	void Dafny() {

 		ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;

 		Attributes attrs;  IToken/*!*/ id;  List<string/*!*/> theImports;

@@ -1100,7 +1100,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 	void VarDeclStatement(out Statement/*!*/ s) {

 		IToken x = null, assignTok = null;  bool isGhost = false;

 		VarDecl/*!*/ d;

-		AssignmentRhs r;  Expression lhs0;

+		AssignmentRhs r;  IdentifierExpr lhs0;

 		List<VarDecl> lhss = new List<VarDecl>();

 		List<AssignmentRhs> rhss = new List<AssignmentRhs>();

 		

@@ -1119,7 +1119,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 		}

 		if (la.kind == 49) {

 			Get();

-			assignTok = t;  lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name); 

+			assignTok = t;

+			lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);

+			lhs0.Var = lhss[0];  lhs0.Type = lhss[0].OptionalType;  // resolve here

+			

 			Rhs(out r, lhs0);

 			rhss.Add(r); 

 			while (la.kind == 19) {

@@ -1789,7 +1792,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); 

 			break;

 		}

-		case 38: case 55: case 61: case 62: case 63: case 98: case 99: case 100: case 101: {

+		case 18: case 38: case 55: case 61: case 62: case 63: case 98: case 99: case 100: case 101: {

 			EndlessExpression(out e);

 			break;

 		}

@@ -1845,6 +1848,8 @@ List<Expression/*!*/>/*!*/ decreases) {
 		IToken/*!*/ x;

 		Expression e0, e1;

 		e = dummyExpr;

+		BoundVar d;

+		List<BoundVar> letVars;  List<Expression> letRHSs;

 		

 		switch (la.kind) {

 		case 55: {

@@ -1888,6 +1893,31 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new AssumeExpr(x, e0, e1); 

 			break;

 		}

+		case 18: {

+			Get();

+			x = t;

+			letVars = new List<BoundVar>();

+			letRHSs = new List<Expression>(); 

+			IdentTypeOptional(out d);

+			letVars.Add(d); 

+			while (la.kind == 19) {

+				Get();

+				IdentTypeOptional(out d);

+				letVars.Add(d); 

+			}

+			Expect(49);

+			Expression(out e);

+			letRHSs.Add(e); 

+			while (la.kind == 19) {

+				Get();

+				Expression(out e);

+				letRHSs.Add(e); 

+			}

+			Expect(17);

+			Expression(out e);

+			e = new LetExpr(x, letVars, letRHSs, e); 

+			break;

+		}

 		default: SynErr(133); break;

 		}

 	}

@@ -2277,13 +2307,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 

 	public void Parse() {

 		la = new Token();

-		la.val = "";

+		la.val = "";		

 		Get();

 		Dafny();

 

-		Expect(0);

+    Expect(0);

 	}

-

+	

 	static readonly bool[,]/*!*/ set = {

 		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

 		{x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

@@ -2291,17 +2321,17 @@ List<Expression/*!*/>/*!*/ decreases) {
 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

 		{x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},

+		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},

 		{x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, x,x,x,T, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},

-		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},

+		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},

 		{x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,T,T, x,x,T,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},

+		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,T,T, x,x,T,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},

 		{x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},

 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

 		{x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, T,T,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, T,x,x,x, T,T,T,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, T,T,x,x, x,x,T,T, x,x},

-		{x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}

+		{x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}

 

 	};

 } // end Parser

@@ -2310,20 +2340,18 @@ List<Expression/*!*/>/*!*/ decreases) {
 public class Errors {

 	public int count = 0;                                    // number of errors detected

 	public System.IO.TextWriter/*!*/ errorStream = Console.Out;   // error messages go to this stream

-	public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text

-	public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text

-

+  public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text

+  public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text

+  

 	public void SynErr(string filename, int line, int col, int n) {

-		SynErr(filename, line, col, GetSyntaxErrorString(n));

-	}

-

-	public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {

-		Contract.Requires(msg != null);

+    SynErr(filename, line, col, GetSyntaxErrorString(n));

+  }

+	public virtual void SynErr(string filename, int line, int col, string msg) {

+	  Contract.Requires(msg != null);

 		errorStream.WriteLine(errMsgFormat, filename, line, col, msg);

 		count++;

-	}

-

-	string GetSyntaxErrorString(int n) {

+  }

+  string GetSyntaxErrorString(int n) {

 		string s;

 		switch (n) {

 			case 0: s = "EOF expected"; break;

@@ -2473,7 +2501,7 @@ public class Errors {
 

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

 		}

-		return s;

+    return s;

 	}

 

 	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {  // semantic errors

@@ -2481,9 +2509,8 @@ public class Errors {
 		Contract.Requires(msg != null);

 		SemErr(tok.filename, tok.line, tok.col, msg);

 	}

-

 	public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {

-		Contract.Requires(msg != null);

+	  Contract.Requires(msg != null);

 		errorStream.WriteLine(errMsgFormat, filename, line, col, msg);

 		count++;

 	}

diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index 10099bf4..5b9ba1d6 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -1014,6 +1014,23 @@ namespace Microsoft.Dafny {
         }

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

 

+      } else if (expr is LetExpr) {

+        var e = (LetExpr)expr;

+        bool parensNeeded = !isRightmost;

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

+        string sep = "";

+        foreach (var v in e.Vars) {

+          wr.Write("{0}{1}", sep, v.Name);

+          PrintType(": ", v.Type);

+          sep = ", ";

+        }

+        wr.Write(" := ");

+        PrintExpressionList(e.RHSs);

+        wr.Write("; ");

+        PrintExpression(e.Body);

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

+

+

       } else if (expr is QuantifierExpr) {

         QuantifierExpr e = (QuantifierExpr)expr;

         bool parensNeeded = !isRightmost;

@@ -1106,8 +1123,8 @@ namespace Microsoft.Dafny {
       string sep = "";

       foreach (BoundVar bv in boundVars) {

         wr.Write("{0}{1}", sep, bv.Name);

-        sep = ", ";

         PrintType(": ", bv.Type);

+        sep = ", ";

       }

       PrintAttributes(attrs);

       if (range != null) {

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index b6bc4059..81216f32 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -2751,6 +2751,30 @@ namespace Microsoft.Dafny {
         }

         e.ResolvedOp = ResolveOp(e.Op, e.E1.Type);

 

+      } else if (expr is LetExpr) {

+        var e = (LetExpr)expr;

+        foreach (var rhs in e.RHSs) {

+          ResolveExpression(rhs, twoState);

+        }

+        scope.PushMarker();

+        if (e.Vars.Count != e.RHSs.Count) {

+          Error(expr, "let expression must have same number of bound variables (found {0}) as RHSs (found {1})", e.Vars.Count, e.RHSs.Count);

+        }

+        int i = 0;

+        foreach (var v in e.Vars) {

+          if (!scope.Push(v.Name, v)) {

+            Error(v, "Duplicate let-variable name: {0}", v.Name);

+          }

+          ResolveType(v.tok, v.Type);

+          if (i < e.RHSs.Count && !UnifyTypes(v.Type, e.RHSs[i].Type)) {

+            Error(e.RHSs[i].tok, "type of RHS ({0}) does not match type of bound variable ({1})", e.RHSs[i].Type, v.Type);

+          }

+          i++;

+        }

+        ResolveExpression(e.Body, twoState);

+        scope.PopMarker();

+        expr.Type = e.Body.Type;

+

       } else if (expr is QuantifierExpr) {

         QuantifierExpr e = (QuantifierExpr)expr;

         int prevErrorCount = ErrorCount;

diff --git a/Dafny/Scanner.cs b/Dafny/Scanner.cs
index 634abf45..1ab06974 100644
--- a/Dafny/Scanner.cs
+++ b/Dafny/Scanner.cs
@@ -19,7 +19,7 @@ public class Buffer {
 	//    a) whole stream in buffer

 	//    b) part of stream in buffer

 	// 2) non seekable stream (network, console)

-

+  

 	public const int EOF = 65535 + 1; // char.MaxValue + 1;

 	const int MIN_BUFFER_LENGTH = 1024; // 1KB

 	const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB

@@ -31,17 +31,15 @@ public class Buffer {
 	Stream/*!*/ stream;      // input stream (seekable)

 	bool isUserStream;  // was the stream opened by the user?

 

-	[ContractInvariantMethod]

-	void ObjectInvariant(){

-		Contract.Invariant(buf != null);

-		Contract.Invariant(stream != null);

-	}

-

-//  [NotDelayed]

-	public Buffer (Stream/*!*/ s, bool isUserStream) : base() {

+[ContractInvariantMethod]

+void ObjectInvariant(){

+  Contract.Invariant(buf != null);

+  Contract.Invariant(stream != null);}

+    [NotDelayed]

+	public Buffer (Stream/*!*/ s, bool isUserStream) :base() {

 	  Contract.Requires(s != null);

 		stream = s; this.isUserStream = isUserStream;

-

+		

 		int fl, bl;

 		if (s.CanSeek) {

 			fl = (int) s.Length;

@@ -53,12 +51,12 @@ public class Buffer {
 

 		buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];

 		fileLen = fl;  bufLen = bl;

-

+		

 		if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start)

 		else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid

 		if (bufLen == fileLen && s.CanSeek) Close();

 	}

-

+	

 	protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor

 	  Contract.Requires(b != null);

 		buf = b.buf;

@@ -75,14 +73,14 @@ public class Buffer {
 	}

 

 	~Buffer() { Close(); }

-

+	

 	protected void Close() {

 		if (!isUserStream && stream != null) {

 			stream.Close();

 			//stream = null;

 		}

 	}

-

+	

 	public virtual int Read () {

 		if (bufPos < bufLen) {

 			return buf[bufPos++];

@@ -102,7 +100,7 @@ public class Buffer {
 		Pos = curPos;

 		return ch;

 	}

-

+	

 	public string/*!*/ GetString (int beg, int end) {

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

 		int len = 0;

@@ -141,7 +139,7 @@ public class Buffer {
 			}

 		}

 	}

-

+	

 	// Read the next chunk of bytes from the stream, increases the buffer

 	// if needed and updates the fields fileLen and bufLen.

 	// Returns the number of bytes read.

@@ -215,20 +213,19 @@ public class Scanner {
 	const int noSym = 104;

 

 

-	[ContractInvariantMethod]

-	void objectInvariant(){

-		Contract.Invariant(buffer!=null);

-		Contract.Invariant(t != null);

-		Contract.Invariant(start != null);

-		Contract.Invariant(tokens != null);

-		Contract.Invariant(pt != null);

-		Contract.Invariant(tval != null);

-		Contract.Invariant(Filename != null);

-		Contract.Invariant(errorHandler != null);

-	}

-

+[ContractInvariantMethod]

+void objectInvariant(){

+  Contract.Invariant(buffer!=null);

+  Contract.Invariant(t != null);

+  Contract.Invariant(start != null);

+  Contract.Invariant(tokens != null);

+  Contract.Invariant(pt != null);

+  Contract.Invariant(tval != null);

+  Contract.Invariant(Filename != null);

+  Contract.Invariant(errorHandler != null);

+}

 	public Buffer/*!*/ buffer; // scanner buffer

-

+	

 	Token/*!*/ t;          // current token

 	int ch;           // current input character

 	int pos;          // byte position of current character

@@ -239,13 +236,13 @@ public class Scanner {
 

 	Token/*!*/ tokens;     // list of tokens already peeked (first token is a dummy)

 	Token/*!*/ pt;         // current peek token

-

+	

 	char[]/*!*/ tval = new char[128]; // text of current token

 	int tlen;         // length of current token

-

+	

 	private string/*!*/ Filename;

 	private Errors/*!*/ errorHandler;

-

+	

 	static Scanner() {

 		start = new Hashtable(128);

 		for (int i = 39; i <= 39; ++i) start[i] = 1;

@@ -293,9 +290,9 @@ public class Scanner {
 		start[Buffer.EOF] = -1;

 

 	}

-

-//	[NotDelayed]

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

+	

+	[NotDelayed]

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

 	  Contract.Requires(fileName != null);

 	  Contract.Requires(errorHandler != null);

 		this.errorHandler = errorHandler;

@@ -305,14 +302,15 @@ public class Scanner {
 			Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);

 			buffer = new Buffer(stream, false);

 			Filename = fileName;

+			

 			Init();

 		} catch (IOException) {

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

 		}

 	}

-

-//	[NotDelayed]

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

+	

+	[NotDelayed]

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

 	  Contract.Requires(s != null);

 	  Contract.Requires(errorHandler != null);

 	  Contract.Requires(fileName != null);

@@ -321,9 +319,10 @@ public class Scanner {
 		buffer = new Buffer(s, true);

 		this.errorHandler = errorHandler;

 		this.Filename = fileName;

+		

 		Init();

 	}

-

+	

 	void Init() {

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

 		oldEols = 0;

@@ -344,11 +343,11 @@ public class Scanner {
 	Contract.Ensures(Contract.Result<string>() != null);

 	  int p = buffer.Pos;

 	  int ch = buffer.Read();

-	  // replace isolated '\r' by '\n' in order to make

+      // replace isolated '\r' by '\n' in order to make

 	  // eol handling uniform across Windows, Unix and Mac

 	  if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

 	  while (ch != EOL && ch != Buffer.EOF){

-		ch = buffer.Read();

+	    ch = buffer.Read();

 		// replace isolated '\r' by '\n' in order to make

 		// eol handling uniform across Windows, Unix and Mac

 		if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

@@ -359,7 +358,7 @@ public class Scanner {
 	}

 

 	void NextCh() {

-		if (oldEols > 0) { ch = EOL; oldEols--; }

+		if (oldEols > 0) { ch = EOL; oldEols--; } 

 		else {

 //			pos = buffer.Pos;

 //			ch = buffer.Read(); col++;

@@ -367,9 +366,9 @@ public class Scanner {
 //			// eol handling uniform across Windows, Unix and Mac

 //			if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

 //			if (ch == EOL) { line++; col = 0; }

-

+			

 			while (true) {

-				pos = buffer.Pos;

+			    pos = buffer.Pos;

 				ch = buffer.Read(); col++;

 				// replace isolated '\r' by '\n' in order to make

 				// eol handling uniform across Windows, Unix and Mac

@@ -419,7 +418,7 @@ public class Scanner {
 				return;

 			  }

 

-

+			

 		}

 

 	}

@@ -557,13 +556,10 @@ public class Scanner {
 		t.pos = pos; t.col = col; t.line = line;

 		t.filename = this.Filename;

 		int state;

-		if (start.ContainsKey(ch)) {

-			Contract.Assert(start[ch] != null);

-			state = (int) start[ch];

-		}

+		if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }

 		else { state = 0; }

 		tlen = 0; AddCh();

-

+		

 		switch (state) {

 			case -1: { t.kind = eofSym; break; } // NextCh already done

 			case 0: {

@@ -763,14 +759,14 @@ public class Scanner {
 		t.val = new String(tval, 0, tlen);

 		return t;

 	}

-

+	

 	private void SetScannerBehindT() {

 		buffer.Pos = t.pos;

 		NextCh();

 		line = t.line; col = t.col;

 		for (int i = 0; i < tlen; i++) NextCh();

 	}

-

+	

 	// get the next token (possibly a token already seen during peeking)

 	public Token/*!*/ Scan () {

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

@@ -791,7 +787,7 @@ public class Scanner {
 			}

 			pt = pt.next;

 		} while (pt.kind > maxT); // skip pragmas

-

+	

 		return pt;

 	}

 

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 028891b5..f3373736 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -1738,7 +1738,7 @@ namespace Microsoft.Dafny {
         return r;

       } else if (expr is OldExpr) {

         OldExpr e = (OldExpr)expr;

-        return new Bpl.OldExpr(expr.tok, IsTotal(e.E, etran));

+        return IsTotal(e.E, etran.Old);

       } else if (expr is MultiSetFormingExpr) {

         MultiSetFormingExpr e = (MultiSetFormingExpr)expr;

         return IsTotal(e.E, etran);

@@ -1780,6 +1780,14 @@ namespace Microsoft.Dafny {
         }

         Bpl.Expr r = BplAnd(t0, t1);

         return z == null ? r : BplAnd(r, z);

+      } else if (expr is LetExpr) {

+        var e = (LetExpr)expr;

+        Bpl.Expr total = Bpl.Expr.True;

+        foreach (var rhs in e.RHSs) {

+          total = BplAnd(total, IsTotal(rhs, etran));

+        }

+        return BplAnd(total, IsTotal(etran.GetSubstitutedBody(e), etran));

+

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

         var total = IsTotal(e.Term, etran);

@@ -1797,7 +1805,7 @@ namespace Microsoft.Dafny {
         Bpl.Expr gTotal = IsTotal(e.Guard, etran);

         Bpl.Expr g = etran.TrExpr(e.Guard);

         Bpl.Expr bTotal = IsTotal(e.Body, etran);

-        if (e is AssertExpr) {

+        if (e is AssertExpr || CommandLineOptions.Clo.DisallowSoundnessCheating) {

           return BplAnd(gTotal, BplAnd(g, bTotal));

         } else {

           return BplAnd(gTotal, Bpl.Expr.Imp(g, bTotal));

@@ -1896,7 +1904,7 @@ namespace Microsoft.Dafny {
         return CanCallAssumption(dtv.Arguments, etran);

       } else if (expr is OldExpr) {

         OldExpr e = (OldExpr)expr;

-        return new Bpl.OldExpr(expr.tok, CanCallAssumption(e.E, etran));

+        return CanCallAssumption(e.E, etran.Old);

       } else if (expr is MultiSetFormingExpr) {

         MultiSetFormingExpr e = (MultiSetFormingExpr)expr;

         return CanCallAssumption(e.E, etran);

@@ -1926,6 +1934,14 @@ namespace Microsoft.Dafny {
             break;

         }

         return BplAnd(t0, t1);

+      } else if (expr is LetExpr) {

+        var e = (LetExpr)expr;

+        Bpl.Expr canCall = Bpl.Expr.True;

+        foreach (var rhs in e.RHSs) {

+          canCall = BplAnd(canCall, CanCallAssumption(rhs, etran));

+        }

+        return BplAnd(canCall, CanCallAssumption(etran.GetSubstitutedBody(e), etran));

+

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

         var total = CanCallAssumption(e.Term, etran);

@@ -1941,11 +1957,11 @@ namespace Microsoft.Dafny {
       } else if (expr is PredicateExpr) {

         var e = (PredicateExpr)expr;

         Bpl.Expr gCanCall = CanCallAssumption(e.Guard, etran);

-        Bpl.Expr g = etran.TrExpr(e.Guard);

         Bpl.Expr bCanCall = CanCallAssumption(e.Body, etran);

-        if (e is AssertExpr) {

-          return BplAnd(gCanCall, BplAnd(g, bCanCall));

+        if (e is AssertExpr || CommandLineOptions.Clo.DisallowSoundnessCheating) {

+          return BplAnd(gCanCall, bCanCall);

         } else {

+          Bpl.Expr g = etran.TrExpr(e.Guard);

           return BplAnd(gCanCall, Bpl.Expr.Imp(g, bCanCall));

         }

       } else if (expr is ITEExpr) {

@@ -2328,6 +2344,13 @@ namespace Microsoft.Dafny {
             break;

         }

 

+      } else if (expr is LetExpr) {

+        var e = (LetExpr)expr;

+        foreach (var rhs in e.RHSs) {

+          CheckWellformed(rhs, options, locals, builder, etran);

+        }

+        CheckWellformedWithResult(etran.GetSubstitutedBody(e), options, result, resultType, locals, builder, etran);

+

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

         var substMap = SetupBoundVarsAsLocals(e.BoundVars, builder, locals, etran);

@@ -2346,7 +2369,7 @@ namespace Microsoft.Dafny {
       } else if (expr is PredicateExpr) {

         var e = (PredicateExpr)expr;

         CheckWellformed(e.Guard, options, locals, builder, etran);

-        if (e is AssertExpr) {

+        if (e is AssertExpr || CommandLineOptions.Clo.DisallowSoundnessCheating) {

           bool splitHappened;

           var ss = TrSplitExpr(e.Guard, etran, out splitHappened);

           if (!splitHappened) {

@@ -4146,7 +4169,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(locals != null);

       Contract.Requires(etran != null);

 

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

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

       Bpl.ExprSeq ins = new Bpl.ExprSeq();

       if (!method.IsStatic) {

         if (bReceiver == null) {

@@ -5002,11 +5025,13 @@ namespace Microsoft.Dafny {
     internal class BoogieWrapper : Expression

     {

       public readonly Bpl.Expr Expr;

-      public BoogieWrapper(Bpl.Expr expr)

+      public BoogieWrapper(Bpl.Expr expr, Type dafnyType)

         : base(expr.tok)

       {

         Contract.Requires(expr != null);

+        Contract.Requires(dafnyType != null);

         Expr = expr;

+        Type = dafnyType;  // resolve immediately

       }

     }

 

@@ -5016,7 +5041,7 @@ namespace Microsoft.Dafny {
       public readonly PredefinedDecls predef;

       public readonly Translator translator;

       public readonly string This;

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

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

       readonly Function applyLimited_CurrentFunction;

       public readonly int layerOffset = 0;

       public int Statistics_CustomLayerFunctionCount = 0;

@@ -5027,66 +5052,60 @@ namespace Microsoft.Dafny {
         Contract.Invariant(predef != null);

         Contract.Invariant(translator != null);

         Contract.Invariant(This != null);

+        Contract.Invariant(modifiesFrame != null);

         Contract.Invariant(layerOffset == 0 || layerOffset == 1);

         Contract.Invariant(0 <= Statistics_CustomLayerFunctionCount);

       }

 

-      public ExpressionTranslator(Translator translator, PredefinedDecls predef, IToken heapToken) {

+      /// <summary>

+      /// This is the most general constructor.  It is private and takes all the parameters.  Whenever

+      /// one ExpressionTranslator is constructed from another, unchanged parameters are just copied in.

+      /// </summary>

+      ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, string thisVar,

+        Function applyLimited_CurrentFunction, int layerOffset, string modifiesFrame) {

+

         Contract.Requires(translator != null);

         Contract.Requires(predef != null);

-        Contract.Requires(heapToken != null);

+        Contract.Requires(heap != null);

+        Contract.Requires(thisVar != null);

+        Contract.Invariant(layerOffset == 0 || layerOffset == 1);

+        Contract.Invariant(modifiesFrame != null);

+

         this.translator = translator;

         this.predef = predef;

-        this.HeapExpr = new Bpl.IdentifierExpr(heapToken, predef.HeapVarName, predef.HeapType);

-        this.This = "this";

+        this.HeapExpr = heap;

+        this.This = thisVar;

+        this.applyLimited_CurrentFunction = applyLimited_CurrentFunction;

+        this.layerOffset = layerOffset;

+        this.modifiesFrame = modifiesFrame;

       }

 

-      public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap) {

+      public ExpressionTranslator(Translator translator, PredefinedDecls predef, IToken heapToken)

+        : this(translator, predef, new Bpl.IdentifierExpr(heapToken, predef.HeapVarName, predef.HeapType)) {

         Contract.Requires(translator != null);

         Contract.Requires(predef != null);

-        Contract.Requires(heap != null);

-        this.translator = translator;

-        this.predef = predef;

-        this.HeapExpr = heap;

-        this.This = "this";

+        Contract.Requires(heapToken != null);

       }

 

-      public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, string thisVar) {

+      public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap)

+        : this(translator, predef, heap, "this") {

         Contract.Requires(translator != null);

         Contract.Requires(predef != null);

         Contract.Requires(heap != null);

-        Contract.Requires(thisVar != null);

-        this.translator = translator;

-        this.predef = predef;

-        this.HeapExpr = heap;

-        this.This = thisVar;

       }

 

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

-      {

-          Contract.Requires(translator != null);

-          Contract.Requires(predef != null);

-          Contract.Requires(heap != null);

-          this.translator = translator;

-          this.predef = predef;

-          this.HeapExpr = heap;

-          this.applyLimited_CurrentFunction = applyLimited_CurrentFunction;

-          this.This = "this";

-          this.layerOffset = layerOffset;

+      public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, string thisVar)

+        : this(translator, predef, heap, thisVar, null, 0, "$_Frame") {

+        Contract.Requires(translator != null);

+        Contract.Requires(predef != null);

+        Contract.Requires(heap != null);

+        Contract.Requires(thisVar != null);

       }

 

       public ExpressionTranslator(ExpressionTranslator etran, string modifiesFrame)

-      {

-          Contract.Requires(etran != null);

-          Contract.Requires(modifiesFrame != null);

-          this.translator = etran.translator;

-          this.HeapExpr = etran.HeapExpr;

-          this.predef = etran.predef;

-          this.This = etran.This;

-          this.applyLimited_CurrentFunction = etran.applyLimited_CurrentFunction;

-          this.layerOffset = etran.layerOffset;

-          this.oldEtran = etran.oldEtran;

-          this.modifiesFrame = modifiesFrame;

+        : this(etran.translator, etran.predef, etran.HeapExpr, etran.This, etran.applyLimited_CurrentFunction, etran.layerOffset, modifiesFrame) {

+        Contract.Requires(etran != null);

+        Contract.Requires(modifiesFrame != null);

       }

 

       ExpressionTranslator oldEtran;

@@ -5095,7 +5114,7 @@ namespace Microsoft.Dafny {
           Contract.Ensures(Contract.Result<ExpressionTranslator>() != null);

 

           if (oldEtran == null) {

-            oldEtran = new ExpressionTranslator(translator, predef, new Bpl.OldExpr(HeapExpr.tok, HeapExpr), applyLimited_CurrentFunction, layerOffset);

+            oldEtran = new ExpressionTranslator(translator, predef, new Bpl.OldExpr(HeapExpr.tok, HeapExpr), This, applyLimited_CurrentFunction, layerOffset, modifiesFrame);

           }

           return oldEtran;

         }

@@ -5111,7 +5130,7 @@ namespace Microsoft.Dafny {
         Contract.Requires(applyLimited_CurrentFunction != null);

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

 

-        return new ExpressionTranslator(translator, predef, HeapExpr, applyLimited_CurrentFunction, layerOffset);

+        return new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerOffset, modifiesFrame);

       }

 

       public ExpressionTranslator LayerOffset(int offset) {

@@ -5119,7 +5138,7 @@ namespace Microsoft.Dafny {
         Contract.Requires(layerOffset + offset <= 1);

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

 

-        return new ExpressionTranslator(translator, predef, HeapExpr, applyLimited_CurrentFunction, layerOffset + offset);

+        return new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerOffset + offset, modifiesFrame);

       }

 

       public Bpl.IdentifierExpr TheFrame(IToken tok)

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

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

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

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

+        return new Bpl.IdentifierExpr(tok, this.modifiesFrame, ty);

       }

 

       public Bpl.IdentifierExpr Tick() {

@@ -5141,24 +5160,33 @@ namespace Microsoft.Dafny {
         return new Bpl.IdentifierExpr(Token.NoToken, "$Tick", predef.TickType);

       }

 

-      public Bpl.IdentifierExpr ModuleContextHeight()

-        {

-       Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>().Type != null);

+      public Bpl.IdentifierExpr ModuleContextHeight() {

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

         return new Bpl.IdentifierExpr(Token.NoToken, "$ModuleContextHeight", Bpl.Type.Int);

       }

 

-      public Bpl.IdentifierExpr FunctionContextHeight()

-        {

-       Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>().Type != null);

+      public Bpl.IdentifierExpr FunctionContextHeight() {

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

         return new Bpl.IdentifierExpr(Token.NoToken, "$FunctionContextHeight", Bpl.Type.Int);

       }

 

-      public Bpl.IdentifierExpr InMethodContext()

-        {

-       Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>().Type != null);

+      public Bpl.IdentifierExpr InMethodContext() {

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

         return new Bpl.IdentifierExpr(Token.NoToken, "$InMethodContext", Bpl.Type.Bool);

       }

 

+      public Expression GetSubstitutedBody(LetExpr e) {

+        Contract.Requires(e != null);

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

+        Contract.Assert(e.Vars.Count == e.RHSs.Count);  // checked by resolution

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

+          Expression rhs = e.RHSs[i];

+          substMap.Add(e.Vars[i], new BoogieWrapper(TrExpr(rhs), rhs.Type));

+        }

+        return Translator.Substitute(e.Body, null, substMap);

+      }

+

+

       /// <summary>

       /// Translates Dafny expression "expr" into a Boogie expression.  If the type of "expr" can be a boolean, then the

       /// token (source location) of the resulting expression is filled in (it wouldn't hurt if the token were always

@@ -5329,7 +5357,7 @@ namespace Microsoft.Dafny {
 

         } else if (expr is OldExpr) {

           OldExpr e = (OldExpr)expr;

-          return new Bpl.OldExpr(expr.tok, TrExpr(e.E));

+          return Old.TrExpr(e.E);

 

         } else if (expr is MultiSetFormingExpr) {

           MultiSetFormingExpr e = (MultiSetFormingExpr)expr;

@@ -5344,7 +5372,6 @@ namespace Microsoft.Dafny {
 

         } else if (expr is FreshExpr) {

           FreshExpr e = (FreshExpr)expr;

-          Bpl.Expr oldHeap = new Bpl.OldExpr(expr.tok, HeapExpr);

           if (e.E.Type is SetType) {

             // generate:  (forall $o: ref :: $o != null && X[Box($o)] ==> !old($Heap)[$o,alloc])

             // TODO: trigger?

@@ -5352,7 +5379,7 @@ namespace Microsoft.Dafny {
             Bpl.Expr o = new Bpl.IdentifierExpr(expr.tok, oVar);

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

             Bpl.Expr oInSet = TrInSet(expr.tok, o, e.E, ((SetType)e.E.Type).Arg);

-            Bpl.Expr oIsFresh = Bpl.Expr.Not(IsAlloced(expr.tok, o, oldHeap));

+            Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, o));

             Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(oNotNull, oInSet), oIsFresh);

             return new Bpl.ForallExpr(expr.tok, new Bpl.VariableSeq(oVar), body);

           } else if (e.E.Type is SeqType) {

@@ -5362,14 +5389,14 @@ namespace Microsoft.Dafny {
             Bpl.Expr i = new Bpl.IdentifierExpr(expr.tok, iVar);

             Bpl.Expr iBounds = translator.InSeqRange(expr.tok, i, TrExpr(e.E), true, null, false);

             Bpl.Expr XsubI = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.RefType, TrExpr(e.E), i);

-            Bpl.Expr oIsFresh = Bpl.Expr.Not(IsAlloced(expr.tok, XsubI, oldHeap));

+            Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, XsubI));

             Bpl.Expr xsubiNotNull = Bpl.Expr.Neq(translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, predef.RefType, XsubI), predef.Null);

             Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(iBounds, xsubiNotNull), oIsFresh);

             return new Bpl.ForallExpr(expr.tok, new Bpl.VariableSeq(iVar), body);

           } else {

             // generate:  x == null || !old($Heap)[x]

             Bpl.Expr oNull = Bpl.Expr.Eq(TrExpr(e.E), predef.Null);

-            Bpl.Expr oIsFresh = Bpl.Expr.Not(IsAlloced(expr.tok, TrExpr(e.E), oldHeap));

+            Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, TrExpr(e.E)));

             return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.Or, oNull, oIsFresh);

           }

 

@@ -5546,6 +5573,10 @@ namespace Microsoft.Dafny {
           }

           return Bpl.Expr.Binary(expr.tok, bOpcode, e0, e1);

 

+        } else if (expr is LetExpr) {

+          var e = (LetExpr)expr;

+          return TrExpr(GetSubstitutedBody(e));

+

         } else if (expr is QuantifierExpr) {

           QuantifierExpr e = (QuantifierExpr)expr;

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

@@ -5930,16 +5961,7 @@ namespace Microsoft.Dafny {
         Contract.Requires(e != null);

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

 

-        return IsAlloced(tok, e, HeapExpr);

-      }

-

-      Bpl.Expr IsAlloced(IToken tok, Bpl.Expr e, Bpl.Expr heap) {

-        Contract.Requires(tok != null);

-        Contract.Requires(e != null);

-        Contract.Requires(heap != null);

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

-

-        return ReadHeap(tok, heap, e, predef.Alloc(tok));

+        return ReadHeap(tok, HeapExpr, e, predef.Alloc(tok));

       }

 

       public Bpl.Expr GoodRef(IToken tok, Bpl.Expr e, Type type) {

@@ -6401,9 +6423,9 @@ namespace Microsoft.Dafny {
         var e = (ConcreteSyntaxExpression)expr;

         return TrSplitExpr(e.ResolvedExpression, splits, position, expandFunctions, etran);

 

-      } else if (expr is PredicateExpr) {

-        var e = (PredicateExpr)expr;

-        return TrSplitExpr(e.Body, splits, position, expandFunctions, etran);

+      } else if (expr is LetExpr) {

+        var e = (LetExpr)expr;

+        return TrSplitExpr(etran.GetSubstitutedBody(e), splits, position, expandFunctions, etran);

 

       } else if (expr is UnaryExpr) {

         var e = (UnaryExpr)expr;

@@ -6474,15 +6496,33 @@ namespace Microsoft.Dafny {
           return true;

         }

 

-      } else if (expr is OldExpr) {

-        var e = (OldExpr)expr;

-        var ss = new List<SplitExprInfo>();

-        if (TrSplitExpr(e.E, ss, position, expandFunctions, etran)) {

+      } else if (expr is PredicateExpr) {

+        var e = (PredicateExpr)expr;

+        // For a predicate expression in split position, the predicate can be used as an assumption.  Unfortunately,

+        // this assumption is not generated in non-split positions (because I don't know how.)

+        // So, treat "assert/assume P; E" like "P ==> E".

+        if (position) {

+          var guard = etran.TrExpr(e.Guard);

+          var ss = new List<SplitExprInfo>();

+          TrSplitExpr(e.Body, ss, position, expandFunctions, etran);

+          foreach (var s in ss) {

+            // as the source location in the following implication, use that of the translated "s"

+            splits.Add(new SplitExprInfo(s.IsFree, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, guard, s.E)));

+          }

+        } else {

+          var ss = new List<SplitExprInfo>();

+          TrSplitExpr(e.Guard, ss, !position, expandFunctions, etran);

+          var rhs = etran.TrExpr(e.Body);

           foreach (var s in ss) {

-            splits.Add(new SplitExprInfo(s.IsFree, new Bpl.OldExpr(s.E.tok, s.E)));

+            // as the source location in the following implication, use that of the translated "s"

+            splits.Add(new SplitExprInfo(s.IsFree, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, s.E, rhs)));

           }

-          return true;

         }

+        return true;

+

+      } else if (expr is OldExpr) {

+        var e = (OldExpr)expr;

+        return TrSplitExpr(e.E, splits, position, expandFunctions, etran.Old);

 

       } else if (expandFunctions && position && expr is FunctionCallExpr) {

         var fexp = (FunctionCallExpr)expr;

@@ -6845,9 +6885,6 @@ namespace Microsoft.Dafny {
         var e = (DatatypeValue)expr;

         var q = n.Type.IsDatatype ? exprIsProminent : subExprIsProminent;  // prominent status continues, if we're looking for a variable whose type is a datatype

         return e.Arguments.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, q));

-      } else if (expr is OldExpr) {

-        var e = (OldExpr)expr;

-        return VarOccursInArgumentToRecursiveFunction(e.E, n, exprIsProminent);  // prominent status continues

       } else if (expr is UnaryExpr) {

         var e = (UnaryExpr)expr;

         // both Not and SeqLength preserve prominence

@@ -6965,7 +7002,7 @@ namespace Microsoft.Dafny {
       }

     }

 

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

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

       Contract.Requires(expr != null);

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

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

@@ -7051,7 +7088,11 @@ namespace Microsoft.Dafny {
 

       } else if (expr is OldExpr) {

         OldExpr e = (OldExpr)expr;

-        Expression se = Substitute(e.E, receiverReplacement, substMap);  // TODO: whoa, won't this do improper variable capture?

+        // Note, it is up to the caller to avoid variable capture.  In most cases, this is not a

+        // problem, since variables have unique declarations.  However, it is an issue if the substitution

+        // takes place inside an OldExpr.  In those cases (see LetExpr), the caller can use a

+        // BoogieWrapper before calling Substitute.

+        Expression se = Substitute(e.E, receiverReplacement, substMap);

         if (se != e.E) {

           newExpr = new OldExpr(expr.tok, se);

         }

@@ -7083,6 +7124,22 @@ namespace Microsoft.Dafny {
           newExpr = newBin;

         }

 

+      } else if (expr is LetExpr) {

+        var e = (LetExpr)expr;

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

+        bool anythingChanged = false;

+        foreach (var rhs in e.RHSs) {

+          var r = Substitute(rhs, receiverReplacement, substMap);

+          if (r != rhs) {

+            anythingChanged = true;

+          }

+          rhss.Add(r);

+        }

+        var body = Substitute(e.Body, receiverReplacement, substMap);

+        if (anythingChanged || body != e.Body) {

+          newExpr = new LetExpr(e.tok, e.Vars, rhss, body);

+        }

+

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

         Expression newRange = e.Range == null ? null : Substitute(e.Range, receiverReplacement, substMap);

@@ -7109,10 +7166,12 @@ namespace Microsoft.Dafny {
         var e = (PredicateExpr)expr;

         Expression g = Substitute(e.Guard, receiverReplacement, substMap);

         Expression b = Substitute(e.Body, receiverReplacement, substMap);

-        if (expr is AssertExpr) {

-          newExpr = new AssertExpr(e.tok, g, b);

-        } else {

-          newExpr = new AssumeExpr(e.tok, g, b);

+        if (g != e.Guard || b != e.Body) {

+          if (expr is AssertExpr) {

+            newExpr = new AssertExpr(e.tok, g, b);

+          } else {

+            newExpr = new AssumeExpr(e.tok, g, b);

+          }

         }

 

       } else if (expr is ITEExpr) {

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 50c238fc..15cec24f 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1321,12 +1321,33 @@ CallStmtTests.dfy(15,8): Error: actual out-parameter 0 is required to be a ghost
 Dafny program verifier finished with 22 verified, 0 errors

 

 -------------------- PredExpr.dfy --------------------

-PredExpr.dfy(23,15): Error: value assigned to a nat must be non-negative

+PredExpr.dfy(4,12): Error: condition in assert expression might not hold

+Execution trace:

+    (0,0): anon3_Else

+PredExpr.dfy(36,15): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon6_Else

     (0,0): anon7_Else

-PredExpr.dfy(36,17): Error: condition in assert expression might not hold

+PredExpr.dfy(49,17): Error: condition in assert expression might not hold

+Execution trace:

+    (0,0): anon0

+PredExpr.dfy(74,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon8_Else

+    (0,0): anon3

+    PredExpr.dfy(73,20): anon10_Else

+    (0,0): anon6

+

+Dafny program verifier finished with 11 verified, 4 errors

+

+-------------------- LetExpr.dfy --------------------

+LetExpr.dfy(5,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

+LetExpr.dfy(104,21): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon11_Then

 

-Dafny program verifier finished with 9 verified, 2 errors

+Dafny program verifier finished with 13 verified, 2 errors

diff --git a/Test/dafny0/LetExpr.dfy b/Test/dafny0/LetExpr.dfy
new file mode 100644
index 00000000..703813d2
--- /dev/null
+++ b/Test/dafny0/LetExpr.dfy
@@ -0,0 +1,109 @@
+method M0(n: int)

+  requires var f := 100; n < f;

+{

+  assert n < 200;

+  assert 0 <= n;  // error

+}

+

+method M1()

+{

+  assert var f := 54; var g := f + 1; g == 55;

+}

+

+method M2()

+{

+  assert var f := 54; var f := f + 1; f == 55;

+}

+

+function method Fib(n: nat): nat

+{

+  if n < 2 then n else Fib(n-1) + Fib(n-2)

+}

+

+method M3(a: array<int>) returns (r: int)

+  requires a != null && forall i :: 0 <= i < a.Length ==> a[i] == 6;

+  ensures (r + var t := r; t*2) == 3*r;

+{

+  assert Fib(2) + Fib(4) == Fib(0) + Fib(1) + Fib(2) + Fib(3);

+

+  {

+    var x,y := Fib(8), Fib(11);

+    assume x == 21;

+    assert Fib(7) == 3 ==> Fib(9) == 24;

+    assume Fib(1000) == 1000;

+    assume Fib(9) - Fib(8) == 13;

+    assert Fib(9) <= Fib(10);

+    assert y == 89;

+  }

+

+  assert Fib(1000) == 1000;  // does it still know this?

+

+  parallel (i | 0 <= i < a.Length) ensures true; {

+    var j := i+1;

+    assert j < a.Length ==> a[i] == a[j];

+  }

+}

+

+// M4 is pretty much the same as M3, except with things rolled into expressions.

+method M4(a: array<int>) returns (r: int)

+  requires a != null && forall i :: 0 <= i < a.Length ==> a[i] == 6;

+  ensures (r + var t := r; t*2) == 3*r;

+{

+  assert Fib(2) + Fib(4) == Fib(0) + Fib(1) + Fib(2) + Fib(3);

+  assert

+    var x,y := Fib(8), Fib(11);

+    assume x == 21;

+    assert Fib(7) == 3 ==> Fib(9) == 24;

+    assume Fib(1000) == 1000;

+    assume Fib(9) - Fib(8) == 13;

+    assert Fib(9) <= Fib(10);

+    y == 89;

+  assert Fib(1000) == 1000;  // still known, because the assume was on the path here

+  assert forall i :: 0 <= i < a.Length ==> var j := i+1; j < a.Length ==> a[i] == a[j];

+}

+

+var index: int;

+method P(a: array<int>) returns (b: bool, ii: int)

+  requires a != null && exists k :: 0 <= k < a.Length && a[k] == 19;

+  modifies this, a;

+  ensures ii == index;

+  // The following uses a variable with a non-old definition inside an old expression:

+  ensures 0 <= index < a.Length && old(a[ii]) == 19;

+  ensures 0 <= index < a.Length && var newIndex := index; old(a[newIndex]) == 19;

+  // The following places both the variable and the body inside an old:

+  ensures b ==> old(var oldIndex := index; 0 <= oldIndex < a.Length && a[oldIndex] == 17);

+  // Here, the definition of the variable is old, and it's used both inside and

+  // inside an old expression:

+  ensures var oi := old(index); oi == index ==> a[oi] == 21 && old(a[oi]) == 19;

+{

+  b := 0 <= index < a.Length && a[index] == 17;

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

+  while (i < a.Length)

+    invariant 0 <= i <= a.Length;

+    invariant forall k :: 0 <= k < i ==> a[k] == 21;

+    invariant forall k :: i <= k < a.Length ==> a[k] == old(a[k]);

+    invariant (0 <= j < i && old(a[j]) == 19) ||

+              (j == -1 && exists k :: i <= k < a.Length && a[k] == 19);

+  {

+    if (a[i] == 19) { j := i; }

+    i, a[i] := i + 1, 21;

+  }

+  index := j;

+  ii := index;

+}

+

+method PMain(a: array<int>)

+  requires a != null && exists k :: 0 <= k < a.Length && a[k] == 19;

+  modifies this, a;

+{

+  var s := a[..];

+  var b17, ii := P(a);

+  assert s == old(a[..]);

+  assert s[index] == 19;

+  if (*) {

+    assert a[index] == 19;  // error (a can have changed in P)

+  } else {

+    assert b17 ==> 0 <= old(index) < a.Length && old(a[index]) == 17;

+    assert index == old(index) ==> a[index] == 21 && old(a[index]) == 19;

+  }

+}

diff --git a/Test/dafny0/PredExpr.dfy b/Test/dafny0/PredExpr.dfy
index 740c2308..96561ebd 100644
--- a/Test/dafny0/PredExpr.dfy
+++ b/Test/dafny0/PredExpr.dfy
@@ -1,3 +1,16 @@
+function SimpleAssert(n: int): int

+  ensures n < 100;

+{

+  assert n == 58;  // error: assert violation

+  n  // but postcondition is fine

+}

+

+function SimpleAssume(n: int): int

+  ensures n < 100;

+{

+  assume n == 58; n  // all is fine

+}

+

 function Subonacci(n: nat): nat

 {

   if 2 <= n then

@@ -18,7 +31,7 @@ function F(n: int): nat
 function G(n: int, b: bool): nat

 {

   if b then

-    Subonacci(assume 0 <= n; n)

+    Subonacci(assume 0 <= n; n) + n  // the last n is also affected by the assume

   else

     Subonacci(n)  // error: n may not be a nat

 }

@@ -49,3 +62,18 @@ function method FuncMeth(): int {
                       // PredicateExpr is not included in compilation

   15

 }

+

+method M5(a: int, b: int)

+{

+  var k := if a < 0 then

+             assume b < 0; 5

+           else

+             5;

+  if (*) {

+    assert a == -7 ==> b < 0;

+    assert b < 0;  // error: this condition does not hold on every path here

+  } else {

+    assert assume a == -7; b < 0;  // note, this is different than the ==> above

+    assert b < 0;  // this condition does hold on all paths to here

+  }

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 32a60340..18c23e55 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -20,7 +20,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy

             Refinement.dfy RefinementErrors.dfy LoopModifies.dfy

             ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy

-            CallStmtTests.dfy MultiSets.dfy PredExpr.dfy) do (

+            CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f