Dafny: added syntactic support for ...'s in statements, and started implementation of refinement transformations thereof

9 files changed, 402 insertions, 141 deletions

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 84db0535..3aa7f2d3 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -677,6 +677,8 @@ OneStmt<out Statement/*!*/ s>
     SYNC

     ";"                                (. s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); .)

   | ReturnStmt<out s>

+  | "..."                              (. s = new SkeletonStatement(t); .)

+    ";"

   )

   .

 ReturnStmt<out Statement/*!*/ s>

@@ -702,7 +704,7 @@ UpdateStmt<out Statement/*!*/ s>
      Attributes attrs = null;

   .)

   Lhs<out e>                       (. x = e.tok; .)

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

+  ( { Attribute<ref attrs> }

     ";"                            (. rhss.Add(new ExprRhs(e, attrs)); .)

   |                                (. lhss.Add(e);  lhs0 = e; .)

     { "," Lhs<out e>               (. lhss.Add(e); .)

@@ -750,7 +752,7 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall>
   | "*"                                (. r = new HavocRhs(t); .)

   | Expression<out e>                  (. r = new ExprRhs(e); .)

   )

-  { IF(IsAttribute()) Attribute<ref attrs> }     (. r.Attributes = attrs; .)

+  { Attribute<ref attrs> }             (. r.Attributes = attrs; .)

   .

 VarDeclStatement<.out Statement/*!*/ s.>

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

@@ -790,7 +792,7 @@ VarDeclStatement<.out Statement/*!*/ s.>
   .

 IfStmt<out Statement/*!*/ ifStmt>

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

-     Expression guard;

+     Expression guard = null;  bool guardOmitted = false;

      Statement/*!*/ thn;

      Statement/*!*/ s;

      Statement els = null;

@@ -800,14 +802,21 @@ IfStmt<out Statement/*!*/ ifStmt>
   .)

   "if"                       (. x = t; .)

   (

-    Guard<out guard>

+    ( Guard<out guard>

+    | "..."                  (. guardOmitted = true; .)

+    )

     BlockStmt<out thn, out bodyStart, out bodyEnd>

     [ "else"

       ( IfStmt<out s>                                 (. els = s; .)

       | BlockStmt<out s, out bodyStart, out bodyEnd>  (. els = s; .)

       )

     ]

-    (. ifStmt = new IfStmt(x, guard, thn, els); .)

+    (. if (guardOmitted) {

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

+       } else {

+         ifStmt = new IfStmt(x, guard, thn, els);

+       }

+    .)

   |

     AlternativeBlock<out alternatives>

     (. ifStmt = new AlternativeStmt(x, alternatives); .)

@@ -831,23 +840,43 @@ AlternativeBlock<.out List<GuardedAlternative> alternatives.>
   .

 WhileStmt<out Statement/*!*/ stmt>

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

-     Expression guard;

+     Expression guard = null;  bool guardOmitted = false;

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

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

      Attributes decAttrs = null;

      Attributes modAttrs = null;

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

-     Statement/*!*/ body;

-     IToken bodyStart, bodyEnd;

+     Statement/*!*/ body = null;  bool bodyOmitted = false;

+     IToken bodyStart = null, bodyEnd = null;

      List<GuardedAlternative> alternatives;

      stmt = dummyStmt;  // to please the compiler

   .)

   "while"                    (. x = t; .)

   (

-    Guard<out guard>           (. Contract.Assume(guard == null || cce.Owner.None(guard)); .)

+    ( Guard<out guard>           (. Contract.Assume(guard == null || cce.Owner.None(guard)); .)

+    | "..."                      (. guardOmitted = true; .)

+    )

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

-    BlockStmt<out body, out bodyStart, out bodyEnd>

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

+    ( BlockStmt<out body, out bodyStart, out bodyEnd>

+    | "..."                      (. bodyOmitted = true; .)

+    )

+    (.

+      if (guardOmitted || bodyOmitted) {

+        if (decreases.Count != 0) {

+          SemErr(decreases[0].tok, "'decreases' clauses are not allowed on refining loops");

+        }

+        if (mod != null) {

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

+        }

+        if (body == null) {

+          body = new AssertStmt(x, new LiteralExpr(x, true), null);

+        }

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

+        stmt = new SkeletonStatement(stmt, guardOmitted, bodyOmitted);

+      } else {

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

+      }

+    .)

   |

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

     AlternativeBlock<out alternatives>

@@ -863,12 +892,15 @@ LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*
   .)

   {

     Invariant<out invariant> SYNC ";"   (. invariants.Add(invariant); .)

-  | SYNC "decreases" { IF(IsAttribute()) Attribute<ref decAttrs> } DecreasesList<decreases, true> SYNC ";"

-  | SYNC "modifies" { IF(IsAttribute()) Attribute<ref modAttrs> } (. mod = mod ?? new List<FrameExpression>(); .)

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

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

-                 }

-               ] SYNC ";"

+  | SYNC "decreases"

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

+    DecreasesList<decreases, true> SYNC ";"

+  | SYNC "modifies"

+    { IF(IsAttribute()) Attribute<ref modAttrs> } (. mod = mod ?? new List<FrameExpression>(); .)

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

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

+      }

+    ] SYNC ";"

   }

   .

 Invariant<out MaybeFreeExpression/*!*/ invariant>

@@ -934,10 +966,21 @@ CaseStatement<out MatchCaseStmt/*!*/ c>
   .

 /*------------------------------------------------------------------------*/

 AssertStmt<out Statement/*!*/ s>

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

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

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

+  .)

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

-  { IF(IsAttribute()) Attribute<ref attrs> } Expression<out e> (. s = new AssertStmt(x, e, attrs); .)

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

+  ( Expression<out e>                 

+  | "..."

+  )

   ";"

+  (. if (e == null) {

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

+     } else {

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

+     }

+  .)

   .

 AssumeStmt<out Statement/*!*/ s>

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

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index c9ace165..27fbb05c 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -1915,6 +1915,40 @@ namespace Microsoft.Dafny {
     }

   }

 

+  /// <summary>

+  /// The class represents several possible scenarios:

+  /// * ...;

+  ///   S == null

+  /// * assert ...

+  ///   ConditionOmitted == true

+  /// * if ... { Stmt }

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

+  ///   ConditionOmitted == true

+  /// * while ... invariant J;

+  ///   ConditionOmitted == true && BodyOmitted == true

+  /// * while ... invariant J; { Stmt }

+  ///   ConditionOmitted == true && BodyOmitted == false

+  /// </summary>

+  public class SkeletonStatement : Statement

+  {

+    public readonly Statement S;

+    public readonly bool ConditionOmitted;

+    public readonly bool BodyOmitted;

+    public SkeletonStatement(IToken tok)

+      : base(tok)

+    {

+      Contract.Requires(tok != null);

+    }

+    public SkeletonStatement(Statement s, bool conditionOmitted, bool bodyOmitted)

+      : base(s.Tok)

+    {

+      Contract.Requires(s != null);

+      S = s;

+      ConditionOmitted = conditionOmitted;

+      BodyOmitted = bodyOmitted;

+    }

+  }

+

   // ------------------------------------------------------------------------------------------------------

 

   public abstract class TokenWrapper : IToken

diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index e74c24f6..7de10ac7 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -1091,20 +1091,37 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			ReturnStmt(out s);

 			break;

 		}

+		case 27: {

+			Get();

+			s = new SkeletonStatement(t); 

+			Expect(18);

+			break;

+		}

 		default: SynErr(139); break;

 		}

 	}

 

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

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

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

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

+		

 		Expect(63);

 		x = t; s = null;

 		while (IsAttribute()) {

 			Attribute(ref attrs);

 		}

-		Expression(out e);

-		s = new AssertStmt(x, e, attrs); 

+		if (StartOf(9)) {

+			Expression(out e);

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

+			Get();

+		} else SynErr(140);

 		Expect(18);

+		if (e == null) {

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

+		} else {

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

+		}

+		

 	}

 

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

@@ -1144,7 +1161,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Lhs(out e);

 		x = e.tok; 

 		if (la.kind == 6 || la.kind == 18) {

-			while (IsAttribute()) {

+			while (la.kind == 6) {

 				Attribute(ref attrs);

 			}

 			Expect(18);

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

 			Get();

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

-		} else SynErr(140);

+		} else SynErr(141);

 		s = new UpdateStmt(x, lhss, rhss); 

 	}

 

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

 	void IfStmt(out Statement/*!*/ ifStmt) {

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

-		Expression guard;

+		Expression guard = null;  bool guardOmitted = false;

 		Statement/*!*/ thn;

 		Statement/*!*/ s;

 		Statement els = null;

@@ -1234,8 +1251,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		Expect(56);

 		x = t; 

-		if (la.kind == 33) {

-			Guard(out guard);

+		if (la.kind == 27 || la.kind == 33) {

+			if (la.kind == 33) {

+				Guard(out guard);

+			} else {

+				Get();

+				guardOmitted = true; 

+			}

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

 			if (la.kind == 57) {

 				Get();

@@ -1245,41 +1267,71 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				} else if (la.kind == 6) {

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

 					els = s; 

-				} else SynErr(141);

+				} else SynErr(142);

+			}

+			if (guardOmitted) {

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

+			} else {

+			 ifStmt = new IfStmt(x, guard, thn, els);

 			}

-			ifStmt = new IfStmt(x, guard, thn, els); 

+			

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

 			AlternativeBlock(out alternatives);

 			ifStmt = new AlternativeStmt(x, alternatives); 

-		} else SynErr(142);

+		} else SynErr(143);

 	}

 

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

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

-		Expression guard;

+		Expression guard = null;  bool guardOmitted = false;

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

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

 		Attributes decAttrs = null;

 		Attributes modAttrs = null;

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

-		Statement/*!*/ body;

-		IToken bodyStart, bodyEnd;

+		Statement/*!*/ body = null;  bool bodyOmitted = false;

+		IToken bodyStart = null, bodyEnd = null;

 		List<GuardedAlternative> alternatives;

 		stmt = dummyStmt;  // to please the compiler

 		

 		Expect(60);

 		x = t; 

-		if (la.kind == 33) {

-			Guard(out guard);

-			Contract.Assume(guard == null || cce.Owner.None(guard)); 

+		if (la.kind == 27 || la.kind == 33) {

+			if (la.kind == 33) {

+				Guard(out guard);

+				Contract.Assume(guard == null || cce.Owner.None(guard)); 

+			} else {

+				Get();

+				guardOmitted = true; 

+			}

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

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

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

+			if (la.kind == 6) {

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

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

+				Get();

+				bodyOmitted = true; 

+			} else SynErr(144);

+			if (guardOmitted || bodyOmitted) {

+			 if (decreases.Count != 0) {

+			   SemErr(decreases[0].tok, "'decreases' clauses are not allowed on refining loops");

+			 }

+			 if (mod != null) {

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

+			 }

+			 if (body == null) {

+			   body = new AssertStmt(x, new LiteralExpr(x, true), null);

+			 }

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

+			 stmt = new SkeletonStatement(stmt, guardOmitted, bodyOmitted);

+			} else {

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

+			}

+			

 		} else if (StartOf(13)) {

 			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(143);

+		} else SynErr(145);

 	}

 

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

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

 			Expression(out e);

 			r = new ExprRhs(e); 

-		} else SynErr(144);

-		while (IsAttribute()) {

+		} else SynErr(146);

+		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

 		r.Attributes = attrs; 

@@ -1430,7 +1482,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			while (la.kind == 52 || la.kind == 54) {

 				Suffix(ref e);

 			}

-		} else SynErr(145);

+		} else SynErr(147);

 	}

 

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

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

 			Expression(out ee);

 			e = ee; 

-		} else SynErr(146);

+		} else SynErr(148);

 		Expect(34);

 	}

 

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

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

 				Invariant(out invariant);

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

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

 				Expect(18);

 				invariants.Add(invariant); 

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

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

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

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref decAttrs);

 				}

 				DecreasesList(decreases, true);

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

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

 				Expect(18);

 			} else {

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

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

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref modAttrs);

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

 					}

 				}

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

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

 				Expect(18);

 			}

 		}

@@ -1524,7 +1576,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 == 29 || la.kind == 61)) {SynErr(152); Get();}

+		while (!(la.kind == 0 || la.kind == 29 || la.kind == 61)) {SynErr(154); Get();}

 		if (la.kind == 29) {

 			Get();

 			isFree = true; 

@@ -1573,7 +1625,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(153);

+		} else SynErr(155);

 	}

 

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

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

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

 			Get();

-		} else SynErr(154);

+		} else SynErr(156);

 	}

 

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

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

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

 			Get();

-		} else SynErr(155);

+		} else SynErr(157);

 	}

 

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

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

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

 			Get();

-		} else SynErr(156);

+		} else SynErr(158);

 	}

 

 	void OrOp() {

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

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

 			Get();

-		} else SynErr(157);

+		} else SynErr(159);

 	}

 

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

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

 			break;

 		}

-		default: SynErr(158); break;

+		default: SynErr(160); break;

 		}

 	}

 

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

 			Get();

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

-		} else SynErr(159);

+		} else SynErr(161);

 	}

 

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

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

 			break;

 		}

-		default: SynErr(160); break;

+		default: SynErr(162); break;

 		}

 	}

 

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

 			Get();

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

-		} else SynErr(161);

+		} else SynErr(163);

 	}

 

 	void NegOp() {

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

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

 			Get();

-		} else SynErr(162);

+		} else SynErr(164);

 	}

 

 	void EndlessExpression(out Expression e) {

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

 			break;

 		}

-		default: SynErr(163); break;

+		default: SynErr(165); break;

 		}

 	}

 

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

 						

 					}

-				} else SynErr(164);

+				} else SynErr(166);

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

 				Get();

 				anyDots = true; 

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

 					e1 = ee; 

 				}

-			} else SynErr(165);

+			} else SynErr(167);

 			if (multipleIndices != null) {

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

 			 // make sure an array class with this dimensionality exists

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

 			

 			Expect(53);

-		} else SynErr(166);

+		} else SynErr(168);

 	}

 

 	void DisplayExpr(out Expression e) {

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

 			e = new SeqDisplayExpr(x, elements); 

 			Expect(53);

-		} else SynErr(167);

+		} else SynErr(169);

 	}

 

 	void MultiSetExpr(out Expression e) {

@@ -2185,7 +2237,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(34);

 		} else if (StartOf(19)) {

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

-		} else SynErr(168);

+		} else SynErr(170);

 	}

 

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

@@ -2262,7 +2314,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(34);

 			break;

 		}

-		default: SynErr(169); break;

+		default: SynErr(171); break;

 		}

 	}

 

@@ -2305,7 +2357,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 101 || la.kind == 102) {

 			Exists();

 			x = t; 

-		} else SynErr(170);

+		} else SynErr(172);

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

 		QSep();

 		Expression(out body);

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

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

 			Get();

-		} else SynErr(171);

+		} else SynErr(173);

 	}

 

 	void Exists() {

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

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

 			Get();

-		} else SynErr(172);

+		} else SynErr(174);

 	}

 

 	void QSep() {

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

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

 			Get();

-		} else SynErr(173);

+		} else SynErr(175);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

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

 

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

-		{T,T,T,x, x,x,T,x, x,x,x,T, T,x,x,T, x,T,T,T, x,x,x,x, T,T,x,x, T,T,T,T, T,T,x,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,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,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x},

+		{T,T,T,x, x,x,T,x, x,x,x,T, T,x,x,T, x,T,T,T, x,x,x,x, T,T,x,T, T,T,T,T, T,T,x,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,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,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, T,x,x,T, T,T,T,T, x,x,x,T, x,T,x,x, T,T,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,x,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,T, x,T,x,x, T,T,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,x,x,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,T, x,x,x,x, T,T,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

@@ -2437,9 +2489,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		{x,T,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,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,x,x,x, 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},

 		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, 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,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,T,x, x,x,x,x, T,x,x,x, x,T,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,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,T,x, x,x,x,x, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,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,T,x, x,x,x,x, x,x,x,x, x,T,x,T, 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,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},

-		{T,T,T,x, x,x,T,x, x,x,x,x, T,x,x,x, x,T,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,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},

+		{T,T,T,x, x,x,T,x, x,x,x,x, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,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,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, 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, 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,T,x, x,x,x,x, x,x,x,x, x,T,x,T, 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,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, x,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,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x},

@@ -2612,40 +2664,42 @@ public class Errors {
 			case 137: s = "invalid OneStmt"; break;

 			case 138: s = "this symbol not expected in OneStmt"; break;

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

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

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

+			case 140: s = "invalid AssertStmt"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 

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

 		}

diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index 067effcd..351df668 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -528,22 +528,7 @@ namespace Microsoft.Dafny {
 

       } else if (stmt is IfStmt) {

         IfStmt s = (IfStmt)stmt;

-        while (true) {

-          wr.Write("if (");

-          PrintGuard(s.Guard);

-          wr.Write(") ");

-          PrintStatement(s.Thn, indent);

-          if (s.Els == null) {

-            break;

-          }

-          wr.Write(" else ");

-          if (s.Els is IfStmt) {

-            s = (IfStmt)s.Els;

-          } else {

-            PrintStatement(s.Els, indent);

-            break;

-          }

-        }

+        PrintIfStatement(indent, s, false);

 

       } else if (stmt is AlternativeStmt) {

         var s = (AlternativeStmt)stmt;

@@ -554,18 +539,7 @@ namespace Microsoft.Dafny {
 

       } else if (stmt is WhileStmt) {

         WhileStmt s = (WhileStmt)stmt;

-        wr.Write("while (");

-        PrintGuard(s.Guard);

-        wr.WriteLine(")");

-

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

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

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

-        {

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

-        }

-        Indent(indent);

-        PrintStatement(s.Body, indent);

+        PrintWhileStatement(indent, s, false, false);

 

       } else if (stmt is AlternativeLoopStmt) {

         var s = (AlternativeLoopStmt)stmt;

@@ -663,11 +637,71 @@ namespace Microsoft.Dafny {
         }

         wr.Write(";");

 

+      } else if (stmt is SkeletonStatement) {

+        var s = (SkeletonStatement)stmt;

+        if (s.S == null) {

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

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

+          Contract.Assert(s.ConditionOmitted);

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

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

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

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

+          PrintWhileStatement(indent, (WhileStmt)s.S, s.ConditionOmitted, s.BodyOmitted);

+        } else {

+          Contract.Assert(false); throw new cce.UnreachableException();  // unexpected skeleton statement

+        }

+

       } else {

         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected statement

       }

     }

 

+    void PrintIfStatement(int indent, IfStmt s, bool omitGuard) {

+      while (true) {

+        if (omitGuard) {

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

+        } else {

+          wr.Write("if (");

+          PrintGuard(s.Guard);

+          wr.Write(") ");

+        }

+        PrintStatement(s.Thn, indent);

+        if (s.Els == null) {

+          break;

+        }

+        wr.Write(" else ");

+        if (s.Els is IfStmt) {

+          s = (IfStmt)s.Els;

+        } else {

+          PrintStatement(s.Els, indent);

+          break;

+        }

+      }

+    }

+

+    void PrintWhileStatement(int indent, WhileStmt s, bool omitGuard, bool omitBody) {

+      if (omitGuard) {

+        wr.WriteLine("while ...");

+      } else {

+        wr.Write("while (");

+        PrintGuard(s.Guard);

+        wr.WriteLine(")");

+      }

+

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

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

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

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

+      }

+      Indent(indent);

+      if (omitBody) {

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

+      } else {

+        PrintStatement(s.Body, indent);

+      }

+    }

+

     void PrintAlternatives(int indent, List<GuardedAlternative> alternatives) {

       int caseInd = indent + IndentAmount;

       foreach (var alternative in alternatives) {

diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs
index f46046ef..df31a834 100644
--- a/Dafny/RefinementTransformer.cs
+++ b/Dafny/RefinementTransformer.cs
@@ -748,8 +748,97 @@ namespace Microsoft.Dafny {
     BlockStmt MergeBlockStmt(BlockStmt skeleton, BlockStmt oldStmt) {

       Contract.Requires(skeleton != null);

       Contract.Requires(oldStmt != null);

-      reporter.Error(skeleton.Tok, "body of refining method is not yet supported");  // TODO (merge the new body into the old)

-      return null;

+

+      var body = new List<Statement>();

+      int i = 0, j = 0;

+      while (i < skeleton.Body.Count) {

+        var cur = skeleton.Body[i];

+        if (j == oldStmt.Body.Count) {

+          if (!(cur is SkeletonStatement)) {

+            MergeAddStatement(cur, body);

+          } else if (((SkeletonStatement)cur).S == null) {

+            // the "..." matches the empty statement sequence

+          } else {

+            reporter.Error(cur.Tok, "skeleton statement does not match old statement");

+          }

+          i++;

+        } else {

+          var oldS = oldStmt.Body[j];

+          /* See how the two statements match up.

+           *   cur                         oldS                         result

+           *   ------                      ------                       ------

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

+           *   assert ...;                 assert E;                    assert E;

+           *   assert E;                                                assert E;

+           *   

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

+           *   var VarProduction;                                       var VarProduction;

+           *   

+           *   if ... Then else Else       if (G) Then' else Else'      if (G) Merge(Then,Then') else Merge(Else,Else')

+           *   if (G) Then else Else       if (*) Then' else Else'      if (G) Merge(Then,Then') else Merge(Else,Else')

+           *

+           *   while ... LoopSpec ...      while (G) LoopSpec' Body     while (G) Merge(LoopSpec,LoopSpec') Body

+           *   while ... LoopSpec Body     while (G) LoopSpec' Body'    while (G) Merge(LoopSpec,LoopSpec') Merge(Body,Body')

+           *   while (G) LoopSpec ...      while (*) LoopSpec' Body     while (G) Merge(LoopSpec,LoopSpec') Body

+           *   while (G) LoopSpec Body     while (*) LoopSpec' Body'    while (G) Merge(LoopSpec,LoopSpec') Merge(Body,Body')

+           *   

+           *   ...; S                      StmtThatDoesNotMatchS; S'    StatementThatDoesNotMatchS; Merge( ...;S , S')

+           * 

+           * Note, LoopSpec must contain only invariant declarations (as the parser ensures for the first three cases).

+           * Note, there is an implicit "...;" at the end of every block in a skeleton.

+           *   

+           * TODO:  should also handle labels and some form of new "replace" statement

+           */

+          if (cur is SkeletonStatement) {

+            var ass = ((SkeletonStatement)cur).S as AssertStmt;

+            if (ass != null) {

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

+              var oldAssume = oldS as PredicateStmt;

+              if (oldAssume == null) {

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

+              } else {

+                body.Add(new AssertStmt(ass.Tok, CloneExpr(oldAssume.Expr)));

+              }

+              i++; j++;

+            } else {

+              reporter.Error(cur.Tok, "sorry, this skeleton statement is not yet supported");

+              i++;

+            }

+          } else {

+            var cNew = cur as VarDeclStmt;

+            var cOld = oldS as VarDeclStmt;

+            if (cNew != null && cOld != null && cNew.Lhss.Count == 1 && cOld.Lhss.Count == 1 &&

+              cNew.Lhss[0].Name == cOld.Lhss[0].Name && cOld.Update == null) {

+              body.Add(cNew);  // TODO:  there should perhaps be some more validity checks here first

+              i++; j++;

+            } else {

+              MergeAddStatement(cur, body);

+              i++;

+            }

+          }

+        }

+      }

+      // implement the implicit "...;" at the end of each block statement skeleton

+      for (; j < oldStmt.Body.Count; j++) {

+        MergeAddStatement(CloneStmt(oldStmt.Body[j]), body);

+      }

+      return new BlockStmt(skeleton.Tok, body);

+    }

+

+    /// <summary>

+    /// Add "s" to "stmtList", but complain if "s" contains further occurrences of "..." or if "s" assigns to a

+    /// variable that was not declared in the refining module.

+    /// TODO: and what about new control flow?

+    /// </summary>

+    void MergeAddStatement(Statement s, List<Statement> stmtList) {

+      Contract.Requires(s != null);

+      Contract.Requires(stmtList != null);

+      if (s is AssertStmt) {

+        // this is fine to add

+      } else {

+        // TODO: validity checks

+      }

+      stmtList.Add(s);

     }

 

     // ---------------------- additional methods -----------------------------------------------------------------------------

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index fa2a48e8..f66a2c5c 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -1709,6 +1709,13 @@ namespace Microsoft.Dafny {
         }

 

 

+      } else if (stmt is SkeletonStatement) {

+        var s = (SkeletonStatement)stmt;

+        Error(s.Tok, "skeleton statements are allowed only in refining methods");

+        // nevertheless, resolve the underlying statement; hey, why not

+        if (s.S != null) {

+          ResolveStatement(s.S, specContextOnly, method);

+        }

       } else {

         Contract.Assert(false); throw new cce.UnreachableException();

       }

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 58cc29fc..8cb67403 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1360,7 +1360,7 @@ Refinement.dfy(74,15): Related location: This is the postcondition that might no
 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 28 verified, 6 errors

+Dafny program verifier finished with 44 verified, 6 errors

 

 -------------------- RefinementErrors.dfy --------------------

 RefinementErrors.dfy(27,17): Error: a refining method is not allowed to add preconditions

@@ -1373,9 +1373,8 @@ RefinementErrors.dfy(35,11): Error: type parameters are not allowed to be rename
 RefinementErrors.dfy(35,13): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'C', found 'B')

 RefinementErrors.dfy(36,23): Error: the type of parameter 'z' is different from the type of the same parameter in the corresponding function in the module it refines ('seq<C>' instead of 'set<C>')

 RefinementErrors.dfy(37,9): Error: there is a difference in name of parameter 3 ('k' versus 'b') of function F compared to corresponding function in the module it refines

-RefinementErrors.dfy(47,4): Error: body of refining method is not yet supported

 RefinementErrors.dfy(54,20): Error: a function can be changed into a function method in a refining module only if the function has not yet been given a body: G

-12 resolution/type errors detected in RefinementErrors.dfy

+11 resolution/type errors detected in RefinementErrors.dfy

 

 -------------------- ReturnErrors.dfy --------------------

 ReturnErrors.dfy(30,10): Error: cannot have method call in return statement.

diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy
index fc531e23..c24ed555 100644
--- a/Test/dafny0/Refinement.dfy
+++ b/Test/dafny0/Refinement.dfy
@@ -96,10 +96,10 @@ module FullBodied refines BodyFree {
 }
 
 // ------------------------------------------------
-/*  SOON
+
 module Abstract {
   class MyNumber {
-    var N: int;
+    ghost var N: int;
     ghost var Repr: set<object>;
     predicate Valid
       reads this, Repr;
@@ -125,7 +125,8 @@ module Abstract {
       requires Valid;
       ensures n == N;
     {
-      n := N;
+      var k;  assume k == N;
+      n := k;
     }
   }
 }
@@ -148,7 +149,8 @@ module Concrete refines Abstract {
     }
     method Get() returns (n: int)
     {
-      n := a - b;
+      var k := a - b;
+      assert ...;
     }
   }
 }
@@ -164,4 +166,3 @@ module Client imports Concrete {
     }
   }
 }
-*/
diff --git a/Test/dafny0/RefinementErrors.dfy b/Test/dafny0/RefinementErrors.dfy
index 25ba94ad..df6f1a71 100644
--- a/Test/dafny0/RefinementErrors.dfy
+++ b/Test/dafny0/RefinementErrors.dfy
@@ -44,7 +44,7 @@ module B refines A {
     {  // yes, can give it a body
     }
     method FullBodied(x: int) returns (y: bool, k: seq<set<object>>)
-    {  // error: not allowed to change body (not yet implemented)
+    {
     }
   }
 }