Dafny: added assert/assume expressions

7 files changed, 186 insertions, 16 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 61b0398f..de863e39 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1767,6 +1767,10 @@ namespace Microsoft.Dafny {
         wr.Write("return Dafny.Set<{0}>.FromCollection(_coll); ", typeName);

         wr.Write("})()");

 

+      } else if (expr is PredicateExpr) {

+        var e = (PredicateExpr)expr;

+        TrExpr(e.Body);

+

       } else if (expr is ITEExpr) {

         ITEExpr e = (ITEExpr)expr;

         wr.Write("(");

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index fa857aad..8a9108f0 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1205,13 +1205,19 @@ EndlessExpression<out Expression e>
      Expression e0, e1;

      e = dummyExpr;

   .)

-  ( "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; .)

+    Expression<out e0> ";"

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

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

+    Expression<out e0> ";"

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

   )

   .

 MatchExpression<out Expression/*!*/ e>

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index bf8eb6b0..04b6b00e 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2721,7 +2721,52 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public class ITEExpr : Expression {

+  public abstract class PredicateExpr : Expression

+  {

+    public readonly Expression Guard;

+    public readonly Expression Body;

+    public PredicateExpr(IToken tok, Expression guard, Expression body)

+      : base(tok) {

+      Contract.Requires(tok != null);

+      Contract.Requires(guard != null);

+      Contract.Requires(body != null);

+      Guard = guard;

+      Body = body;

+    }

+    public abstract string Kind { get; }

+

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        yield return Guard;

+        yield return Body;

+      }

+    }

+  }

+

+  public class AssertExpr : PredicateExpr

+  {

+    public AssertExpr(IToken tok, Expression guard, Expression body)

+      : base(tok, guard, body) {

+      Contract.Requires(tok != null);

+      Contract.Requires(guard != null);

+      Contract.Requires(body != null);

+    }

+    public override string Kind { get { return "assert"; } }

+  }

+

+  public class AssumeExpr : PredicateExpr

+  {

+    public AssumeExpr(IToken tok, Expression guard, Expression body)

+      : base(tok, guard, body) {

+      Contract.Requires(tok != null);

+      Contract.Requires(guard != null);

+      Contract.Requires(body != null);

+    }

+    public override string Kind { get { return "assume"; } }

+  }

+

+  public class ITEExpr : Expression

+  {

     public readonly Expression Test;

     public readonly Expression Thn;

     public readonly Expression Els;

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 2fc50c37..0dc30e8a 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1789,7 +1789,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); 

 			break;

 		}

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

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

 			EndlessExpression(out e);

 			break;

 		}

@@ -1846,7 +1846,8 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expression e0, e1;

 		e = dummyExpr;

 		

-		if (la.kind == 55) {

+		switch (la.kind) {

+		case 55: {

 			Get();

 			x = t; 

 			Expression(out e);

@@ -1855,13 +1856,40 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Expect(56);

 			Expression(out e1);

 			e = new ITEExpr(x, e, e0, e1); 

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

+			break;

+		}

+		case 61: {

 			MatchExpression(out e);

-		} else if (StartOf(15)) {

+			break;

+		}

+		case 98: case 99: case 100: case 101: {

 			QuantifierGuts(out e);

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

+			break;

+		}

+		case 38: {

 			ComprehensionExpr(out e);

-		} else SynErr(133);

+			break;

+		}

+		case 62: {

+			Get();

+			x = t; 

+			Expression(out e0);

+			Expect(17);

+			Expression(out e1);

+			e = new AssertExpr(x, e0, e1); 

+			break;

+		}

+		case 63: {

+			Get();

+			x = t; 

+			Expression(out e0);

+			Expect(17);

+			Expression(out e1);

+			e = new AssumeExpr(x, e0, e1); 

+			break;

+		}

+		default: SynErr(133); break;

+		}

 	}

 

 	void DottedIdentifiersAndFunction(out Expression e) {

@@ -2014,7 +2042,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Expression(out e);

 			e = new MultiSetFormingExpr(x, e); 

 			Expect(34);

-		} else if (StartOf(16)) {

+		} else if (StartOf(15)) {

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

 		} else SynErr(138);

 	}

@@ -2233,7 +2261,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expect(22);

 		Expect(1);

 		aName = t.val; 

-		if (StartOf(17)) {

+		if (StartOf(16)) {

 			AttributeArg(out aArg);

 			aArgs.Add(aArg); 

 			while (la.kind == 19) {

@@ -2263,18 +2291,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,x,x, 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,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,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,x,x, 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,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,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,x,x, 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,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,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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,x,x, 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,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}

 

 	};

 } // end Parser

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 7f7ba963..10099bf4 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1054,6 +1054,16 @@ namespace Microsoft.Dafny {
       } else if (expr is WildcardExpr) {

         wr.Write("*");

 

+      } else if (expr is PredicateExpr) {

+        var e = (PredicateExpr)expr;

+        bool parensNeeded = !isRightmost;

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

+        wr.Write("{0} ", e.Kind);

+        PrintExpression(e.Guard);

+        wr.Write("; ");

+        PrintExpression(e.Body);

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

+

       } else if (expr is ITEExpr) {

         ITEExpr ite = (ITEExpr)expr;

         bool parensNeeded = !isRightmost;

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 2d3ddcca..c7fb8481 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2823,6 +2823,17 @@ namespace Microsoft.Dafny {
       } else if (expr is WildcardExpr) {

         expr.Type = new SetType(new ObjectType());

 

+      } else if (expr is PredicateExpr) {

+        var e = (PredicateExpr)expr;

+        ResolveExpression(e.Guard, twoState);

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

+        ResolveExpression(e.Body, twoState);

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

+        if (!UnifyTypes(e.Guard.Type, Type.Bool)) {

+          Error(expr, "guard condition in {0} expression must be a boolean (instead got {1})", e.Kind, e.Guard.Type);

+        }

+        expr.Type = e.Body.Type;

+

       } else if (expr is ITEExpr) {

         ITEExpr e = (ITEExpr)expr;

         ResolveExpression(e.Test, twoState);

@@ -3932,6 +3943,9 @@ namespace Microsoft.Dafny {
         return (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term));

       } else if (expr is WildcardExpr) {

         return false;

+      } else if (expr is PredicateExpr) {

+        var e = (PredicateExpr)expr;

+        return UsesSpecFeatures(e.Body);

       } else if (expr is ITEExpr) {

         ITEExpr e = (ITEExpr)expr;

         return UsesSpecFeatures(e.Test) || UsesSpecFeatures(e.Thn) || UsesSpecFeatures(e.Els);

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index e455561a..37f80bf1 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1789,6 +1789,16 @@ namespace Microsoft.Dafny {
           total = new Bpl.ForallExpr(expr.tok, bvars, Bpl.Expr.Imp(typeAntecedent, total));

         }

         return total;

+      } else if (expr is PredicateExpr) {

+        var e = (PredicateExpr)expr;

+        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) {

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

+        } else {

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

+        }

       } else if (expr is ITEExpr) {

         ITEExpr e = (ITEExpr)expr;

         Bpl.Expr total = IsTotal(e.Test, etran);

@@ -1925,6 +1935,16 @@ namespace Microsoft.Dafny {
           total = new Bpl.ForallExpr(expr.tok, bvars, Bpl.Expr.Imp(typeAntecedent, total));

         }

         return total;

+      } 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));

+        } else {

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

+        }

       } else if (expr is ITEExpr) {

         ITEExpr e = (ITEExpr)expr;

         Bpl.Expr total = CanCallAssumption(e.Test, etran);

@@ -2316,6 +2336,27 @@ namespace Microsoft.Dafny {
           builder.Add(new Bpl.IfCmd(expr.tok, etran.TrExpr(range), b.Collect(expr.tok), null, null));

         }

 

+      } else if (expr is PredicateExpr) {

+        var e = (PredicateExpr)expr;

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

+        if (e is AssertExpr) {

+          bool splitHappened;

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

+          if (!splitHappened) {

+            builder.Add(Assert(e.Guard.tok, etran.TrExpr(e.Guard), "condition in assert expression might not hold"));

+          } else {

+            foreach (var split in ss) {

+              if (!split.IsFree) {

+                builder.Add(AssertNS(split.E.tok, split.E, "condition in assert expression might not hold"));

+              }

+            }

+            builder.Add(new Bpl.AssumeCmd(e.tok, etran.TrExpr(e.Guard)));

+          }

+        } else {

+          builder.Add(new Bpl.AssumeCmd(e.tok, etran.TrExpr(e.Guard)));

+        }

+        CheckWellformed(e.Body, options, locals, builder, etran);

+

       } else if (expr is ITEExpr) {

         ITEExpr e = (ITEExpr)expr;

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

@@ -5547,6 +5588,10 @@ namespace Microsoft.Dafny {
 

           return new Bpl.LambdaExpr(expr.tok, new Bpl.TypeVariableSeq(), new VariableSeq(yVar), kv, exst);

 

+        } else if (expr is PredicateExpr) {

+          var e = (PredicateExpr)expr;

+          return TrExpr(e.Body);

+

         } else if (expr is ITEExpr) {

           ITEExpr e = (ITEExpr)expr;

           Bpl.Expr g = TrExpr(e.Test);

@@ -6349,6 +6394,10 @@ 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 UnaryExpr) {

         var e = (UnaryExpr)expr;

         if (e.Op == UnaryExpr.Opcode.Not) {

@@ -6819,6 +6868,11 @@ namespace Microsoft.Dafny {
         }

         return VarOccursInArgumentToRecursiveFunction(e.E0, n, q) ||

           VarOccursInArgumentToRecursiveFunction(e.E1, n, q);

+      } else if (expr is PredicateExpr) {

+        var e = (PredicateExpr)expr;

+        // ignore the guard

+        return VarOccursInArgumentToRecursiveFunction(e.Body, n);

+

       } else if (expr is ITEExpr) {

         var e = (ITEExpr)expr;

         return VarOccursInArgumentToRecursiveFunction(e.Test, n, subExprIsProminent) ||  // test is not "prominent"

@@ -7044,6 +7098,16 @@ namespace Microsoft.Dafny {
           Contract.Assume(false);  // unexpected ComprehensionExpr

         }

 

+      } else if (expr is PredicateExpr) {

+        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);

+        }

+

       } else if (expr is ITEExpr) {

         ITEExpr e = (ITEExpr)expr;

         Expression test = Substitute(e.Test, receiverReplacement, substMap);