Dafny: allow "assume ..." as a refining statement (provided it replaces an "assume E")

5 files changed, 133 insertions, 114 deletions

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 3000d348..4b9e0c27 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -1036,11 +1036,11 @@ CaseStatement<out MatchCaseStmt/*!*/ c>
 /*------------------------------------------------------------------------*/

 AssertStmt<out Statement/*!*/ s>

 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;

-     Expression/*!*/ e = null; Attributes attrs = null;

+     Expression e = null; Attributes attrs = null;

   .)

-  "assert"                                     (. x = t; s = null;.)

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

   { IF(IsAttribute()) Attribute<ref attrs> }

-  ( Expression<out e>                 

+  ( Expression<out e>

   | "..."

   )

   ";"

@@ -1052,9 +1052,21 @@ AssertStmt<out Statement/*!*/ s>
   .)

   .

 AssumeStmt<out Statement/*!*/ s>

-= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Expression/*!*/ e; .)

+= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;

+     Expression e = null; Attributes attrs = null;

+  .)

   "assume"                                     (. x = t; .)

-  Expression<out e> ";"                        (. s = new AssumeStmt(x, e); .)

+  { IF(IsAttribute()) Attribute<ref attrs> }

+  ( Expression<out e>

+  | "..."

+  )

+  (. if (e == null) {

+       s = new SkeletonStatement(new AssumeStmt(x, new LiteralExpr(x, true), attrs), true, false);

+     } else {

+       s = new AssumeStmt(x, e, attrs);

+     }

+  .)

+  ";"

   .

 PrintStmt<out Statement/*!*/ s>

 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Attributes.Argument/*!*/ arg;

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 1f3326da..a9e34dca 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -1559,60 +1559,40 @@ namespace Microsoft.Dafny {
 

   public abstract class PredicateStmt : Statement

   {

-    [Peer]

     public readonly Expression Expr;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Expr != null);

     }

 

-    [Captured]

     public PredicateStmt(IToken tok, Expression expr, Attributes attrs)

       : base(tok, attrs) {

       Contract.Requires(tok != null);

       Contract.Requires(expr != null);

-      Contract.Ensures(cce.Owner.Same(this, expr));

-      cce.Owner.AssignSame(this, expr);

       this.Expr = expr;

     }

 

-    [Captured]

     public PredicateStmt(IToken tok, Expression expr)

       : this(tok, expr, null) {

       Contract.Requires(tok != null);

       Contract.Requires(expr != null);

-      Contract.Ensures(cce.Owner.Same(this, expr));

-      cce.Owner.AssignSame(this, expr);

       this.Expr = expr;

     }

   }

 

   public class AssertStmt : PredicateStmt {

-    [Captured]

     public AssertStmt(IToken/*!*/ tok, Expression/*!*/ expr, Attributes attrs)

       : base(tok, expr, attrs) {

       Contract.Requires(tok != null);

       Contract.Requires(expr != null);

-      Contract.Ensures(cce.Owner.Same(this, expr));

-    }

-

-    [Captured]

-    public AssertStmt(IToken/*!*/ tok, Expression/*!*/ expr)

-      : this(tok, expr, null) {

-      Contract.Requires(tok != null);

-      Contract.Requires(expr != null);

-      Contract.Ensures(cce.Owner.Same(this, expr));

     }

   }

 

   public class AssumeStmt : PredicateStmt {

-    [Captured]

-    public AssumeStmt(IToken/*!*/ tok, Expression/*!*/ expr)

-      : base(tok, expr) {

+    public AssumeStmt(IToken/*!*/ tok, Expression/*!*/ expr, Attributes attrs)

+      : base(tok, expr, attrs) {

       Contract.Requires(tok != null);

       Contract.Requires(expr != null);

-      Contract.Ensures(cce.Owner.Same(this, expr));

-

     }

   }

 

@@ -2412,6 +2392,8 @@ namespace Microsoft.Dafny {
   ///   S == null

   /// * assert ...

   ///   ConditionOmitted == true

+  /// * assume ...

+  ///   ConditionOmitted == true

   /// * if ... { Stmt }

   ///   if ... { Stmt } else ElseStmt

   ///   ConditionOmitted == true

diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index 0c1920a6..a4e51924 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -1157,10 +1157,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

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

 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;

-		Expression/*!*/ e = null; Attributes attrs = null;

+		Expression e = null; Attributes attrs = null;

 		

 		Expect(67);

-		x = t; s = null;

+		x = t; 

 		while (IsAttribute()) {

 			Attribute(ref attrs);

 		}

@@ -1179,12 +1179,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

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

-		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Expression/*!*/ e; 

+		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;

+		Expression e = null; Attributes attrs = null;

+		

 		Expect(55);

 		x = t; 

-		Expression(out e);

+		while (IsAttribute()) {

+			Attribute(ref attrs);

+		}

+		if (StartOf(9)) {

+			Expression(out e);

+		} else if (la.kind == 30) {

+			Get();

+		} else SynErr(145);

+		if (e == null) {

+		 s = new SkeletonStatement(new AssumeStmt(x, new LiteralExpr(x, true), attrs), true, false);

+		} else {

+		 s = new AssumeStmt(x, e, attrs);

+		}

+		

 		Expect(18);

-		s = new AssumeStmt(x, e); 

 	}

 

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

@@ -1247,12 +1261,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					suchThatAssume = t; 

 				}

 				Expression(out suchThat);

-			} else SynErr(145);

+			} else SynErr(146);

 			Expect(18);

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

 			Get();

 			SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); 

-		} else SynErr(146);

+		} else SynErr(147);

 		if (suchThat != null) {

 		 s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);

 		} else {

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

 					BlockStmt(out bs, out bodyStart, out bodyEnd);

 					els = bs; 

-				} else SynErr(147);

+				} else SynErr(148);

 			}

 			if (guardOmitted) {

 			 ifStmt = new SkeletonStatement(new IfStmt(x, guard, thn, els), true, false);

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

 			AlternativeBlock(out alternatives);

 			ifStmt = new AlternativeStmt(x, alternatives); 

-		} else SynErr(148);

+		} else SynErr(149);

 	}

 

 	void WhileStmt(out Statement/*!*/ stmt) {

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

 				Get();

 				bodyOmitted = true; 

-			} else SynErr(149);

+			} else SynErr(150);

 			if (guardOmitted || bodyOmitted) {

 			 if (mod != null) {

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

@@ -1418,7 +1432,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);

 			AlternativeBlock(out alternatives);

 			stmt = new AlternativeLoopStmt(x, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), alternatives); 

-		} else SynErr(150);

+		} else SynErr(151);

 	}

 

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

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

 			Expression(out e);

 			r = new ExprRhs(e); 

-		} else SynErr(151);

+		} else SynErr(152);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

@@ -1589,7 +1603,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			while (la.kind == 44 || la.kind == 57) {

 				Suffix(ref e);

 			}

-		} else SynErr(152);

+		} else SynErr(153);

 	}

 

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

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

 			Expression(out ee);

 			e = ee; 

-		} else SynErr(153);

+		} else SynErr(154);

 		Expect(24);

 	}

 

@@ -1647,20 +1661,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		while (StartOf(16)) {

 			if (la.kind == 32 || la.kind == 65) {

 				Invariant(out invariant);

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

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

 				Expect(18);

 				invariants.Add(invariant); 

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

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

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

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref decAttrs);

 				}

 				DecreasesList(decreases, true);

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

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

 				Expect(18);

 			} else {

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

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

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref modAttrs);

@@ -1675,7 +1689,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						mod.Add(fe); 

 					}

 				}

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

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

 				Expect(18);

 			}

 		}

@@ -1683,7 +1697,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 == 32 || la.kind == 65)) {SynErr(159); Get();}

+		while (!(la.kind == 0 || la.kind == 32 || la.kind == 65)) {SynErr(160); Get();}

 		if (la.kind == 32) {

 			Get();

 			isFree = true; 

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

 			Expression(out e);

 			arg = new Attributes.Argument(t, e); 

-		} else SynErr(160);

+		} else SynErr(161);

 	}

 

 	void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {

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

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

 			Get();

-		} else SynErr(161);

+		} else SynErr(162);

 	}

 

 	void LogicalExpression(out Expression/*!*/ e0) {

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

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

 			Get();

-		} else SynErr(162);

+		} else SynErr(163);

 	}

 

 	void RelationalExpression(out Expression/*!*/ e) {

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

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

 			Get();

-		} else SynErr(163);

+		} else SynErr(164);

 	}

 

 	void OrOp() {

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

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

 			Get();

-		} else SynErr(164);

+		} else SynErr(165);

 	}

 

 	void Term(out Expression/*!*/ e0) {

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

 			break;

 		}

-		default: SynErr(165); break;

+		default: SynErr(166); break;

 		}

 	}

 

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

 			Get();

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

-		} else SynErr(166);

+		} else SynErr(167);

 	}

 

 	void UnaryExpression(out Expression/*!*/ e) {

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

 			break;

 		}

-		default: SynErr(167); break;

+		default: SynErr(168); break;

 		}

 	}

 

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

 			Get();

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

-		} else SynErr(168);

+		} else SynErr(169);

 	}

 

 	void NegOp() {

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

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

 			Get();

-		} else SynErr(169);

+		} else SynErr(170);

 	}

 

 	void EndlessExpression(out Expression e) {

@@ -2192,7 +2206,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new LetExpr(x, letVars, letRHSs, e); 

 			break;

 		}

-		default: SynErr(170); break;

+		default: SynErr(171); break;

 		}

 	}

 

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

 						

 					}

-				} else SynErr(171);

+				} else SynErr(172);

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

 				Get();

 				anyDots = true; 

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

 					e1 = ee; 

 				}

-			} else SynErr(172);

+			} else SynErr(173);

 			if (multipleIndices != null) {

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

 			 // make sure an array class with this dimensionality exists

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

 			

 			Expect(58);

-		} else SynErr(173);

+		} else SynErr(174);

 	}

 

 	void DisplayExpr(out Expression e) {

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

 			e = new SeqDisplayExpr(x, elements); 

 			Expect(58);

-		} else SynErr(174);

+		} else SynErr(175);

 	}

 

 	void MultiSetExpr(out Expression e) {

@@ -2348,7 +2362,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(24);

 		} else if (StartOf(19)) {

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

-		} else SynErr(175);

+		} else SynErr(176);

 	}

 

 	void MapExpr(out Expression e) {

@@ -2382,7 +2396,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new MapComprehension(x, bvars, range, body); 

 		} else if (StartOf(19)) {

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

-		} else SynErr(176);

+		} else SynErr(177);

 	}

 

 	void ConstAtomExpression(out Expression/*!*/ e) {

@@ -2459,7 +2473,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(24);

 			break;

 		}

-		default: SynErr(177); break;

+		default: SynErr(178); break;

 		}

 	}

 

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

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

 			Get();

-		} else SynErr(178);

+		} else SynErr(179);

 	}

 

 	void MatchExpression(out Expression/*!*/ e) {

@@ -2526,7 +2540,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 103 || la.kind == 104) {

 			Exists();

 			x = t; 

-		} else SynErr(179);

+		} else SynErr(180);

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

 		QSep();

 		Expression(out body);

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

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

 			Get();

-		} else SynErr(180);

+		} else SynErr(181);

 	}

 

 	void Exists() {

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

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

 			Get();

-		} else SynErr(181);

+		} else SynErr(182);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

@@ -2830,43 +2844,44 @@ public class Errors {
 			case 142: s = "this symbol not expected in OneStmt"; break;

 			case 143: s = "invalid OneStmt"; break;

 			case 144: s = "invalid AssertStmt"; break;

-			case 145: s = "invalid UpdateStmt"; break;

+			case 145: s = "invalid AssumeStmt"; break;

 			case 146: s = "invalid UpdateStmt"; break;

-			case 147: s = "invalid IfStmt"; break;

+			case 147: s = "invalid UpdateStmt"; break;

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

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

+			case 149: s = "invalid IfStmt"; break;

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

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

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

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

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

+			case 151: s = "invalid WhileStmt"; break;

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

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

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

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

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

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

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

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

-			case 160: s = "invalid AttributeArg"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

+			case 161: s = "invalid AttributeArg"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-			case 176: s = "invalid MapExpr"; break;

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

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

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

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

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

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

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

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

+			case 177: s = "invalid MapExpr"; break;

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

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

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

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

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

 

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

 		}

diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index 498546c3..3654c672 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -433,24 +433,14 @@ namespace Microsoft.Dafny {
         }

       }

 

-      if (stmt is AssertStmt) {

-        Expression expr = ((AssertStmt)stmt).Expr;

-

-        wr.Write("assert");

-

-        if (stmt.HasAttributes())

-        {

+      if (stmt is PredicateStmt) {

+        Expression expr = ((PredicateStmt)stmt).Expr;

+        wr.Write(stmt is AssertStmt ? "assert" : "assume");

+        if (stmt.HasAttributes()) {

           PrintAttributes(stmt.Attributes);

         }

-

         wr.Write(" ");

         PrintExpression(expr);

-

-        wr.Write(";");

-

-      } else if (stmt is AssumeStmt) {

-        wr.Write("assume ");

-        PrintExpression(((AssumeStmt)stmt).Expr);

         wr.Write(";");

 

       } else if (stmt is PrintStmt) {

@@ -635,6 +625,9 @@ namespace Microsoft.Dafny {
         } else if (s.S is AssertStmt) {

           Contract.Assert(s.ConditionOmitted);

           wr.Write("assert ...;");

+        } else if (s.S is AssumeStmt) {

+          Contract.Assert(s.ConditionOmitted);

+          wr.Write("assume ...;");

         } else if (s.S is IfStmt) {

           PrintIfStatement(indent, (IfStmt)s.S, s.ConditionOmitted);

         } else if (s.S is WhileStmt) {

diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs
index 5afe1ba7..e3b778d8 100644
--- a/Dafny/RefinementTransformer.cs
+++ b/Dafny/RefinementTransformer.cs
@@ -476,11 +476,11 @@ namespace Microsoft.Dafny {
       Statement r;

       if (stmt is AssertStmt) {

         var s = (AssertStmt)stmt;

-        r = new AssertStmt(Tok(s.Tok), CloneExpr(s.Expr));

+        r = new AssertStmt(Tok(s.Tok), CloneExpr(s.Expr), null);

 

       } else if (stmt is AssumeStmt) {

         var s = (AssumeStmt)stmt;

-        r = new AssumeStmt(Tok(s.Tok), CloneExpr(s.Expr));

+        r = new AssumeStmt(Tok(s.Tok), CloneExpr(s.Expr), null);

 

       } else if (stmt is PrintStmt) {

         var s = (PrintStmt)stmt;

@@ -864,6 +864,8 @@ namespace Microsoft.Dafny {
            *   assert ...;                 assert E;                    assert E;

            *   assert E;                                                assert E;

            *   

+           *   assume ...;                 assume E;                    assume E;

+           *   

            *   var x := E;                 var x;                       var x := E;

            *   var x := E;                 var x := *;                  var x := E;

            *   var x := E1;                var x :| E0;                 var x := E1; assert E0;

@@ -925,6 +927,19 @@ namespace Microsoft.Dafny {
                 i++; j++;

               }

 

+            } else if (S is AssumeStmt) {

+              var skel = (AssumeStmt)S;

+              Contract.Assert(((SkeletonStatement)cur).ConditionOmitted);

+              var oldAssume = oldS as AssumeStmt;

+              if (oldAssume == null) {

+                reporter.Error(cur.Tok, "assume template does not match inherited statement");

+                i++;

+              } else {

+                var e = CloneExpr(oldAssume.Expr);

+                body.Add(new AssumeStmt(skel.Tok, e, null));

+                i++; j++;

+              }

+

             } else if (S is IfStmt) {

               var skel = (IfStmt)S;

               Contract.Assert(((SkeletonStatement)cur).ConditionOmitted);

@@ -998,7 +1013,7 @@ namespace Microsoft.Dafny {
               body.Add(cNew);

               i++; j++;

               if (addedAssert != null) {

-                body.Add(new AssertStmt(addedAssert.tok, addedAssert));

+                body.Add(new AssertStmt(addedAssert.tok, addedAssert, null));

               }

             } else {

               MergeAddStatement(cur, body);

@@ -1076,6 +1091,8 @@ namespace Microsoft.Dafny {
         var S = ((SkeletonStatement)nxt).S;

         if (S is AssertStmt) {

           return other is PredicateStmt;

+        } else if (S is AssumeStmt) {

+          return other is AssumeStmt;

         } else if (S is IfStmt) {

           return other is IfStmt;

         } else if (S is WhileStmt) {