Dafny: Start of new refinement features -- clean out old ones

13 files changed, 794 insertions, 1332 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 97492776..ca779bf1 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -487,9 +487,6 @@ namespace Microsoft.Dafny {
             }

           }

 

-        } else if (member is CouplingInvariant) {

-          Error("coupling invariants are not supported in compilation");

-

         } else {

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

         }

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 34dde196..ddb8d15e 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -195,8 +195,6 @@ ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c>
      IToken/*!*/ id;

      Attributes attrs = null;

      List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();

-     IToken/*!*/ idRefined;

-     IToken optionalId = null;

      List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();

      IToken bodyStart;

   .)

@@ -205,16 +203,11 @@ ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c>
   { Attribute<ref attrs> }

   Ident<out id>

   [ GenericParameters<typeArgs> ]

-  [ "refines" Ident<out idRefined>               (. optionalId = idRefined; .)

-  ]

   "{"                                            (. bodyStart = t; .)

   { ClassMemberDecl<members, true>

   }

   "}"

-  (. if (optionalId == null)

-       c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);

-     else

-       c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);

+  (. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);

      c.BodyStartTok = bodyStart;

      c.BodyEndTok = t;

   .)

@@ -232,7 +225,6 @@ ClassMemberDecl<.List<MemberDecl/*!*/>/*!*/ mm, bool allowConstructors.>
   ( FieldDecl<mmod, mm>

   | FunctionDecl<mmod, out f>                   (. mm.Add(f); .)

   | MethodDecl<mmod, allowConstructors, out m>  (. mm.Add(m); .)

-  | CouplingInvDecl<mmod, mm>

   )

   .

 DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt>

@@ -294,27 +286,6 @@ ArbitraryTypeDecl<ModuleDecl/*!*/ module, out ArbitraryTypeDecl at>
   Ident<out id>               (. at = new ArbitraryTypeDecl(id, id.val, module, attrs); .)

   SYNC ";"

   .

-CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>

-= (. Contract.Requires(cce.NonNullElements(mm));

-     Attributes attrs = null;

-     List<IToken/*!*/> ids = new List<IToken/*!*/>();;

-     IToken/*!*/ id;

-     Expression/*!*/ e;

-  .)

-  "replaces"

-  (. if (mmod.IsUnlimited) { SemErr(t, "coupling invariants cannot be declared 'unlimited'"); }

-     if (mmod.IsStatic) { SemErr(t, "coupling invariants cannot be declared 'static'"); }

-     if (mmod.IsGhost) { SemErr(t, "coupling invariants cannot be declared 'ghost'"); }

-  .)

-  { Attribute<ref attrs> }

-  Ident<out id>                                     (. ids.Add(id); .)

-  { "," Ident<out id>                               (. ids.Add(id); .)

-  }

-  "by"

-  Expression<out e>

-  ";"

-  (. mm.Add(new CouplingInvariant(ids, e, attrs)); .)

-  .

 GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost>

 /* isGhost always returns as false if allowGhostKeyword is false */

 = (. Contract.Ensures(Contract.ValueAtReturn(out id)!=null);

@@ -398,7 +369,6 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
      Attributes modAttrs = null;

      Statement/*!*/ bb;  BlockStmt body = null;

      bool isConstructor = false;

-     bool isRefinement = false;

      IToken bodyStart = Token.NoToken;

      IToken bodyEnd = Token.NoToken;

   .)

@@ -410,7 +380,6 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
                                          SemErr(t, "constructors are only allowed in classes");

                                        }

                                     .)

-  | "refines"                       (. isRefinement = true; .)

   )

   (. if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }

      if (isConstructor) {

@@ -432,9 +401,7 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
   { MethodSpec<req, mod, ens, dec, ref decAttrs, ref modAttrs> }

   [ BlockStmt<out bb, out bodyStart, out bodyEnd>    (. body = (BlockStmt)bb; .)

   ]

-  (. if (isRefinement)

-       m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs);

-     else if (isConstructor)

+  (. if (isConstructor)

        m = new Constructor(id, id.val, typeArgs, ins, req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs);

      else

        m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs);

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index be062fba..86342409 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -689,27 +689,6 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public class ClassRefinementDecl : ClassDecl {

-    public readonly IToken/*!*/ RefinedClass;

-    public ClassDecl Refined; // filled in during resolution

-    [ContractInvariantMethod]

-    void ObjectInvariant() {

-      Contract.Invariant(RefinedClass != null);

-    }

-

-    public ClassRefinementDecl(IToken tok, string name, ModuleDecl module, List<TypeParameter/*!*/>/*!*/ typeArgs,

-      [Captured] List<MemberDecl/*!*/>/*!*/ members, Attributes attributes, IToken/*!*/ refinedClass)

-      : base(tok, name, module, typeArgs, members, attributes) {

-      Contract.Requires(tok != null);

-      Contract.Requires(name != null);

-      Contract.Requires(module != null);

-      Contract.Requires(cce.NonNullElements(typeArgs));

-      Contract.Requires(cce.NonNullElements(members));

-      Contract.Requires(refinedClass != null);

-      RefinedClass = refinedClass;

-    }

-  }

-

   public class DefaultClassDecl : ClassDecl {

     public DefaultClassDecl(DefaultModuleDecl/*!*/ module, [Captured] List<MemberDecl/*!*/>/*!*/ members)

       : base(Token.NoToken, "_default", module, new List<TypeParameter/*!*/>(), members, null) {

@@ -875,48 +854,6 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public class CouplingInvariant : MemberDecl {

-    public readonly Expression Expr;

-    public readonly List<IToken/*!*/>/*!*/ Toks;

-    public List<Formal/*!*/> Formals; // filled in during resolution

-    public List<Field/*!*/> Refined; // filled in during resolution

-

-    [ContractInvariantMethod]

-    void ObjectInvariant() {

-      Contract.Invariant(Expr != null);

-      Contract.Invariant(cce.NonNullElements(Toks));

-      Contract.Invariant(Formals == null || cce.NonNullElements(Formals));

-      Contract.Invariant(Refined == null || cce.NonNullElements(Refined));

-    }

-

-

-    public CouplingInvariant(List<IToken/*!*/>/*!*/ toks, Expression/*!*/ expr, Attributes attributes)

-      : base(toks[0], "_coupling_invariant" + getNames(toks), false, attributes) {

-      Contract.Requires(toks.Count > 0);

-      Expr = expr;

-      Toks = toks;

-    }

-

-    private static string getNames(List<IToken> toks) {

-      Contract.Requires(toks != null);

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

-

-      StringBuilder sb = new StringBuilder();

-      foreach (IToken tok in toks) {

-        Contract.Assert(tok != null);

-        sb.Append("_").Append(tok.val);

-      }

-      return sb.ToString();

-    }

-

-    public string[] Tokens() {

-      string[] result = new string[Toks.Count];

-      for (int i = 0; i < Toks.Count; i++)

-        result[i] = Toks[i].val;

-      return result;

-    }

-  }

-

   public class ArbitraryTypeDecl : TopLevelDecl, TypeParameter.ParentType

   {

     public readonly TypeParameter TheType;

@@ -1219,31 +1156,6 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public class MethodRefinement : Method

-  {

-    public Method Refined; // filled in during resolution

-    public MethodRefinement(IToken/*!*/ tok, string/*!*/ name,

-                  bool isStatic, bool isGhost,

-                  [Captured] List<TypeParameter/*!*/>/*!*/ typeArgs,

-                  [Captured] List<Formal/*!*/>/*!*/ ins, [Captured] List<Formal/*!*/>/*!*/ outs,

-                  [Captured] List<MaybeFreeExpression/*!*/>/*!*/ req, [Captured] Specification<FrameExpression>/*!*/ mod,

-                  [Captured] List<MaybeFreeExpression/*!*/>/*!*/ ens,

-                  [Captured] Specification<Expression>/*!*/ decreases,

-                  [Captured] BlockStmt body,

-                  Attributes attributes)

-      : base(tok, name, isStatic, isGhost, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes) {

-      Contract.Requires(tok != null);

-      Contract.Requires(name != null);

-      Contract.Requires(cce.NonNullElements(typeArgs));

-      Contract.Requires(cce.NonNullElements(ins));

-      Contract.Requires(cce.NonNullElements(outs));

-      Contract.Requires(cce.NonNullElements(req));

-      Contract.Requires(mod != null);

-      Contract.Requires(cce.NonNullElements(ens));

-      Contract.Requires(decreases != null);

-    }

-  }

-

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

 

   public abstract class Statement {

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 52f86e5f..f344aa76 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -21,12 +21,12 @@ public class Parser {
 	public const int _colon = 5;

 	public const int _lbrace = 6;

 	public const int _rbrace = 7;

-	public const int maxT = 105;

+	public const int maxT = 102;

 

 	const bool T = true;

 	const bool x = false;

 	const int minErrDist = 2;

-

+	

 	public Scanner/*!*/ scanner;

 	public Errors/*!*/  errors;

 

@@ -141,10 +141,10 @@ bool IsAttribute() {
 		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);

 	}

 

@@ -157,15 +157,15 @@ bool IsAttribute() {
 			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 {

@@ -189,7 +189,7 @@ bool IsAttribute() {
 		}

 	}

 

-

+	

 	void Dafny() {

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

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

@@ -198,13 +198,13 @@ bool IsAttribute() {
 		// to support multiple files, create a default module only if theModules doesn't already contain one

 		DefaultModuleDecl defaultModule = null;

 		foreach (ModuleDecl mdecl in theModules) {

-		 defaultModule = mdecl as DefaultModuleDecl;

-		 if (defaultModule != null) { break; }

+		  defaultModule = mdecl as DefaultModuleDecl;

+		  if (defaultModule != null) { break; }

 		}

 		bool defaultModuleCreatedHere = false;

 		if (defaultModule == null) {

-		 defaultModuleCreatedHere = true;

-		 defaultModule = new DefaultModuleDecl();

+		  defaultModuleCreatedHere = true;

+		  defaultModule = new DefaultModuleDecl();

 		}

 		

 		while (StartOf(1)) {

@@ -222,11 +222,11 @@ bool IsAttribute() {
 				module = new ModuleDecl(id, id.val, theImports, attrs); 

 				Expect(6);

 				module.BodyStartTok = t; 

-				while (la.kind == 10 || la.kind == 15 || la.kind == 21) {

+				while (la.kind == 10 || la.kind == 14 || la.kind == 20) {

 					if (la.kind == 10) {

 						ClassDecl(module, out c);

 						module.TopLevelDecls.Add(c); 

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

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

 						DatatypeDecl(module, out dt);

 						module.TopLevelDecls.Add(dt); 

 					} else {

@@ -240,10 +240,10 @@ bool IsAttribute() {
 			} else if (la.kind == 10) {

 				ClassDecl(defaultModule, out c);

 				defaultModule.TopLevelDecls.Add(c); 

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

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

 				DatatypeDecl(defaultModule, out dt);

 				defaultModule.TopLevelDecls.Add(dt); 

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

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

 				ArbitraryTypeDecl(defaultModule, out at);

 				defaultModule.TopLevelDecls.Add(at); 

 			} else {

@@ -254,14 +254,14 @@ bool IsAttribute() {
 		 defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass));

 		 theModules.Add(defaultModule);

 		} else {

-		 // find the default class in the default module, then append membersDefaultClass to its member list

-		 foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {

-		   DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl;

-		   if (defaultClass != null) {

-		     defaultClass.Members.AddRange(membersDefaultClass);

-		     break;

-		   }

-		 }

+		  // find the default class in the default module, then append membersDefaultClass to its member list

+		  foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {

+		    DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl;

+		    if (defaultClass != null) {

+		      defaultClass.Members.AddRange(membersDefaultClass);

+		      break;

+		    }

+		  }

 		}

 		

 		Expect(0);

@@ -283,7 +283,7 @@ bool IsAttribute() {
 		IToken/*!*/ id; 

 		Ident(out id);

 		ids.Add(id.val); 

-		while (la.kind == 20) {

+		while (la.kind == 19) {

 			Get();

 			Ident(out id);

 			ids.Add(id.val); 

@@ -296,35 +296,25 @@ bool IsAttribute() {
 		IToken/*!*/ id;

 		Attributes attrs = null;

 		List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();

-		IToken/*!*/ idRefined;

-		IToken optionalId = null;

 		List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();

 		IToken bodyStart;

 		

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

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

 		Expect(10);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (la.kind == 24) {

+		if (la.kind == 21) {

 			GenericParameters(typeArgs);

 		}

-		if (la.kind == 11) {

-			Get();

-			Ident(out idRefined);

-			optionalId = idRefined; 

-		}

 		Expect(6);

 		bodyStart = t; 

 		while (StartOf(2)) {

 			ClassMemberDecl(members, true);

 		}

 		Expect(7);

-		if (optionalId == null)

-		 c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);

-		else

-		 c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);

+		c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);

 		c.BodyStartTok = bodyStart;

 		c.BodyEndTok = t;

 		

@@ -339,24 +329,24 @@ bool IsAttribute() {
 		List<DatatypeCtor/*!*/> ctors = new List<DatatypeCtor/*!*/>();

 		IToken bodyStart = Token.NoToken;  // dummy assignment

 		

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

-		Expect(15);

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

+		Expect(14);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (la.kind == 24) {

+		if (la.kind == 21) {

 			GenericParameters(typeArgs);

 		}

-		Expect(16);

+		Expect(15);

 		bodyStart = t; 

 		DatatypeMemberDecl(ctors);

-		while (la.kind == 17) {

+		while (la.kind == 16) {

 			Get();

 			DatatypeMemberDecl(ctors);

 		}

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

-		Expect(18);

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

+		Expect(17);

 		dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);

 		dt.BodyStartTok = bodyStart;

 		dt.BodyEndTok = t;

@@ -367,14 +357,14 @@ bool IsAttribute() {
 		IToken/*!*/ id;

 		Attributes attrs = null;

 		

-		Expect(21);

+		Expect(20);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

 		Ident(out id);

 		at = new ArbitraryTypeDecl(id, id.val, module, attrs); 

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

-		Expect(18);

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

+		Expect(17);

 	}

 

 	void ClassMemberDecl(List<MemberDecl/*!*/>/*!*/ mm, bool allowConstructors) {

@@ -383,11 +373,11 @@ bool IsAttribute() {
 		Function/*!*/ f;

 		MemberModifiers mmod = new MemberModifiers();

 		

-		while (la.kind == 12 || la.kind == 13 || la.kind == 14) {

-			if (la.kind == 12) {

+		while (la.kind == 11 || la.kind == 12 || la.kind == 13) {

+			if (la.kind == 11) {

 				Get();

 				mmod.IsGhost = true; 

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

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

 				Get();

 				mmod.IsStatic = true; 

 			} else {

@@ -395,31 +385,29 @@ bool IsAttribute() {
 				mmod.IsUnlimited = true; 

 			}

 		}

-		if (la.kind == 19) {

+		if (la.kind == 18) {

 			FieldDecl(mmod, mm);

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

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

 			FunctionDecl(mmod, out f);

 			mm.Add(f); 

-		} else if (la.kind == 11 || la.kind == 26 || la.kind == 27) {

+		} else if (la.kind == 23 || la.kind == 24) {

 			MethodDecl(mmod, allowConstructors, out m);

 			mm.Add(m); 

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

-			CouplingInvDecl(mmod, mm);

-		} else SynErr(110);

+		} else SynErr(107);

 	}

 

 	void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {

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

 		IToken/*!*/ id; 

-		Expect(24);

+		Expect(21);

 		Ident(out id);

 		typeArgs.Add(new TypeParameter(id, id.val)); 

-		while (la.kind == 20) {

+		while (la.kind == 19) {

 			Get();

 			Ident(out id);

 			typeArgs.Add(new TypeParameter(id, id.val)); 

 		}

-		Expect(25);

+		Expect(22);

 	}

 

 	void FieldDecl(MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm) {

@@ -427,8 +415,8 @@ bool IsAttribute() {
 		Attributes attrs = null;

 		IToken/*!*/ id;  Type/*!*/ ty;

 		

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

-		Expect(19);

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

+		Expect(18);

 		if (mmod.IsUnlimited) { SemErr(t, "fields cannot be declared 'unlimited'"); }

 		if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }

 		

@@ -437,13 +425,13 @@ bool IsAttribute() {
 		}

 		IdentType(out id, out ty);

 		mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); 

-		while (la.kind == 20) {

+		while (la.kind == 19) {

 			Get();

 			IdentType(out id, out ty);

 			mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); 

 		}

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

-		Expect(18);

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

+		Expect(17);

 	}

 

 	void FunctionDecl(MemberModifiers mmod, out Function/*!*/ f) {

@@ -462,8 +450,8 @@ bool IsAttribute() {
 		IToken bodyStart = Token.NoToken;

 		IToken bodyEnd = Token.NoToken;

 		

-		Expect(43);

-		if (la.kind == 26) {

+		Expect(40);

+		if (la.kind == 23) {

 			Get();

 			isFunctionMethod = true; 

 		}

@@ -473,7 +461,7 @@ bool IsAttribute() {
 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (la.kind == 24) {

+		if (la.kind == 21) {

 			GenericParameters(typeArgs);

 		}

 		Formals(true, isFunctionMethod, formals);

@@ -507,94 +495,60 @@ bool IsAttribute() {
 		Attributes modAttrs = null;

 		Statement/*!*/ bb;  BlockStmt body = null;

 		bool isConstructor = false;

-		bool isRefinement = false;

 		IToken bodyStart = Token.NoToken;

 		IToken bodyEnd = Token.NoToken;

 		

-		while (!(StartOf(4))) {SynErr(113); Get();}

-		if (la.kind == 26) {

+		while (!(la.kind == 0 || la.kind == 23 || la.kind == 24)) {SynErr(110); Get();}

+		if (la.kind == 23) {

 			Get();

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

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

 			Get();

 			if (allowConstructor) {

 			 isConstructor = true;

 			} else {

-			 SemErr(t, "constructors are only allowed in classes");

+			  SemErr(t, "constructors are only allowed in classes");

 			}

 			

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

-			Get();

-			isRefinement = true; 

-		} else SynErr(114);

+		} else SynErr(111);

 		if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }

 		if (isConstructor) {

-		 if (mmod.IsGhost) {

-		   SemErr(t, "constructors cannot be declared 'ghost'");

-		 }

-		 if (mmod.IsStatic) {

-		   SemErr(t, "constructors cannot be declared 'static'");

-		 }

+		  if (mmod.IsGhost) {

+		    SemErr(t, "constructors cannot be declared 'ghost'");

+		  }

+		  if (mmod.IsStatic) {

+		    SemErr(t, "constructors cannot be declared 'static'");

+		  }

 		}

 		

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (la.kind == 24) {

+		if (la.kind == 21) {

 			GenericParameters(typeArgs);

 		}

 		Formals(true, !mmod.IsGhost, ins);

-		if (la.kind == 28) {

+		if (la.kind == 25) {

 			Get();

 			if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } 

 			Formals(false, !mmod.IsGhost, outs);

 		}

-		while (StartOf(5)) {

+		while (StartOf(4)) {

 			MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs);

 		}

 		if (la.kind == 6) {

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

 			body = (BlockStmt)bb; 

 		}

-		if (isRefinement)

-		 m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs);

-		else if (isConstructor)

+		if (isConstructor)

 		 m = new Constructor(id, id.val, typeArgs, ins, req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs);

 		else

-		 m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs);

+		  m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs);

 		m.BodyStartTok = bodyStart;

 		m.BodyEndTok = bodyEnd;

 		

 	}

 

-	void CouplingInvDecl(MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm) {

-		Contract.Requires(cce.NonNullElements(mm));

-		Attributes attrs = null;

-		List<IToken/*!*/> ids = new List<IToken/*!*/>();;

-		IToken/*!*/ id;

-		Expression/*!*/ e;

-		

-		Expect(22);

-		if (mmod.IsUnlimited) { SemErr(t, "coupling invariants cannot be declared 'unlimited'"); }

-		if (mmod.IsStatic) { SemErr(t, "coupling invariants cannot be declared 'static'"); }

-		if (mmod.IsGhost) { SemErr(t, "coupling invariants cannot be declared 'ghost'"); }

-		

-		while (la.kind == 6) {

-			Attribute(ref attrs);

-		}

-		Ident(out id);

-		ids.Add(id); 

-		while (la.kind == 20) {

-			Get();

-			Ident(out id);

-			ids.Add(id); 

-		}

-		Expect(23);

-		Expression(out e);

-		Expect(18);

-		mm.Add(new CouplingInvariant(ids, e, attrs)); 

-	}

-

 	void DatatypeMemberDecl(List<DatatypeCtor/*!*/>/*!*/ ctors) {

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

 		Attributes attrs = null;

@@ -605,7 +559,7 @@ bool IsAttribute() {
 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (la.kind == 34) {

+		if (la.kind == 31) {

 			FormalsOptionalIds(formals);

 		}

 		ctors.Add(new DatatypeCtor(id, id.val, formals, attrs)); 

@@ -613,17 +567,17 @@ bool IsAttribute() {
 

 	void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {

 		Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  string/*!*/ name;  bool isGhost; 

-		Expect(34);

-		if (StartOf(6)) {

+		Expect(31);

+		if (StartOf(5)) {

 			TypeIdentOptional(out id, out name, out ty, out isGhost);

 			formals.Add(new Formal(id, name, ty, true, isGhost)); 

-			while (la.kind == 20) {

+			while (la.kind == 19) {

 				Get();

 				TypeIdentOptional(out id, out name, out ty, out isGhost);

 				formals.Add(new Formal(id, name, ty, true, isGhost)); 

 			}

 		}

-		Expect(35);

+		Expect(32);

 	}

 

 	void IdentType(out IToken/*!*/ id, out Type/*!*/ ty) {

@@ -633,15 +587,11 @@ bool IsAttribute() {
 		Type(out ty);

 	}

 

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

-		EquivExpression(out e);

-	}

-

 	void GIdentType(bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost) {

 		Contract.Ensures(Contract.ValueAtReturn(out id)!=null);

 		Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);

 		isGhost = false; 

-		if (la.kind == 12) {

+		if (la.kind == 11) {

 			Get();

 			if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } 

 		}

@@ -682,7 +632,7 @@ bool IsAttribute() {
 		Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);

 		Contract.Ensures(Contract.ValueAtReturn(out identName)!=null);

 		string name = null;  isGhost = false; 

-		if (la.kind == 12) {

+		if (la.kind == 11) {

 			Get();

 			isGhost = true; 

 		}

@@ -691,9 +641,9 @@ bool IsAttribute() {
 			Get();

 			UserDefinedType udt = ty as UserDefinedType;

 			if (udt != null && udt.TypeArgs.Count == 0) {

-			 name = udt.Name;

+			  name = udt.Name;

 			} else {

-			 SemErr(id, "invalid formal-parameter name in datatype constructor");

+			  SemErr(id, "invalid formal-parameter name in datatype constructor");

 			}

 			

 			Type(out ty);

@@ -701,7 +651,7 @@ bool IsAttribute() {
 		if (name != null) {

 		 identName = name;

 		} else {

-		 identName = "#" + anonymousIds++;

+		  identName = "#" + anonymousIds++;

 		}

 		

 	}

@@ -711,22 +661,22 @@ bool IsAttribute() {
 		List<Type/*!*/>/*!*/ gt;

 		

 		switch (la.kind) {

-		case 36: {

+		case 33: {

 			Get();

 			tok = t; 

 			break;

 		}

-		case 37: {

+		case 34: {

 			Get();

 			tok = t;  ty = new NatType(); 

 			break;

 		}

-		case 38: {

+		case 35: {

 			Get();

 			tok = t;  ty = new IntType(); 

 			break;

 		}

-		case 39: {

+		case 36: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

 			GenericInstantiation(gt);

@@ -737,7 +687,7 @@ bool IsAttribute() {
 			

 			break;

 		}

-		case 40: {

+		case 37: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

 			GenericInstantiation(gt);

@@ -748,7 +698,7 @@ bool IsAttribute() {
 			

 			break;

 		}

-		case 41: {

+		case 38: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

 			GenericInstantiation(gt);

@@ -759,27 +709,27 @@ bool IsAttribute() {
 			

 			break;

 		}

-		case 1: case 3: case 42: {

+		case 1: case 3: case 39: {

 			ReferenceType(out tok, out ty);

 			break;

 		}

-		default: SynErr(115); break;

+		default: SynErr(112); break;

 		}

 	}

 

 	void Formals(bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals) {

 		Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  bool isGhost; 

-		Expect(34);

-		if (la.kind == 1 || la.kind == 12) {

+		Expect(31);

+		if (la.kind == 1 || la.kind == 11) {

 			GIdentType(allowGhostKeyword, out id, out ty, out isGhost);

 			formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); 

-			while (la.kind == 20) {

+			while (la.kind == 19) {

 				Get();

 				GIdentType(allowGhostKeyword, out id, out ty, out isGhost);

 				formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); 

 			}

 		}

-		Expect(35);

+		Expect(32);

 	}

 

 	void MethodSpec(List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/*!*/ mod, List<MaybeFreeExpression/*!*/>/*!*/ ens,

@@ -787,53 +737,53 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));

 		Expression/*!*/ e;  FrameExpression/*!*/ fe;  bool isFree = false; Attributes ensAttrs = null;

 		

-		while (!(StartOf(7))) {SynErr(116); Get();}

-		if (la.kind == 29) {

+		while (!(StartOf(6))) {SynErr(113); Get();}

+		if (la.kind == 26) {

 			Get();

 			while (IsAttribute()) {

 				Attribute(ref modAttrs);

 			}

-			if (StartOf(8)) {

+			if (StartOf(7)) {

 				FrameExpression(out fe);

 				mod.Add(fe); 

-				while (la.kind == 20) {

+				while (la.kind == 19) {

 					Get();

 					FrameExpression(out fe);

 					mod.Add(fe); 

 				}

 			}

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

-			Expect(18);

-		} else if (la.kind == 30 || la.kind == 31 || la.kind == 32) {

-			if (la.kind == 30) {

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

+			Expect(17);

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

+			if (la.kind == 27) {

 				Get();

 				isFree = true; 

 			}

-			if (la.kind == 31) {

+			if (la.kind == 28) {

 				Get();

 				Expression(out e);

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

-				Expect(18);

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

+				Expect(17);

 				req.Add(new MaybeFreeExpression(e, isFree)); 

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

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

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref ensAttrs);

 				}

 				Expression(out e);

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

-				Expect(18);

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

+				Expect(17);

 				ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); 

-			} else SynErr(120);

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

+			} else SynErr(117);

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

 			Get();

 			while (IsAttribute()) {

 				Attribute(ref decAttrs);

 			}

 			DecreasesList(decreases, false);

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

-			Expect(18);

-		} else SynErr(122);

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

+			Expect(17);

+		} else SynErr(119);

 	}

 

 	void BlockStmt(out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {

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

 		Expect(6);

 		bodyStart = t; 

-		while (StartOf(9)) {

+		while (StartOf(8)) {

 			Stmt(body);

 		}

 		Expect(7);

@@ -853,7 +803,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void FrameExpression(out FrameExpression/*!*/ fe) {

 		Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e;  IToken/*!*/ id;  string fieldName = null; 

 		Expression(out e);

-		if (la.kind == 46) {

+		if (la.kind == 43) {

 			Get();

 			Ident(out id);

 			fieldName = id.val; 

@@ -861,22 +811,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		fe = new FrameExpression(e, fieldName); 

 	}

 

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

+		EquivExpression(out e);

+	}

+

 	void DecreasesList(List<Expression/*!*/> decreases, bool allowWildcard) {

 		Expression/*!*/ e; 

 		PossiblyWildExpression(out e);

 		if (!allowWildcard && e is WildcardExpr) {

 		 SemErr(e.tok, "'decreases *' is only allowed on loops");

 		} else {

-		 decreases.Add(e);

+		  decreases.Add(e);

 		}

 		

-		while (la.kind == 20) {

+		while (la.kind == 19) {

 			Get();

 			PossiblyWildExpression(out e);

 			if (!allowWildcard && e is WildcardExpr) {

 			 SemErr(e.tok, "'decreases *' is only allowed on loops");

 			} else {

-			 decreases.Add(e);

+			  decreases.Add(e);

 			}

 			

 		}

@@ -884,15 +838,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void GenericInstantiation(List<Type/*!*/>/*!*/ gt) {

 		Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; 

-		Expect(24);

+		Expect(21);

 		Type(out ty);

 		gt.Add(ty); 

-		while (la.kind == 20) {

+		while (la.kind == 19) {

 			Get();

 			Type(out ty);

 			gt.Add(ty); 

 		}

-		Expect(25);

+		Expect(22);

 	}

 

 	void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) {

@@ -900,7 +854,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

 		List<Type/*!*/>/*!*/ gt;

 		

-		if (la.kind == 42) {

+		if (la.kind == 39) {

 			Get();

 			tok = t;  ty = new ObjectType(); 

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

@@ -912,55 +866,55 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			int dims = 1;

 			if (tok.val.Length != 5) {

-			 dims = int.Parse(tok.val.Substring(5));

+			  dims = int.Parse(tok.val.Substring(5));

 			}

 			ty = theBuiltIns.ArrayType(tok, dims, gt[0], true);

 			

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

 			Ident(out tok);

 			gt = new List<Type/*!*/>(); 

-			if (la.kind == 24) {

+			if (la.kind == 21) {

 				GenericInstantiation(gt);

 			}

 			ty = new UserDefinedType(tok, tok.val, gt); 

-		} else SynErr(123);

+		} else SynErr(120);

 	}

 

 	void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases) {

 		Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases));

 		Expression/*!*/ e;  FrameExpression/*!*/ fe; 

-		if (la.kind == 31) {

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

+		if (la.kind == 28) {

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

 			Get();

 			Expression(out e);

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

-			Expect(18);

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

+			Expect(17);

 			reqs.Add(e); 

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

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

 			Get();

-			if (StartOf(10)) {

+			if (StartOf(9)) {

 				PossiblyWildFrameExpression(out fe);

 				reads.Add(fe); 

-				while (la.kind == 20) {

+				while (la.kind == 19) {

 					Get();

 					PossiblyWildFrameExpression(out fe);

 					reads.Add(fe); 

 				}

 			}

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

-			Expect(18);

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

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

+			Expect(17);

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

 			Get();

 			Expression(out e);

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

-			Expect(18);

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

+			Expect(17);

 			ens.Add(e); 

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

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

 			Get();

 			DecreasesList(decreases, false);

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

-			Expect(18);

-		} else SynErr(129);

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

+			Expect(17);

+		} else SynErr(126);

 	}

 

 	void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {

@@ -974,23 +928,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) {

 		Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; 

-		if (la.kind == 45) {

+		if (la.kind == 42) {

 			Get();

 			fe = new FrameExpression(new WildcardExpr(t), null); 

-		} else if (StartOf(8)) {

+		} else if (StartOf(7)) {

 			FrameExpression(out fe);

-		} else SynErr(130);

+		} else SynErr(127);

 	}

 

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

 		Contract.Ensures(Contract.ValueAtReturn(out e)!=null);

 		e = dummyExpr; 

-		if (la.kind == 45) {

+		if (la.kind == 42) {

 			Get();

 			e = new WildcardExpr(t); 

-		} else if (StartOf(8)) {

+		} else if (StartOf(7)) {

 			Expression(out e);

-		} else SynErr(131);

+		} else SynErr(128);

 	}

 

 	void Stmt(List<Statement/*!*/>/*!*/ ss) {

@@ -1006,49 +960,49 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken bodyStart, bodyEnd;

 		int breakCount;

 		

-		while (!(StartOf(11))) {SynErr(132); Get();}

+		while (!(StartOf(10))) {SynErr(129); Get();}

 		switch (la.kind) {

 		case 6: {

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

 			break;

 		}

-		case 63: {

+		case 60: {

 			AssertStmt(out s);

 			break;

 		}

-		case 64: {

+		case 61: {

 			AssumeStmt(out s);

 			break;

 		}

-		case 65: {

+		case 62: {

 			PrintStmt(out s);

 			break;

 		}

-		case 1: case 2: case 17: case 34: case 90: case 91: case 92: case 93: case 94: case 95: case 96: {

+		case 1: case 2: case 16: case 31: case 87: case 88: case 89: case 90: case 91: case 92: case 93: {

 			UpdateStmt(out s);

 			break;

 		}

-		case 12: case 19: {

+		case 11: case 18: {

 			VarDeclStatement(out s);

 			break;

 		}

-		case 56: {

+		case 53: {

 			IfStmt(out s);

 			break;

 		}

-		case 60: {

+		case 57: {

 			WhileStmt(out s);

 			break;

 		}

-		case 62: {

+		case 59: {

 			MatchStmt(out s);

 			break;

 		}

-		case 66: {

+		case 63: {

 			ParallelStmt(out s);

 			break;

 		}

-		case 47: {

+		case 44: {

 			Get();

 			x = t; 

 			Ident(out id);

@@ -1057,49 +1011,49 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			s.Labels = new LabelNode(x, id.val, s.Labels); 

 			break;

 		}

-		case 48: {

+		case 45: {

 			Get();

 			x = t; breakCount = 1; label = null; 

 			if (la.kind == 1) {

 				Ident(out id);

 				label = id.val; 

-			} else if (la.kind == 18 || la.kind == 48) {

-				while (la.kind == 48) {

+			} else if (la.kind == 17 || la.kind == 45) {

+				while (la.kind == 45) {

 					Get();

 					breakCount++; 

 				}

-			} else SynErr(133);

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

-			Expect(18);

+			} else SynErr(130);

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

+			Expect(17);

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

 			break;

 		}

-		case 49: {

+		case 46: {

 			ReturnStmt(out s);

 			break;

 		}

-		default: SynErr(135); break;

+		default: SynErr(132); break;

 		}

 	}

 

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

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

-		Expect(63);

+		Expect(60);

 		x = t; s = null;

 		while (IsAttribute()) {

 			Attribute(ref attrs);

 		}

 		Expression(out e);

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

-		Expect(18);

+		Expect(17);

 	}

 

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

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

-		Expect(64);

+		Expect(61);

 		x = t; 

 		Expression(out e);

-		Expect(18);

+		Expect(17);

 		s = new AssumeStmt(x, e); 

 	}

 

@@ -1107,16 +1061,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Attributes.Argument/*!*/ arg;

 		List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();

 		

-		Expect(65);

+		Expect(62);

 		x = t; 

 		AttributeArg(out arg);

 		args.Add(arg); 

-		while (la.kind == 20) {

+		while (la.kind == 19) {

 			Get();

 			AttributeArg(out arg);

 			args.Add(arg); 

 		}

-		Expect(18);

+		Expect(17);

 		s = new PrintStmt(x, args); 

 	}

 

@@ -1130,33 +1084,33 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		Lhs(out e);

 		x = e.tok; 

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

+		if (la.kind == 6 || la.kind == 17) {

 			while (IsAttribute()) {

 				Attribute(ref attrs);

 			}

-			Expect(18);

+			Expect(17);

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

-		} else if (la.kind == 20 || la.kind == 50) {

+		} else if (la.kind == 19 || la.kind == 47) {

 			lhss.Add(e);  lhs0 = e; 

-			while (la.kind == 20) {

+			while (la.kind == 19) {

 				Get();

 				Lhs(out e);

 				lhss.Add(e); 

 			}

-			Expect(50);

+			Expect(47);

 			x = t; 

 			Rhs(out r, lhs0);

 			rhss.Add(r); 

-			while (la.kind == 20) {

+			while (la.kind == 19) {

 				Get();

 				Rhs(out r, lhs0);

 				rhss.Add(r); 

 			}

-			Expect(18);

+			Expect(17);

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

 			Get();

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

-		} else SynErr(136);

+		} else SynErr(133);

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

 	}

 

@@ -1167,20 +1121,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<VarDecl> lhss = new List<VarDecl>();

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

 		

-		if (la.kind == 12) {

+		if (la.kind == 11) {

 			Get();

 			isGhost = true;  x = t; 

 		}

-		Expect(19);

+		Expect(18);

 		if (!isGhost) { x = t; } 

 		LocalIdentTypeOptional(out d, isGhost);

 		lhss.Add(d); 

-		while (la.kind == 20) {

+		while (la.kind == 19) {

 			Get();

 			LocalIdentTypeOptional(out d, isGhost);

 			lhss.Add(d); 

 		}

-		if (la.kind == 50) {

+		if (la.kind == 47) {

 			Get();

 			assignTok = t;

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

@@ -1188,22 +1142,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			

 			Rhs(out r, lhs0);

 			rhss.Add(r); 

-			while (la.kind == 20) {

+			while (la.kind == 19) {

 				Get();

 				Rhs(out r, lhs0);

 				rhss.Add(r); 

 			}

 		}

-		Expect(18);

+		Expect(17);

 		UpdateStmt update;

 		if (rhss.Count == 0) {

-		 update = null;

+		  update = null;

 		} else {

-		 var ies = new List<Expression>();

-		 foreach (var lhs in lhss) {

-		   ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));

-		 }

-		 update = new UpdateStmt(assignTok, ies, rhss);

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

+		  foreach (var lhs in lhss) {

+		    ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));

+		  }

+		  update = new UpdateStmt(assignTok, ies, rhss);

 		}

 		s = new VarDeclStmt(x, lhss, update);

 		

@@ -1219,26 +1173,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<GuardedAlternative> alternatives;

 		ifStmt = dummyStmt;  // to please the compiler

 		

-		Expect(56);

+		Expect(53);

 		x = t; 

-		if (la.kind == 34) {

+		if (la.kind == 31) {

 			Guard(out guard);

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

-			if (la.kind == 57) {

+			if (la.kind == 54) {

 				Get();

-				if (la.kind == 56) {

+				if (la.kind == 53) {

 					IfStmt(out s);

 					els = s; 

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

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

 					els = s; 

-				} else SynErr(137);

+				} else SynErr(134);

 			}

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

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

 			AlternativeBlock(out alternatives);

 			ifStmt = new AlternativeStmt(x, alternatives); 

-		} else SynErr(138);

+		} else SynErr(135);

 	}

 

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

@@ -1254,30 +1208,30 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<GuardedAlternative> alternatives;

 		stmt = dummyStmt;  // to please the compiler

 		

-		Expect(60);

+		Expect(57);

 		x = t; 

-		if (la.kind == 34) {

+		if (la.kind == 31) {

 			Guard(out guard);

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

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

-		} else if (StartOf(12)) {

+		} else if (StartOf(11)) {

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

+		} else SynErr(136);

 	}

 

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

 		Contract.Ensures(Contract.ValueAtReturn(out s) != null);

 		Token x;  Expression/*!*/ e;  MatchCaseStmt/*!*/ c;

 		List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>(); 

-		Expect(62);

+		Expect(59);

 		x = t; 

 		Expression(out e);

 		Expect(6);

-		while (la.kind == 58) {

+		while (la.kind == 55) {

 			CaseStatement(out c);

 			cases.Add(c); 

 		}

@@ -1297,21 +1251,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Statement/*!*/ block;

 		IToken bodyStart, bodyEnd;

 		

-		Expect(66);

+		Expect(63);

 		x = t; 

-		Expect(34);

+		Expect(31);

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

 		if (range == null) { range = new LiteralExpr(x, true); } 

-		Expect(35);

-		while (la.kind == 30 || la.kind == 32) {

+		Expect(32);

+		while (la.kind == 27 || la.kind == 29) {

 			isFree = false; 

-			if (la.kind == 30) {

+			if (la.kind == 27) {

 				Get();

 				isFree = true; 

 			}

-			Expect(32);

+			Expect(29);

 			Expression(out e);

-			Expect(18);

+			Expect(17);

 			ens.Add(new MaybeFreeExpression(e, isFree)); 

 		}

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

@@ -1323,18 +1277,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<AssignmentRhs> rhss = null;

 		AssignmentRhs r;

 		

-		Expect(49);

+		Expect(46);

 		returnTok = t; 

-		if (StartOf(13)) {

+		if (StartOf(12)) {

 			Rhs(out r, null);

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

-			while (la.kind == 20) {

+			while (la.kind == 19) {

 				Get();

 				Rhs(out r, null);

 				rhss.Add(r); 

 			}

 		}

-		Expect(18);

+		Expect(17);

 		s = new ReturnStmt(returnTok, rhss); 

 	}

 

@@ -1347,27 +1301,27 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		r = null;  // to please compiler

 		Attributes attrs = null;

 		

-		if (la.kind == 51) {

+		if (la.kind == 48) {

 			Get();

 			newToken = t; 

 			TypeAndToken(out x, out ty);

-			if (la.kind == 52 || la.kind == 54) {

-				if (la.kind == 52) {

+			if (la.kind == 49 || la.kind == 51) {

+				if (la.kind == 49) {

 					Get();

 					ee = new List<Expression>(); 

 					Expressions(ee);

-					Expect(53);

+					Expect(50);

 					UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);

 					

 				} else {

 					Get();

 					Ident(out x);

-					Expect(34);

+					Expect(31);

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

-					if (StartOf(8)) {

+					if (StartOf(7)) {

 						Expressions(args);

 					}

-					Expect(35);

+					Expect(32);

 					initCall = new CallStmt(x, new List<Expression>(),

 					                       receiverForInitCall, x.val, args); 

 				}

@@ -1375,21 +1329,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			if (ee != null) {

 			 r = new TypeRhs(newToken, ty, ee);

 			} else {

-			 r = new TypeRhs(newToken, ty, initCall);

+			  r = new TypeRhs(newToken, ty, initCall);

 			}

 			

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

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

 			Get();

 			x = t; 

 			Expression(out e);

 			r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e)); 

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

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

 			Get();

 			r = new HavocRhs(t); 

-		} else if (StartOf(8)) {

+		} else if (StartOf(7)) {

 			Expression(out e);

 			r = new ExprRhs(e); 

-		} else SynErr(140);

+		} else SynErr(137);

 		while (IsAttribute()) {

 			Attribute(ref attrs);

 		}

@@ -1401,23 +1355,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		if (la.kind == 1) {

 			DottedIdentifiersAndFunction(out e);

-			while (la.kind == 52 || la.kind == 54) {

+			while (la.kind == 49 || la.kind == 51) {

 				Suffix(ref e);

 			}

-		} else if (StartOf(14)) {

+		} else if (StartOf(13)) {

 			ConstAtomExpression(out e);

 			Suffix(ref e);

-			while (la.kind == 52 || la.kind == 54) {

+			while (la.kind == 49 || la.kind == 51) {

 				Suffix(ref e);

 			}

-		} else SynErr(141);

+		} else SynErr(138);

 	}

 

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

 		Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e; 

 		Expression(out e);

 		args.Add(e); 

-		while (la.kind == 20) {

+		while (la.kind == 19) {

 			Get();

 			Expression(out e);

 			args.Add(e); 

@@ -1426,15 +1380,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void Guard(out Expression e) {

 		Expression/*!*/ ee;  e = null; 

-		Expect(34);

-		if (la.kind == 45) {

+		Expect(31);

+		if (la.kind == 42) {

 			Get();

 			e = null; 

-		} else if (StartOf(8)) {

+		} else if (StartOf(7)) {

 			Expression(out ee);

 			e = ee; 

-		} else SynErr(142);

-		Expect(35);

+		} else SynErr(139);

+		Expect(32);

 	}

 

 	void AlternativeBlock(out List<GuardedAlternative> alternatives) {

@@ -1444,13 +1398,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<Statement> body;

 		

 		Expect(6);

-		while (la.kind == 58) {

+		while (la.kind == 55) {

 			Get();

 			x = t; 

 			Expression(out e);

-			Expect(59);

+			Expect(56);

 			body = new List<Statement>(); 

-			while (StartOf(9)) {

+			while (StartOf(8)) {

 				Stmt(body);

 			}

 			alternatives.Add(new GuardedAlternative(x, e, body)); 

@@ -1465,51 +1419,51 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		decreases = new List<Expression/*!*/>();

 		mod = null;

 		

-		while (StartOf(15)) {

-			if (la.kind == 30 || la.kind == 61) {

+		while (StartOf(14)) {

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

 				Invariant(out invariant);

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

-				Expect(18);

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

+				Expect(17);

 				invariants.Add(invariant); 

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

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

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

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

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref decAttrs);

 				}

 				DecreasesList(decreases, true);

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

-				Expect(18);

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

+				Expect(17);

 			} else {

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

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

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref modAttrs);

 				}

 				mod = mod ?? new List<FrameExpression>(); 

-				if (StartOf(8)) {

+				if (StartOf(7)) {

 					FrameExpression(out fe);

 					mod.Add(fe); 

-					while (la.kind == 20) {

+					while (la.kind == 19) {

 						Get();

 						FrameExpression(out fe);

 						mod.Add(fe); 

 					}

 				}

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

-				Expect(18);

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

+				Expect(17);

 			}

 		}

 	}

 

 	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 == 30 || la.kind == 61)) {SynErr(148); Get();}

-		if (la.kind == 30) {

+		while (!(la.kind == 0 || la.kind == 27 || la.kind == 58)) {SynErr(145); Get();}

+		if (la.kind == 27) {

 			Get();

 			isFree = true; 

 		}

-		Expect(61);

+		Expect(58);

 		while (IsAttribute()) {

 			Attribute(ref attrs);

 		}

@@ -1524,22 +1478,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BoundVar/*!*/ bv;

 		List<Statement/*!*/> body = new List<Statement/*!*/>();

 		

-		Expect(58);

+		Expect(55);

 		x = t; 

 		Ident(out id);

-		if (la.kind == 34) {

+		if (la.kind == 31) {

 			Get();

 			IdentTypeOptional(out bv);

 			arguments.Add(bv); 

-			while (la.kind == 20) {

+			while (la.kind == 19) {

 				Get();

 				IdentTypeOptional(out bv);

 				arguments.Add(bv); 

 			}

-			Expect(35);

+			Expect(32);

 		}

-		Expect(59);

-		while (StartOf(9)) {

+		Expect(56);

+		while (StartOf(8)) {

 			Stmt(body);

 		}

 		c = new MatchCaseStmt(x, id.val, arguments, body); 

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

 			Get();

 			arg = new Attributes.Argument(t, t.val.Substring(1, t.val.Length-2)); 

-		} else if (StartOf(8)) {

+		} else if (StartOf(7)) {

 			Expression(out e);

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

-		} else SynErr(149);

+		} else SynErr(146);

 	}

 

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

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

 		IdentTypeOptional(out bv);

 		bvars.Add(bv); 

-		while (la.kind == 20) {

+		while (la.kind == 19) {

 			Get();

 			IdentTypeOptional(out bv);

 			bvars.Add(bv); 

@@ -1572,7 +1526,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

-		if (la.kind == 17) {

+		if (la.kind == 16) {

 			Get();

 			Expression(out range);

 		}

@@ -1581,7 +1535,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void EquivExpression(out Expression/*!*/ e0) {

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

 		ImpliesExpression(out e0);

-		while (la.kind == 67 || la.kind == 68) {

+		while (la.kind == 64 || la.kind == 65) {

 			EquivOp();

 			x = t; 

 			ImpliesExpression(out e1);

@@ -1592,7 +1546,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void ImpliesExpression(out Expression/*!*/ e0) {

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

 		LogicalExpression(out e0);

-		if (la.kind == 69 || la.kind == 70) {

+		if (la.kind == 66 || la.kind == 67) {

 			ImpliesOp();

 			x = t; 

 			ImpliesExpression(out e1);

@@ -1601,23 +1555,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void EquivOp() {

-		if (la.kind == 67) {

+		if (la.kind == 64) {

 			Get();

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

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

 			Get();

-		} else SynErr(150);

+		} else SynErr(147);

 	}

 

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

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

 		RelationalExpression(out e0);

-		if (StartOf(16)) {

-			if (la.kind == 71 || la.kind == 72) {

+		if (StartOf(15)) {

+			if (la.kind == 68 || la.kind == 69) {

 				AndOp();

 				x = t; 

 				RelationalExpression(out e1);

 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); 

-				while (la.kind == 71 || la.kind == 72) {

+				while (la.kind == 68 || la.kind == 69) {

 					AndOp();

 					x = t; 

 					RelationalExpression(out e1);

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

 				RelationalExpression(out e1);

 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); 

-				while (la.kind == 73 || la.kind == 74) {

+				while (la.kind == 70 || la.kind == 71) {

 					OrOp();

 					x = t; 

 					RelationalExpression(out e1);

@@ -1639,11 +1593,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void ImpliesOp() {

-		if (la.kind == 69) {

+		if (la.kind == 66) {

 			Get();

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

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

 			Get();

-		} else SynErr(151);

+		} else SynErr(148);

 	}

 

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

@@ -1652,23 +1606,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<Expression> chain = null;

 		List<BinaryExpr.Opcode> ops = null;

 		int kind = 0;  // 0 ("uncommitted") indicates chain of ==, possibly with one !=

-		              // 1 ("ascending")   indicates chain of ==, <, <=, possibly with one !=

-		              // 2 ("descending")  indicates chain of ==, >, >=, possibly with one !=

-		              // 3 ("illegal")     indicates illegal chain

-		              // 4 ("disjoint")    indicates chain of disjoint set operators

+		               // 1 ("ascending")   indicates chain of ==, <, <=, possibly with one !=

+		               // 2 ("descending")  indicates chain of ==, >, >=, possibly with one !=

+		               // 3 ("illegal")     indicates illegal chain

+		               // 4 ("disjoint")    indicates chain of disjoint set operators

 		bool hasSeenNeq = false;

 		

 		Term(out e0);

 		e = e0; 

-		if (StartOf(17)) {

+		if (StartOf(16)) {

 			RelOp(out x, out op);

 			firstOpTok = x; 

 			Term(out e1);

 			e = new BinaryExpr(x, op, e0, e1);

 			if (op == BinaryExpr.Opcode.Disjoint)

-			 acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.

+			  acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.

 			

-			while (StartOf(17)) {

+			while (StartOf(16)) {

 				if (chain == null) {

 				 chain = new List<Expression>();

 				 ops = new List<BinaryExpr.Opcode>();

@@ -1722,11 +1676,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				Term(out e1);

 				ops.Add(op); chain.Add(e1);

 				if (op == BinaryExpr.Opcode.Disjoint) {

-				 e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1));

-				 acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.

+				  e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1));

+				  acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.

 				}

 				else

-				 e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));

+				  e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));

 				

 			}

 		}

@@ -1737,25 +1691,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void AndOp() {

-		if (la.kind == 71) {

+		if (la.kind == 68) {

 			Get();

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

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

 			Get();

-		} else SynErr(152);

+		} else SynErr(149);

 	}

 

 	void OrOp() {

-		if (la.kind == 73) {

+		if (la.kind == 70) {

 			Get();

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

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

 			Get();

-		} else SynErr(153);

+		} else SynErr(150);

 	}

 

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

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; 

 		Factor(out e0);

-		while (la.kind == 85 || la.kind == 86) {

+		while (la.kind == 82 || la.kind == 83) {

 			AddOp(out x, out op);

 			Factor(out e1);

 			e0 = new BinaryExpr(x, op, e0, e1); 

@@ -1768,87 +1722,87 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken y;

 		

 		switch (la.kind) {

-		case 75: {

+		case 72: {

 			Get();

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

 			break;

 		}

-		case 24: {

+		case 21: {

 			Get();

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

 			break;

 		}

-		case 25: {

+		case 22: {

 			Get();

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

 			break;

 		}

-		case 76: {

+		case 73: {

 			Get();

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

 			break;

 		}

-		case 77: {

+		case 74: {

 			Get();

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

 			break;

 		}

-		case 78: {

+		case 75: {

 			Get();

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

 			break;

 		}

-		case 79: {

+		case 76: {

 			Get();

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

 			break;

 		}

-		case 80: {

+		case 77: {

 			Get();

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

 			break;

 		}

-		case 81: {

+		case 78: {

 			Get();

 			x = t;  y = Token.NoToken; 

-			if (la.kind == 80) {

+			if (la.kind == 77) {

 				Get();

 				y = t; 

 			}

 			if (y == Token.NoToken) {

 			 SemErr(x, "invalid RelOp");

 			} else if (y.pos != x.pos + 1) {

-			 SemErr(x, "invalid RelOp (perhaps you intended \"!in\" with no intervening whitespace?)");

+			  SemErr(x, "invalid RelOp (perhaps you intended \"!in\" with no intervening whitespace?)");

 			} else {

-			 x.val = "!in";

-			 op = BinaryExpr.Opcode.NotIn;

+			  x.val = "!in";

+			  op = BinaryExpr.Opcode.NotIn;

 			}

 			

 			break;

 		}

-		case 82: {

+		case 79: {

 			Get();

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

 			break;

 		}

-		case 83: {

+		case 80: {

 			Get();

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

 			break;

 		}

-		case 84: {

+		case 81: {

 			Get();

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

 			break;

 		}

-		default: SynErr(154); break;

+		default: SynErr(151); break;

 		}

 	}

 

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

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; 

 		UnaryExpression(out e0);

-		while (la.kind == 45 || la.kind == 87 || la.kind == 88) {

+		while (la.kind == 42 || la.kind == 84 || la.kind == 85) {

 			MulOp(out x, out op);

 			UnaryExpression(out e1);

 			e0 = new BinaryExpr(x, op, e0, e1); 

@@ -1857,82 +1811,82 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void AddOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {

 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op=BinaryExpr.Opcode.Add/*(dummy)*/; 

-		if (la.kind == 85) {

+		if (la.kind == 82) {

 			Get();

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

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

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

 			Get();

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

-		} else SynErr(155);

+		} else SynErr(152);

 	}

 

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

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

 		switch (la.kind) {

-		case 86: {

+		case 83: {

 			Get();

 			x = t; 

 			UnaryExpression(out e);

 			e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); 

 			break;

 		}

-		case 81: case 89: {

+		case 78: case 86: {

 			NegOp();

 			x = t; 

 			UnaryExpression(out e);

 			e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); 

 			break;

 		}

-		case 19: case 39: case 56: case 62: case 63: case 64: case 99: case 100: case 101: case 102: {

+		case 18: case 36: case 53: case 59: case 60: case 61: case 96: case 97: case 98: case 99: {

 			EndlessExpression(out e);

 			break;

 		}

 		case 1: {

 			DottedIdentifiersAndFunction(out e);

-			while (la.kind == 52 || la.kind == 54) {

+			while (la.kind == 49 || la.kind == 51) {

 				Suffix(ref e);

 			}

 			break;

 		}

-		case 6: case 52: {

+		case 6: case 49: {

 			DisplayExpr(out e);

 			break;

 		}

-		case 40: {

+		case 37: {

 			MultiSetExpr(out e);

 			break;

 		}

-		case 2: case 17: case 34: case 90: case 91: case 92: case 93: case 94: case 95: case 96: {

+		case 2: case 16: case 31: case 87: case 88: case 89: case 90: case 91: case 92: case 93: {

 			ConstAtomExpression(out e);

-			while (la.kind == 52 || la.kind == 54) {

+			while (la.kind == 49 || la.kind == 51) {

 				Suffix(ref e);

 			}

 			break;

 		}

-		default: SynErr(156); break;

+		default: SynErr(153); break;

 		}

 	}

 

 	void MulOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {

 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op = BinaryExpr.Opcode.Add/*(dummy)*/; 

-		if (la.kind == 45) {

+		if (la.kind == 42) {

 			Get();

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

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

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

 			Get();

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

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

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

 			Get();

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

-		} else SynErr(157);

+		} else SynErr(154);

 	}

 

 	void NegOp() {

-		if (la.kind == 81) {

+		if (la.kind == 78) {

 			Get();

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

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

 			Get();

-		} else SynErr(158);

+		} else SynErr(155);

 	}

 

 	void EndlessExpression(out Expression e) {

@@ -1943,73 +1897,73 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<BoundVar> letVars;  List<Expression> letRHSs;

 		

 		switch (la.kind) {

-		case 56: {

+		case 53: {

 			Get();

 			x = t; 

 			Expression(out e);

-			Expect(97);

+			Expect(94);

 			Expression(out e0);

-			Expect(57);

+			Expect(54);

 			Expression(out e1);

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

 			break;

 		}

-		case 62: {

+		case 59: {

 			MatchExpression(out e);

 			break;

 		}

-		case 99: case 100: case 101: case 102: {

+		case 96: case 97: case 98: case 99: {

 			QuantifierGuts(out e);

 			break;

 		}

-		case 39: {

+		case 36: {

 			ComprehensionExpr(out e);

 			break;

 		}

-		case 63: {

+		case 60: {

 			Get();

 			x = t; 

 			Expression(out e0);

-			Expect(18);

+			Expect(17);

 			Expression(out e1);

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

 			break;

 		}

-		case 64: {

+		case 61: {

 			Get();

 			x = t; 

 			Expression(out e0);

-			Expect(18);

+			Expect(17);

 			Expression(out e1);

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

 			break;

 		}

-		case 19: {

+		case 18: {

 			Get();

 			x = t;

 			letVars = new List<BoundVar>();

 			letRHSs = new List<Expression>(); 

 			IdentTypeOptional(out d);

 			letVars.Add(d); 

-			while (la.kind == 20) {

+			while (la.kind == 19) {

 				Get();

 				IdentTypeOptional(out d);

 				letVars.Add(d); 

 			}

-			Expect(50);

+			Expect(47);

 			Expression(out e);

 			letRHSs.Add(e); 

-			while (la.kind == 20) {

+			while (la.kind == 19) {

 				Get();

 				Expression(out e);

 				letRHSs.Add(e); 

 			}

-			Expect(18);

+			Expect(17);

 			Expression(out e);

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

 			break;

 		}

-		default: SynErr(159); break;

+		default: SynErr(156); break;

 		}

 	}

 

@@ -2020,18 +1974,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		Ident(out id);

 		idents.Add(id); 

-		while (la.kind == 54) {

+		while (la.kind == 51) {

 			Get();

 			Ident(out id);

 			idents.Add(id); 

 		}

-		if (la.kind == 34) {

+		if (la.kind == 31) {

 			Get();

 			openParen = t;  args = new List<Expression>(); 

-			if (StartOf(8)) {

+			if (StartOf(7)) {

 				Expressions(args);

 			}

-			Expect(35);

+			Expect(32);

 		}

 		e = new IdentifierSequence(idents, openParen, args); 

 	}

@@ -2042,38 +1996,38 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<Expression> multipleIndices = null;

 		bool func = false;

 		

-		if (la.kind == 54) {

+		if (la.kind == 51) {

 			Get();

 			Ident(out id);

-			if (la.kind == 34) {

+			if (la.kind == 31) {

 				Get();

 				args = new List<Expression/*!*/>();  func = true; 

-				if (StartOf(8)) {

+				if (StartOf(7)) {

 					Expressions(args);

 				}

-				Expect(35);

+				Expect(32);

 				e = new FunctionCallExpr(id, id.val, e, args); 

 			}

 			if (!func) { e = new FieldSelectExpr(id, e, id.val); } 

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

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

 			Get();

 			x = t; 

-			if (StartOf(8)) {

+			if (StartOf(7)) {

 				Expression(out ee);

 				e0 = ee; 

-				if (la.kind == 98) {

+				if (la.kind == 95) {

 					Get();

 					anyDots = true; 

-					if (StartOf(8)) {

+					if (StartOf(7)) {

 						Expression(out ee);

 						e1 = ee; 

 					}

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

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

 					Get();

 					Expression(out ee);

 					e1 = ee; 

-				} else if (la.kind == 20 || la.kind == 53) {

-					while (la.kind == 20) {

+				} else if (la.kind == 19 || la.kind == 50) {

+					while (la.kind == 19) {

 						Get();

 						Expression(out ee);

 						if (multipleIndices == null) {

@@ -2083,39 +2037,39 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						multipleIndices.Add(ee);

 						

 					}

-				} else SynErr(160);

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

+				} else SynErr(157);

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

 				Get();

 				anyDots = true; 

-				if (StartOf(8)) {

+				if (StartOf(7)) {

 					Expression(out ee);

 					e1 = ee; 

 				}

-			} else SynErr(161);

+			} else SynErr(158);

 			if (multipleIndices != null) {

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

 			 // make sure an array class with this dimensionality exists

 			 UserDefinedType tmp = theBuiltIns.ArrayType(x, multipleIndices.Count, new IntType(), true);

 			} else {

-			 if (!anyDots && e0 == null) {

-			   /* a parsing error occurred */

-			   e0 = dummyExpr;

-			 }

-			 Contract.Assert(anyDots || e0 != null);

-			 if (anyDots) {

-			   //Contract.Assert(e0 != null || e1 != null);

-			   e = new SeqSelectExpr(x, false, e, e0, e1);

-			 } else if (e1 == null) {

-			   Contract.Assert(e0 != null);

-			   e = new SeqSelectExpr(x, true, e, e0, null);

-			 } else {

-			   Contract.Assert(e0 != null);

-			   e = new SeqUpdateExpr(x, e, e0, e1);

-			 }

+			  if (!anyDots && e0 == null) {

+			    /* a parsing error occurred */

+			    e0 = dummyExpr;

+			  }

+			  Contract.Assert(anyDots || e0 != null);

+			  if (anyDots) {

+			    //Contract.Assert(e0 != null || e1 != null);

+			    e = new SeqSelectExpr(x, false, e, e0, e1);

+			  } else if (e1 == null) {

+			    Contract.Assert(e0 != null);

+			    e = new SeqSelectExpr(x, true, e, e0, null);

+			  } else {

+			    Contract.Assert(e0 != null);

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

+			  }

 			}

 			

-			Expect(53);

-		} else SynErr(162);

+			Expect(50);

+		} else SynErr(159);

 	}

 

 	void DisplayExpr(out Expression e) {

@@ -2126,20 +2080,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		if (la.kind == 6) {

 			Get();

 			x = t;  elements = new List<Expression/*!*/>(); 

-			if (StartOf(8)) {

+			if (StartOf(7)) {

 				Expressions(elements);

 			}

 			e = new SetDisplayExpr(x, elements);

 			Expect(7);

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

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

 			Get();

 			x = t;  elements = new List<Expression/*!*/>(); 

-			if (StartOf(8)) {

+			if (StartOf(7)) {

 				Expressions(elements);

 			}

 			e = new SeqDisplayExpr(x, elements); 

-			Expect(53);

-		} else SynErr(163);

+			Expect(50);

+		} else SynErr(160);

 	}

 

 	void MultiSetExpr(out Expression e) {

@@ -2147,25 +2101,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken/*!*/ x = null;  List<Expression/*!*/>/*!*/ elements;

 		e = dummyExpr;

 		

-		Expect(40);

+		Expect(37);

 		x = t; 

 		if (la.kind == 6) {

 			Get();

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

-			if (StartOf(8)) {

+			if (StartOf(7)) {

 				Expressions(elements);

 			}

 			e = new MultiSetDisplayExpr(x, elements);

 			Expect(7);

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

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

 			Get();

 			x = t;  elements = new List<Expression/*!*/>(); 

 			Expression(out e);

 			e = new MultiSetFormingExpr(x, e); 

-			Expect(35);

-		} else if (StartOf(18)) {

+			Expect(32);

+		} else if (StartOf(17)) {

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

-		} else SynErr(164);

+		} else SynErr(161);

 	}

 

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

@@ -2174,17 +2128,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		e = dummyExpr;

 		

 		switch (la.kind) {

-		case 90: {

+		case 87: {

 			Get();

 			e = new LiteralExpr(t, false); 

 			break;

 		}

-		case 91: {

+		case 88: {

 			Get();

 			e = new LiteralExpr(t, true); 

 			break;

 		}

-		case 92: {

+		case 89: {

 			Get();

 			e = new LiteralExpr(t); 

 			break;

@@ -2194,55 +2148,55 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new LiteralExpr(t, n); 

 			break;

 		}

-		case 93: {

+		case 90: {

 			Get();

 			e = new ThisExpr(t); 

 			break;

 		}

-		case 94: {

+		case 91: {

 			Get();

 			x = t; 

-			Expect(34);

+			Expect(31);

 			Expression(out e);

-			Expect(35);

+			Expect(32);

 			e = new FreshExpr(x, e); 

 			break;

 		}

-		case 95: {

+		case 92: {

 			Get();

 			x = t; 

-			Expect(34);

+			Expect(31);

 			Expression(out e);

-			Expect(35);

+			Expect(32);

 			e = new AllocatedExpr(x, e); 

 			break;

 		}

-		case 96: {

+		case 93: {

 			Get();

 			x = t; 

-			Expect(34);

+			Expect(31);

 			Expression(out e);

-			Expect(35);

+			Expect(32);

 			e = new OldExpr(x, e); 

 			break;

 		}

-		case 17: {

+		case 16: {

 			Get();

 			x = t; 

 			Expression(out e);

 			e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); 

-			Expect(17);

+			Expect(16);

 			break;

 		}

-		case 34: {

+		case 31: {

 			Get();

 			x = t; 

 			Expression(out e);

 			e = new ParensExpression(x, e); 

-			Expect(35);

+			Expect(32);

 			break;

 		}

-		default: SynErr(165); break;

+		default: SynErr(162); break;

 		}

 	}

 

@@ -2251,8 +2205,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		try {

 		 n = BigInteger.Parse(t.val);

 		} catch (System.FormatException) {

-		 SemErr("incorrectly formatted number");

-		 n = BigInteger.Zero;

+		  SemErr("incorrectly formatted number");

+		  n = BigInteger.Zero;

 		}

 		

 	}

@@ -2261,10 +2215,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  MatchCaseExpr/*!*/ c;

 		List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();

 		

-		Expect(62);

+		Expect(59);

 		x = t; 

 		Expression(out e);

-		while (la.kind == 58) {

+		while (la.kind == 55) {

 			CaseExpression(out c);

 			cases.Add(c); 

 		}

@@ -2279,20 +2233,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression range;

 		Expression/*!*/ body;

 		

-		if (la.kind == 99 || la.kind == 100) {

+		if (la.kind == 96 || la.kind == 97) {

 			Forall();

 			x = t;  univ = true; 

-		} else if (la.kind == 101 || la.kind == 102) {

+		} else if (la.kind == 98 || la.kind == 99) {

 			Exists();

 			x = t; 

-		} else SynErr(166);

+		} else SynErr(163);

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

 		QSep();

 		Expression(out body);

 		if (univ) {

 		 q = new ForallExpr(x, bvars, range, body, attrs);

 		} else {

-		 q = new ExistsExpr(x, bvars, range, body, attrs);

+		  q = new ExistsExpr(x, bvars, range, body, attrs);

 		}

 		

 	}

@@ -2305,18 +2259,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression/*!*/ range;

 		Expression body = null;

 		

-		Expect(39);

+		Expect(36);

 		x = t; 

 		IdentTypeOptional(out bv);

 		bvars.Add(bv); 

-		while (la.kind == 20) {

+		while (la.kind == 19) {

 			Get();

 			IdentTypeOptional(out bv);

 			bvars.Add(bv); 

 		}

-		Expect(17);

+		Expect(16);

 		Expression(out range);

-		if (la.kind == 103 || la.kind == 104) {

+		if (la.kind == 100 || la.kind == 101) {

 			QSep();

 			Expression(out body);

 		}

@@ -2331,47 +2285,47 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BoundVar/*!*/ bv;

 		Expression/*!*/ body;

 		

-		Expect(58);

+		Expect(55);

 		x = t; 

 		Ident(out id);

-		if (la.kind == 34) {

+		if (la.kind == 31) {

 			Get();

 			IdentTypeOptional(out bv);

 			arguments.Add(bv); 

-			while (la.kind == 20) {

+			while (la.kind == 19) {

 				Get();

 				IdentTypeOptional(out bv);

 				arguments.Add(bv); 

 			}

-			Expect(35);

+			Expect(32);

 		}

-		Expect(59);

+		Expect(56);

 		Expression(out body);

 		c = new MatchCaseExpr(x, id.val, arguments, body); 

 	}

 

 	void Forall() {

-		if (la.kind == 99) {

+		if (la.kind == 96) {

 			Get();

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

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

 			Get();

-		} else SynErr(167);

+		} else SynErr(164);

 	}

 

 	void Exists() {

-		if (la.kind == 101) {

+		if (la.kind == 98) {

 			Get();

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

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

 			Get();

-		} else SynErr(168);

+		} else SynErr(165);

 	}

 

 	void QSep() {

-		if (la.kind == 103) {

+		if (la.kind == 100) {

 			Get();

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

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

 			Get();

-		} else SynErr(169);

+		} else SynErr(166);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

@@ -2382,10 +2336,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expect(5);

 		Expect(1);

 		aName = t.val; 

-		if (StartOf(19)) {

+		if (StartOf(18)) {

 			AttributeArg(out aArg);

 			aArgs.Add(aArg); 

-			while (la.kind == 20) {

+			while (la.kind == 19) {

 				Get();

 				AttributeArg(out aArg);

 				aArgs.Add(aArg); 

@@ -2398,35 +2352,33 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	public void Parse() {

 		la = new Token();

-		la.val = "";

+		la.val = "";		

 		Get();

 		Dafny();

-		Expect(0);

 

-		Expect(0);

+    Expect(0);

 	}

-

+	

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

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

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

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

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

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

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

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

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

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

@@ -2435,20 +2387,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 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;

@@ -2462,169 +2412,166 @@ public class Errors {
 			case 8: s = "\"module\" expected"; break;

 			case 9: s = "\"imports\" expected"; break;

 			case 10: s = "\"class\" expected"; break;

-			case 11: s = "\"refines\" expected"; break;

-			case 12: s = "\"ghost\" expected"; break;

-			case 13: s = "\"static\" expected"; break;

-			case 14: s = "\"unlimited\" expected"; break;

-			case 15: s = "\"datatype\" expected"; break;

-			case 16: s = "\"=\" expected"; break;

-			case 17: s = "\"|\" expected"; break;

-			case 18: s = "\";\" expected"; break;

-			case 19: s = "\"var\" expected"; break;

-			case 20: s = "\",\" expected"; break;

-			case 21: s = "\"type\" expected"; break;

-			case 22: s = "\"replaces\" expected"; break;

-			case 23: s = "\"by\" expected"; break;

-			case 24: s = "\"<\" expected"; break;

-			case 25: s = "\">\" expected"; break;

-			case 26: s = "\"method\" expected"; break;

-			case 27: s = "\"constructor\" expected"; break;

-			case 28: s = "\"returns\" expected"; break;

-			case 29: s = "\"modifies\" expected"; break;

-			case 30: s = "\"free\" expected"; break;

-			case 31: s = "\"requires\" expected"; break;

-			case 32: s = "\"ensures\" expected"; break;

-			case 33: s = "\"decreases\" expected"; break;

-			case 34: s = "\"(\" expected"; break;

-			case 35: s = "\")\" expected"; break;

-			case 36: s = "\"bool\" expected"; break;

-			case 37: s = "\"nat\" expected"; break;

-			case 38: s = "\"int\" expected"; break;

-			case 39: s = "\"set\" expected"; break;

-			case 40: s = "\"multiset\" expected"; break;

-			case 41: s = "\"seq\" expected"; break;

-			case 42: s = "\"object\" expected"; break;

-			case 43: s = "\"function\" expected"; break;

-			case 44: s = "\"reads\" expected"; break;

-			case 45: s = "\"*\" expected"; break;

-			case 46: s = "\"`\" expected"; break;

-			case 47: s = "\"label\" expected"; break;

-			case 48: s = "\"break\" expected"; break;

-			case 49: s = "\"return\" expected"; break;

-			case 50: s = "\":=\" expected"; break;

-			case 51: s = "\"new\" expected"; break;

-			case 52: s = "\"[\" expected"; break;

-			case 53: s = "\"]\" expected"; break;

-			case 54: s = "\".\" expected"; break;

-			case 55: s = "\"choose\" expected"; break;

-			case 56: s = "\"if\" expected"; break;

-			case 57: s = "\"else\" expected"; break;

-			case 58: s = "\"case\" expected"; break;

-			case 59: s = "\"=>\" expected"; break;

-			case 60: s = "\"while\" expected"; break;

-			case 61: s = "\"invariant\" expected"; break;

-			case 62: s = "\"match\" expected"; break;

-			case 63: s = "\"assert\" expected"; break;

-			case 64: s = "\"assume\" expected"; break;

-			case 65: s = "\"print\" expected"; break;

-			case 66: s = "\"parallel\" expected"; break;

-			case 67: s = "\"<==>\" expected"; break;

-			case 68: s = "\"\\u21d4\" expected"; break;

-			case 69: s = "\"==>\" expected"; break;

-			case 70: s = "\"\\u21d2\" expected"; break;

-			case 71: s = "\"&&\" expected"; break;

-			case 72: s = "\"\\u2227\" expected"; break;

-			case 73: s = "\"||\" expected"; break;

-			case 74: s = "\"\\u2228\" expected"; break;

-			case 75: s = "\"==\" expected"; break;

-			case 76: s = "\"<=\" expected"; break;

-			case 77: s = "\">=\" expected"; break;

-			case 78: s = "\"!=\" expected"; break;

-			case 79: s = "\"!!\" expected"; break;

-			case 80: s = "\"in\" expected"; break;

-			case 81: s = "\"!\" expected"; break;

-			case 82: s = "\"\\u2260\" expected"; break;

-			case 83: s = "\"\\u2264\" expected"; break;

-			case 84: s = "\"\\u2265\" expected"; break;

-			case 85: s = "\"+\" expected"; break;

-			case 86: s = "\"-\" expected"; break;

-			case 87: s = "\"/\" expected"; break;

-			case 88: s = "\"%\" expected"; break;

-			case 89: s = "\"\\u00ac\" expected"; break;

-			case 90: s = "\"false\" expected"; break;

-			case 91: s = "\"true\" expected"; break;

-			case 92: s = "\"null\" expected"; break;

-			case 93: s = "\"this\" expected"; break;

-			case 94: s = "\"fresh\" expected"; break;

-			case 95: s = "\"allocated\" expected"; break;

-			case 96: s = "\"old\" expected"; break;

-			case 97: s = "\"then\" expected"; break;

-			case 98: s = "\"..\" expected"; break;

-			case 99: s = "\"forall\" expected"; break;

-			case 100: s = "\"\\u2200\" expected"; break;

-			case 101: s = "\"exists\" expected"; break;

-			case 102: s = "\"\\u2203\" expected"; break;

-			case 103: s = "\"::\" expected"; break;

-			case 104: s = "\"\\u2022\" expected"; break;

-			case 105: s = "??? expected"; break;

-			case 106: s = "this symbol not expected in ClassDecl"; break;

-			case 107: s = "this symbol not expected in DatatypeDecl"; break;

-			case 108: s = "this symbol not expected in DatatypeDecl"; break;

-			case 109: s = "this symbol not expected in ArbitraryTypeDecl"; break;

-			case 110: s = "invalid ClassMemberDecl"; break;

-			case 111: s = "this symbol not expected in FieldDecl"; break;

-			case 112: s = "this symbol not expected in FieldDecl"; break;

-			case 113: s = "this symbol not expected in MethodDecl"; break;

-			case 114: s = "invalid MethodDecl"; break;

-			case 115: s = "invalid TypeAndToken"; break;

+			case 11: s = "\"ghost\" expected"; break;

+			case 12: s = "\"static\" expected"; break;

+			case 13: s = "\"unlimited\" expected"; break;

+			case 14: s = "\"datatype\" expected"; break;

+			case 15: s = "\"=\" expected"; break;

+			case 16: s = "\"|\" expected"; break;

+			case 17: s = "\";\" expected"; break;

+			case 18: s = "\"var\" expected"; break;

+			case 19: s = "\",\" expected"; break;

+			case 20: s = "\"type\" expected"; break;

+			case 21: s = "\"<\" expected"; break;

+			case 22: s = "\">\" expected"; break;

+			case 23: s = "\"method\" expected"; break;

+			case 24: s = "\"constructor\" expected"; break;

+			case 25: s = "\"returns\" expected"; break;

+			case 26: s = "\"modifies\" expected"; break;

+			case 27: s = "\"free\" expected"; break;

+			case 28: s = "\"requires\" expected"; break;

+			case 29: s = "\"ensures\" expected"; break;

+			case 30: s = "\"decreases\" expected"; break;

+			case 31: s = "\"(\" expected"; break;

+			case 32: s = "\")\" expected"; break;

+			case 33: s = "\"bool\" expected"; break;

+			case 34: s = "\"nat\" expected"; break;

+			case 35: s = "\"int\" expected"; break;

+			case 36: s = "\"set\" expected"; break;

+			case 37: s = "\"multiset\" expected"; break;

+			case 38: s = "\"seq\" expected"; break;

+			case 39: s = "\"object\" expected"; break;

+			case 40: s = "\"function\" expected"; break;

+			case 41: s = "\"reads\" expected"; break;

+			case 42: s = "\"*\" expected"; break;

+			case 43: s = "\"`\" expected"; break;

+			case 44: s = "\"label\" expected"; break;

+			case 45: s = "\"break\" expected"; break;

+			case 46: s = "\"return\" expected"; break;

+			case 47: s = "\":=\" expected"; break;

+			case 48: s = "\"new\" expected"; break;

+			case 49: s = "\"[\" expected"; break;

+			case 50: s = "\"]\" expected"; break;

+			case 51: s = "\".\" expected"; break;

+			case 52: s = "\"choose\" expected"; break;

+			case 53: s = "\"if\" expected"; break;

+			case 54: s = "\"else\" expected"; break;

+			case 55: s = "\"case\" expected"; break;

+			case 56: s = "\"=>\" expected"; break;

+			case 57: s = "\"while\" expected"; break;

+			case 58: s = "\"invariant\" expected"; break;

+			case 59: s = "\"match\" expected"; break;

+			case 60: s = "\"assert\" expected"; break;

+			case 61: s = "\"assume\" expected"; break;

+			case 62: s = "\"print\" expected"; break;

+			case 63: s = "\"parallel\" expected"; break;

+			case 64: s = "\"<==>\" expected"; break;

+			case 65: s = "\"\\u21d4\" expected"; break;

+			case 66: s = "\"==>\" expected"; break;

+			case 67: s = "\"\\u21d2\" expected"; break;

+			case 68: s = "\"&&\" expected"; break;

+			case 69: s = "\"\\u2227\" expected"; break;

+			case 70: s = "\"||\" expected"; break;

+			case 71: s = "\"\\u2228\" expected"; break;

+			case 72: s = "\"==\" expected"; break;

+			case 73: s = "\"<=\" expected"; break;

+			case 74: s = "\">=\" expected"; break;

+			case 75: s = "\"!=\" expected"; break;

+			case 76: s = "\"!!\" expected"; break;

+			case 77: s = "\"in\" expected"; break;

+			case 78: s = "\"!\" expected"; break;

+			case 79: s = "\"\\u2260\" expected"; break;

+			case 80: s = "\"\\u2264\" expected"; break;

+			case 81: s = "\"\\u2265\" expected"; break;

+			case 82: s = "\"+\" expected"; break;

+			case 83: s = "\"-\" expected"; break;

+			case 84: s = "\"/\" expected"; break;

+			case 85: s = "\"%\" expected"; break;

+			case 86: s = "\"\\u00ac\" expected"; break;

+			case 87: s = "\"false\" expected"; break;

+			case 88: s = "\"true\" expected"; break;

+			case 89: s = "\"null\" expected"; break;

+			case 90: s = "\"this\" expected"; break;

+			case 91: s = "\"fresh\" expected"; break;

+			case 92: s = "\"allocated\" expected"; break;

+			case 93: s = "\"old\" expected"; break;

+			case 94: s = "\"then\" expected"; break;

+			case 95: s = "\"..\" expected"; break;

+			case 96: s = "\"forall\" expected"; break;

+			case 97: s = "\"\\u2200\" expected"; break;

+			case 98: s = "\"exists\" expected"; break;

+			case 99: s = "\"\\u2203\" expected"; break;

+			case 100: s = "\"::\" expected"; break;

+			case 101: s = "\"\\u2022\" expected"; break;

+			case 102: s = "??? expected"; break;

+			case 103: s = "this symbol not expected in ClassDecl"; break;

+			case 104: s = "this symbol not expected in DatatypeDecl"; break;

+			case 105: s = "this symbol not expected in DatatypeDecl"; break;

+			case 106: s = "this symbol not expected in ArbitraryTypeDecl"; break;

+			case 107: s = "invalid ClassMemberDecl"; break;

+			case 108: s = "this symbol not expected in FieldDecl"; break;

+			case 109: s = "this symbol not expected in FieldDecl"; break;

+			case 110: s = "this symbol not expected in MethodDecl"; break;

+			case 111: s = "invalid MethodDecl"; break;

+			case 112: s = "invalid TypeAndToken"; break;

+			case 113: s = "this symbol not expected in MethodSpec"; break;

+			case 114: s = "this symbol not expected in MethodSpec"; break;

+			case 115: s = "this symbol not expected in MethodSpec"; break;

 			case 116: s = "this symbol not expected in MethodSpec"; break;

-			case 117: s = "this symbol not expected in MethodSpec"; break;

+			case 117: s = "invalid MethodSpec"; break;

 			case 118: s = "this symbol not expected in MethodSpec"; break;

-			case 119: s = "this symbol not expected in MethodSpec"; break;

-			case 120: s = "invalid MethodSpec"; break;

-			case 121: s = "this symbol not expected in MethodSpec"; break;

-			case 122: s = "invalid MethodSpec"; break;

-			case 123: s = "invalid ReferenceType"; break;

+			case 119: s = "invalid MethodSpec"; break;

+			case 120: s = "invalid ReferenceType"; break;

+			case 121: s = "this symbol not expected in FunctionSpec"; break;

+			case 122: s = "this symbol not expected in FunctionSpec"; break;

+			case 123: s = "this symbol not expected in FunctionSpec"; break;

 			case 124: s = "this symbol not expected in FunctionSpec"; break;

 			case 125: s = "this symbol not expected in FunctionSpec"; break;

-			case 126: s = "this symbol not expected in FunctionSpec"; break;

-			case 127: s = "this symbol not expected in FunctionSpec"; break;

-			case 128: s = "this symbol not expected in FunctionSpec"; break;

-			case 129: s = "invalid FunctionSpec"; break;

-			case 130: s = "invalid PossiblyWildFrameExpression"; break;

-			case 131: s = "invalid PossiblyWildExpression"; break;

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

-			case 133: s = "invalid OneStmt"; break;

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

-			case 135: s = "invalid OneStmt"; break;

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

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

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

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

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

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

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

+			case 126: s = "invalid FunctionSpec"; break;

+			case 127: s = "invalid PossiblyWildFrameExpression"; break;

+			case 128: s = "invalid PossiblyWildExpression"; break;

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

+			case 130: s = "invalid OneStmt"; break;

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

+			case 132: s = "invalid OneStmt"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 

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

 		}

-		return s;

+    return s;

 	}

 

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

@@ -2632,9 +2579,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++;

 	}

@@ -2650,5 +2596,4 @@ public class FatalError: Exception {
 	public FatalError(string m): base(m) {}

 }

 

-

 }
\ No newline at end of file
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 4290953b..0912c58d 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -91,10 +91,6 @@ namespace Microsoft.Dafny {
       Contract.Requires(c != null);

       Indent(indent);

       PrintClassMethodHelper("class", c.Attributes, c.Name, c.TypeArgs);

-      if (c is ClassRefinementDecl) {

-        wr.Write(" refines ");

-        wr.Write(((ClassRefinementDecl)c).RefinedClass.val);

-      }

       if (c.Members.Count == 0) {

         wr.WriteLine(" { }");

       } else {

@@ -124,10 +120,6 @@ namespace Microsoft.Dafny {
           if (state != 0) { wr.WriteLine(); }

           PrintFunction((Function)m, indent);

           state = 2;

-        } else if (m is CouplingInvariant) {

-          wr.WriteLine();

-          PrintCouplingInvariant((CouplingInvariant)m, indent);

-          state = 2;

         } else {

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

         }

@@ -222,21 +214,6 @@ namespace Microsoft.Dafny {
       wr.WriteLine(";");

     }

 

-    public void PrintCouplingInvariant(CouplingInvariant inv, int indent) {

-      Contract.Requires(inv != null);

-      Indent(indent);

-      wr.Write("replaces");

-      string sep = " ";

-      foreach (string tok in inv.Tokens()) {

-        wr.Write(sep);

-        wr.Write(tok);

-        sep = ", ";

-      }

-      wr.Write(" by ");

-      PrintExpression(inv.Expr);

-      wr.WriteLine(";");

-    }

-

     public void PrintFunction(Function f, int indent) {

       Contract.Requires(f != null);

       Indent(indent);

@@ -281,7 +258,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(method != null);

 

       Indent(indent);

-      string k = method is MethodRefinement ? "refines" : method is Constructor ? "constructor" : "method";

+      string k = method is Constructor ? "constructor" : "method";

       if (method.IsStatic) { k = "static " + k; }

       if (method.IsGhost) { k = "ghost " + k; }

       PrintClassMethodHelper(k, method.Attributes, method.Name, method.TypeArgs);

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 3705db22..4f62745d 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -80,8 +80,6 @@ namespace Microsoft.Dafny {
       Contract.Invariant(cce.NonNullDictionaryAndValues(datatypeCtors) && Contract.ForAll(datatypeCtors.Values, v => cce.NonNullDictionaryAndValues(v)));

     }

 

-    bool checkRefinements = true; // used to indicate a cycle in refinements

-

     public void ResolveProgram(Program prog) {

       Contract.Requires(prog != null);

       // register modules

@@ -95,7 +93,6 @@ namespace Microsoft.Dafny {
       }

       // resolve imports and register top-level declarations

       RegisterTopLevelDecls(prog.BuiltIns.SystemModule.TopLevelDecls);

-      Graph<TopLevelDecl> refines = new Graph<TopLevelDecl>();

       foreach (ModuleDecl m in prog.Modules) {

         importGraph.AddVertex(m);

         foreach (string imp in m.Imports) {

@@ -110,7 +107,6 @@ namespace Microsoft.Dafny {
           }

         }

         RegisterTopLevelDecls(m.TopLevelDecls);

-        foreach (TopLevelDecl decl in m.TopLevelDecls) {Contract.Assert(decl != null); refines.AddVertex(decl);}

       }

       // check for cycles in the import graph

       List<ModuleDecl> cycle = importGraph.TryFindCycle();

@@ -133,28 +129,6 @@ namespace Microsoft.Dafny {
         }

       }

 

-      // resolve top-level declarations of refinements

-      foreach (ModuleDecl m in prog.Modules)

-        foreach (TopLevelDecl decl in m.TopLevelDecls)

-          if (decl is ClassRefinementDecl) {

-            ClassRefinementDecl rdecl = (ClassRefinementDecl) decl;

-            ResolveTopLevelRefinement(rdecl);

-            if (rdecl.Refined != null) refines.AddEdge(rdecl, rdecl.Refined);

-          }

-

-      // attempt finding refinement cycles

-      List<TopLevelDecl> refinesCycle = refines.TryFindCycle();

-      if (refinesCycle != null) {

-        string cy = "";

-        string sep = "";

-        foreach (TopLevelDecl decl in refinesCycle) {

-          cy = decl + sep + cy;

-          sep = " -> ";

-        }

-        Error(refinesCycle[0], "Detected a cyclic refinement declaration: {0}", cy);

-        checkRefinements = false;

-      }

-

       // resolve top-level declarations

       Graph<DatatypeDecl> datatypeDependencies = new Graph<DatatypeDecl>();

       foreach (ModuleDecl m in prog.Modules) {

@@ -273,21 +247,6 @@ namespace Microsoft.Dafny {
       }

     }

 

-    public void ResolveTopLevelRefinement(ClassRefinementDecl decl) {

-      Contract.Requires(decl != null);

-      if (!classes.ContainsKey(decl.RefinedClass.val)) {

-        Error(decl.RefinedClass, "Refined class declaration is missing: {0}", decl.RefinedClass.val);

-      } else {

-        TopLevelDecl a = classes[decl.RefinedClass.val];

-        if (!(a is ClassDecl)) {

-          Error(a, "Refined declaration is not a class declaration: {0}", a.Name);

-          return;

-        }

-        decl.Refined = cce.NonNull((ClassDecl) a);

-        // TODO: copy over remaining members of a

-      }

-    }

-

     public void ResolveTopLevelDecls_Signatures(List<TopLevelDecl/*!*/>/*!*/ declarations, Graph<DatatypeDecl/*!*/>/*!*/ datatypeDependencies) {

       Contract.Requires(declarations != null);

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

@@ -365,49 +324,9 @@ namespace Microsoft.Dafny {
           ResolveMethodSignature(m);

           allTypeParameters.PopMarker();

 

-        } else if (member is CouplingInvariant) {

-          CouplingInvariant inv = (CouplingInvariant)member;

-          if (currentClass is ClassRefinementDecl) {

-            ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;

-            if (refined != null) {

-              Contract.Assert(classMembers.ContainsKey(refined));

-              Dictionary<string,MemberDecl> members = classMembers[refined];

-

-              // resolve abstracted fields in the refined class

-              List<Field> fields = new List<Field>();

-              foreach (IToken tok in inv.Toks) {

-                if (!members.ContainsKey(tok.val))

-                  Error(tok, "Refined class does not declare a field: {0}", tok.val);

-                else {

-                  MemberDecl field = members[tok.val];

-                  if (!(field is Field))

-                    Error(tok, "Coupling invariant refers to a non-field member: {0}", tok.val);

-                  else if (fields.Contains(cce.NonNull((Field)field)))

-                    Error(tok, "Duplicate reference to a field in the refined class: {0}", tok.val);

-                  else

-                    fields.Add(cce.NonNull((Field)field));

-                }

-              }

-              inv.Refined = fields;

-            }

-

-          } else {

-            Error(member, "Coupling invariants can only be declared in refinement classes");

-          }

         } else {

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

         }

-

-        if (currentClass is ClassRefinementDecl) {

-          ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;

-          if (refined != null) {

-            Contract.Assert(classMembers.ContainsKey(refined));

-

-            // there is a member with the same name in refined class if and only if the member is a refined method

-            if ((member is MethodRefinement) != (classMembers[refined].ContainsKey(member.Name)))

-              Error(member, "Refined class has a member with the same name as in the refinement class: {0}", member.Name);

-          }

-        }

       }

       currentClass = null;

     }

@@ -441,48 +360,6 @@ namespace Microsoft.Dafny {
           ResolveTypeParameters(m.TypeArgs, false, m);

           ResolveMethod(m);

           allTypeParameters.PopMarker();

-

-          // check if signature of the refined method matches the refinement method

-          if (member is MethodRefinement) {

-            MethodRefinement mf = (MethodRefinement)member;

-            if (currentClass is ClassRefinementDecl) {

-              // should have already been resolved

-              if (((ClassRefinementDecl)currentClass).Refined != null) {

-                MemberDecl d = classMembers[((ClassRefinementDecl)currentClass).Refined][mf.Name];

-                if (d is Method) {

-                  mf.Refined = (Method)d;

-                  if (mf.Ins.Count != mf.Refined.Ins.Count)

-                    Error(mf, "Different number of input variables");

-                  if (mf.Outs.Count != mf.Refined.Outs.Count)

-                    Error(mf, "Different number of output variables");

-                  if (mf.IsStatic || mf.Refined.IsStatic)

-                    Error(mf, "Refined methods cannot be static");

-                } else {

-                  Error(member, "Refined class has a non-method member with the same name: {0}", member.Name);

-                }

-              }

-            } else {

-              Error(member, "Refinement methods can only be declared in refinement classes: {0}", member.Name);

-            }

-          }

-

-        } else if (member is CouplingInvariant) {

-          CouplingInvariant inv = (CouplingInvariant)member;

-          ResolveAttributes(member.Attributes, false);

-          if (inv.Refined != null) {

-            inv.Formals = new List<Formal>();

-            scope.PushMarker();

-            for (int i = 0; i < inv.Refined.Count; i++) {

-              Field field = inv.Refined[i];

-              Contract.Assert(field != null);

-              Formal formal = new Formal(inv.Toks[i], field.Name, field.Type, true, field.IsGhost);

-              Contract.Assert(formal != null);

-              inv.Formals.Add(formal);

-              scope.Push(inv.Toks[i].val, formal);

-            }

-            ResolveExpression(inv.Expr, false);

-            scope.PopMarker();

-          }

         } else {

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

         }

@@ -616,13 +493,6 @@ namespace Microsoft.Dafny {
 

       Contract.Requires(tparams != null);

       Contract.Requires(parent != null);

-      // push type arguments of the refined class

-      if (checkRefinements && parent is ClassRefinementDecl) {

-        ClassDecl refined = ((ClassRefinementDecl)parent).Refined;

-        if (refined != null)

-          ResolveTypeParameters(refined.TypeArgs, false, refined);

-      }

-

       // push non-duplicated type parameter names

       foreach (TypeParameter tp in tparams) {

         Contract.Assert(tp != null);

diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index 1ec3ac6f..e4d769d9 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/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.

@@ -211,28 +209,26 @@ public class UTF8Buffer: Buffer {
 public class Scanner {

 	const char EOL = '\n';

 	const int eofSym = 0; /* pdt */

-	const int maxT = 105;

-	const int noSym = 105;

-

-

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

-	}

-

+	const int maxT = 102;

+	const int noSym = 102;

+

+

+[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

-	int charPos;

 	int col;          // column number of current character

 	int line;         // line number of current character

 	int oldEols;      // EOLs that appeared in a comment;

@@ -240,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;

@@ -294,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;

@@ -306,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);

@@ -322,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;

@@ -345,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;

@@ -360,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++;

@@ -368,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

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

 			  }

 

-

+			

 		}

 

 	}

@@ -440,7 +438,7 @@ public class Scanner {
 

 

 	bool Comment0() {

-		int level = 1, pos0 = pos, line0 = line, col0 = col, charPos0 = charPos;

+		int level = 1, pos0 = pos, line0 = line, col0 = col;

 		NextCh();

 		if (ch == '/') {

 			NextCh();

@@ -453,13 +451,13 @@ public class Scanner {
 				else NextCh();

 			}

 		} else {

-			buffer.Pos = pos0; NextCh(); line = line0; col = col0; charPos = charPos0;

+			buffer.Pos = pos0; NextCh(); line = line0; col = col0;

 		}

 		return false;

 	}

 

 	bool Comment1() {

-		int level = 1, pos0 = pos, line0 = line, col0 = col, charPos0 = charPos;

+		int level = 1, pos0 = pos, line0 = line, col0 = col;

 		NextCh();

 		if (ch == '*') {

 			NextCh();

@@ -480,7 +478,7 @@ public class Scanner {
 				else NextCh();

 			}

 		} else {

-			buffer.Pos = pos0; NextCh(); line = line0; col = col0; charPos = charPos0;

+			buffer.Pos = pos0; NextCh(); line = line0; col = col0;

 		}

 		return false;

 	}

@@ -491,58 +489,55 @@ public class Scanner {
 			case "module": t.kind = 8; break;

 			case "imports": t.kind = 9; break;

 			case "class": t.kind = 10; break;

-			case "refines": t.kind = 11; break;

-			case "ghost": t.kind = 12; break;

-			case "static": t.kind = 13; break;

-			case "unlimited": t.kind = 14; break;

-			case "datatype": t.kind = 15; break;

-			case "var": t.kind = 19; break;

-			case "type": t.kind = 21; break;

-			case "replaces": t.kind = 22; break;

-			case "by": t.kind = 23; break;

-			case "method": t.kind = 26; break;

-			case "constructor": t.kind = 27; break;

-			case "returns": t.kind = 28; break;

-			case "modifies": t.kind = 29; break;

-			case "free": t.kind = 30; break;

-			case "requires": t.kind = 31; break;

-			case "ensures": t.kind = 32; break;

-			case "decreases": t.kind = 33; break;

-			case "bool": t.kind = 36; break;

-			case "nat": t.kind = 37; break;

-			case "int": t.kind = 38; break;

-			case "set": t.kind = 39; break;

-			case "multiset": t.kind = 40; break;

-			case "seq": t.kind = 41; break;

-			case "object": t.kind = 42; break;

-			case "function": t.kind = 43; break;

-			case "reads": t.kind = 44; break;

-			case "label": t.kind = 47; break;

-			case "break": t.kind = 48; break;

-			case "return": t.kind = 49; break;

-			case "new": t.kind = 51; break;

-			case "choose": t.kind = 55; break;

-			case "if": t.kind = 56; break;

-			case "else": t.kind = 57; break;

-			case "case": t.kind = 58; break;

-			case "while": t.kind = 60; break;

-			case "invariant": t.kind = 61; break;

-			case "match": t.kind = 62; break;

-			case "assert": t.kind = 63; break;

-			case "assume": t.kind = 64; break;

-			case "print": t.kind = 65; break;

-			case "parallel": t.kind = 66; break;

-			case "in": t.kind = 80; break;

-			case "false": t.kind = 90; break;

-			case "true": t.kind = 91; break;

-			case "null": t.kind = 92; break;

-			case "this": t.kind = 93; break;

-			case "fresh": t.kind = 94; break;

-			case "allocated": t.kind = 95; break;

-			case "old": t.kind = 96; break;

-			case "then": t.kind = 97; break;

-			case "forall": t.kind = 99; break;

-			case "exists": t.kind = 101; break;

+			case "ghost": t.kind = 11; break;

+			case "static": t.kind = 12; break;

+			case "unlimited": t.kind = 13; break;

+			case "datatype": t.kind = 14; break;

+			case "var": t.kind = 18; break;

+			case "type": t.kind = 20; break;

+			case "method": t.kind = 23; break;

+			case "constructor": t.kind = 24; break;

+			case "returns": t.kind = 25; break;

+			case "modifies": t.kind = 26; break;

+			case "free": t.kind = 27; break;

+			case "requires": t.kind = 28; break;

+			case "ensures": t.kind = 29; break;

+			case "decreases": t.kind = 30; break;

+			case "bool": t.kind = 33; break;

+			case "nat": t.kind = 34; break;

+			case "int": t.kind = 35; break;

+			case "set": t.kind = 36; break;

+			case "multiset": t.kind = 37; break;

+			case "seq": t.kind = 38; break;

+			case "object": t.kind = 39; break;

+			case "function": t.kind = 40; break;

+			case "reads": t.kind = 41; break;

+			case "label": t.kind = 44; break;

+			case "break": t.kind = 45; break;

+			case "return": t.kind = 46; break;

+			case "new": t.kind = 48; break;

+			case "choose": t.kind = 52; break;

+			case "if": t.kind = 53; break;

+			case "else": t.kind = 54; break;

+			case "case": t.kind = 55; break;

+			case "while": t.kind = 57; break;

+			case "invariant": t.kind = 58; break;

+			case "match": t.kind = 59; break;

+			case "assert": t.kind = 60; break;

+			case "assume": t.kind = 61; break;

+			case "print": t.kind = 62; break;

+			case "parallel": t.kind = 63; break;

+			case "in": t.kind = 77; break;

+			case "false": t.kind = 87; break;

+			case "true": t.kind = 88; break;

+			case "null": t.kind = 89; break;

+			case "this": t.kind = 90; break;

+			case "fresh": t.kind = 91; break;

+			case "allocated": t.kind = 92; break;

+			case "old": t.kind = 93; break;

+			case "then": t.kind = 94; break;

+			case "forall": t.kind = 96; break;

+			case "exists": t.kind = 98; break;

 			default: break;

 		}

 	}

@@ -559,13 +554,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: {

@@ -648,131 +640,131 @@ public class Scanner {
 				else if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;}

 				else {t.kind = 3; break;}

 			case 19:

-				{t.kind = 18; break;}

+				{t.kind = 17; break;}

 			case 20:

-				{t.kind = 20; break;}

+				{t.kind = 19; break;}

 			case 21:

-				{t.kind = 34; break;}

+				{t.kind = 31; break;}

 			case 22:

-				{t.kind = 35; break;}

+				{t.kind = 32; break;}

 			case 23:

-				{t.kind = 45; break;}

+				{t.kind = 42; break;}

 			case 24:

-				{t.kind = 46; break;}

+				{t.kind = 43; break;}

 			case 25:

-				{t.kind = 50; break;}

+				{t.kind = 47; break;}

 			case 26:

-				{t.kind = 52; break;}

+				{t.kind = 49; break;}

 			case 27:

-				{t.kind = 53; break;}

+				{t.kind = 50; break;}

 			case 28:

-				{t.kind = 59; break;}

+				{t.kind = 56; break;}

 			case 29:

 				if (ch == '>') {AddCh(); goto case 30;}

 				else {goto case 0;}

 			case 30:

-				{t.kind = 67; break;}

+				{t.kind = 64; break;}

 			case 31:

-				{t.kind = 68; break;}

+				{t.kind = 65; break;}

 			case 32:

-				{t.kind = 69; break;}

+				{t.kind = 66; break;}

 			case 33:

-				{t.kind = 70; break;}

+				{t.kind = 67; break;}

 			case 34:

 				if (ch == '&') {AddCh(); goto case 35;}

 				else {goto case 0;}

 			case 35:

-				{t.kind = 71; break;}

+				{t.kind = 68; break;}

 			case 36:

-				{t.kind = 72; break;}

+				{t.kind = 69; break;}

 			case 37:

-				{t.kind = 73; break;}

+				{t.kind = 70; break;}

 			case 38:

-				{t.kind = 74; break;}

+				{t.kind = 71; break;}

 			case 39:

-				{t.kind = 77; break;}

+				{t.kind = 74; break;}

 			case 40:

-				{t.kind = 78; break;}

+				{t.kind = 75; break;}

 			case 41:

-				{t.kind = 79; break;}

+				{t.kind = 76; break;}

 			case 42:

-				{t.kind = 82; break;}

+				{t.kind = 79; break;}

 			case 43:

-				{t.kind = 83; break;}

+				{t.kind = 80; break;}

 			case 44:

-				{t.kind = 84; break;}

+				{t.kind = 81; break;}

 			case 45:

-				{t.kind = 85; break;}

+				{t.kind = 82; break;}

 			case 46:

-				{t.kind = 86; break;}

+				{t.kind = 83; break;}

 			case 47:

-				{t.kind = 87; break;}

+				{t.kind = 84; break;}

 			case 48:

-				{t.kind = 88; break;}

+				{t.kind = 85; break;}

 			case 49:

-				{t.kind = 89; break;}

+				{t.kind = 86; break;}

 			case 50:

-				{t.kind = 98; break;}

+				{t.kind = 95; break;}

 			case 51:

-				{t.kind = 100; break;}

+				{t.kind = 97; break;}

 			case 52:

-				{t.kind = 102; break;}

+				{t.kind = 99; break;}

 			case 53:

-				{t.kind = 103; break;}

+				{t.kind = 100; break;}

 			case 54:

-				{t.kind = 104; break;}

+				{t.kind = 101; break;}

 			case 55:

 				recEnd = pos; recKind = 5;

 				if (ch == '=') {AddCh(); goto case 25;}

 				else if (ch == ':') {AddCh(); goto case 53;}

 				else {t.kind = 5; break;}

 			case 56:

-				recEnd = pos; recKind = 16;

+				recEnd = pos; recKind = 15;

 				if (ch == '>') {AddCh(); goto case 28;}

 				else if (ch == '=') {AddCh(); goto case 62;}

-				else {t.kind = 16; break;}

+				else {t.kind = 15; break;}

 			case 57:

-				recEnd = pos; recKind = 17;

+				recEnd = pos; recKind = 16;

 				if (ch == '|') {AddCh(); goto case 37;}

-				else {t.kind = 17; break;}

+				else {t.kind = 16; break;}

 			case 58:

-				recEnd = pos; recKind = 24;

+				recEnd = pos; recKind = 21;

 				if (ch == '=') {AddCh(); goto case 63;}

-				else {t.kind = 24; break;}

+				else {t.kind = 21; break;}

 			case 59:

-				recEnd = pos; recKind = 25;

+				recEnd = pos; recKind = 22;

 				if (ch == '=') {AddCh(); goto case 39;}

-				else {t.kind = 25; break;}

+				else {t.kind = 22; break;}

 			case 60:

-				recEnd = pos; recKind = 54;

+				recEnd = pos; recKind = 51;

 				if (ch == '.') {AddCh(); goto case 50;}

-				else {t.kind = 54; break;}

+				else {t.kind = 51; break;}

 			case 61:

-				recEnd = pos; recKind = 81;

+				recEnd = pos; recKind = 78;

 				if (ch == '=') {AddCh(); goto case 40;}

 				else if (ch == '!') {AddCh(); goto case 41;}

-				else {t.kind = 81; break;}

+				else {t.kind = 78; break;}

 			case 62:

-				recEnd = pos; recKind = 75;

+				recEnd = pos; recKind = 72;

 				if (ch == '>') {AddCh(); goto case 32;}

-				else {t.kind = 75; break;}

+				else {t.kind = 72; break;}

 			case 63:

-				recEnd = pos; recKind = 76;

+				recEnd = pos; recKind = 73;

 				if (ch == '=') {AddCh(); goto case 29;}

-				else {t.kind = 76; break;}

+				else {t.kind = 73; break;}

 

 		}

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

@@ -793,7 +785,7 @@ public class Scanner {
 			}

 			pt = pt.next;

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

-

+	

 		return pt;

 	}

 

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 9ef34758..da0607e0 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -589,14 +589,6 @@ namespace Microsoft.Dafny {
             AddMethodImpl(m, proc, false);

           }

 

-          // refinement condition

-          if (member is MethodRefinement) {

-            AddMethodRefinement((MethodRefinement)member);

-          }

-

-        } else if (member is CouplingInvariant) {

-          // TODO: define a well-foundedness condition to check

-

         } else {

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

         }

@@ -2810,7 +2802,6 @@ namespace Microsoft.Dafny {
     /// <summary>

     /// This method is expected to be called just twice for each procedure in the program (once with

     /// wellformednessProc set to true, once with wellformednessProc set to false).

-    /// In addition, it is used once to generate refinement conditions.

     /// </summary>

     Bpl.Procedure AddMethod(Method m, bool wellformednessProc, bool skipEnsures)

     {

@@ -2900,191 +2891,6 @@ namespace Microsoft.Dafny {
       return proc;

     }

 

-    #region Refinement extension

-

-    void AddMethodRefinement(MethodRefinement m)

-     {

-      Contract.Requires(m != null);

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

-      // r is abstract, m is concrete

-      Method r = m.Refined;

-      Contract.Assert(r != null);

-      Contract.Assert(m.EnclosingClass != null);

-      string name = "Refinement$$" + m.FullName;

-      string that = "that";

-

-      Bpl.IdentifierExpr heap = new Bpl.IdentifierExpr(m.tok, predef.HeapVarName, predef.HeapType);

-      ExpressionTranslator etran = new ExpressionTranslator(this, predef, heap, that);

-

-      // TODO: this straight inlining does not handle recursive calls

-      // TODO: we assume frame allows anything to be changed -- we don't include post-conditions in the refinement procedure, or check refinement of frames

-

-      // generate procedure declaration with pre-condition wp(r, true)

-      Bpl.Procedure proc = AddMethod(r, false, true);

-      proc.Name = name;

-

-      // create "that" for m

-      Bpl.Expr wh = Bpl.Expr.And(

-        Bpl.Expr.Neq(new Bpl.IdentifierExpr(m.tok, that, predef.RefType), predef.Null),

-        etran.GoodRef(m.tok, new Bpl.IdentifierExpr(m.tok, that, predef.RefType), Resolver.GetReceiverType(m.tok, m)));

-      Bpl.Formal thatVar = new Bpl.Formal(m.tok, new Bpl.TypedIdent(m.tok, that, predef.RefType, wh), true);

-      proc.InParams.Add(thatVar);

-

-      // add outs of m to the outs of the refinement procedure

-      foreach (Formal p in m.Outs) {

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

-        Bpl.Expr w = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);

-        proc.OutParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, w), false));

-      }

-      sink.TopLevelDeclarations.Add(proc);

-

-      // generate procedure implementation:

-      Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);

-      Bpl.VariableSeq inParams = Bpl.Formal.StripWhereClauses(proc.InParams);

-      Bpl.VariableSeq outParams = Bpl.Formal.StripWhereClauses(proc.OutParams);

-      Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();

-      Bpl.VariableSeq localVariables = new Bpl.VariableSeq();

-

-      Contract.Assert(m.Body != null);

-      Contract.Assert(r.Body != null);

-

-      // declare a frame variable that allows anything to be changed (not checking modifies clauses)

-      Bpl.IdentifierExpr theFrame = etran.TheFrame(m.tok);

-      Contract.Assert(theFrame.Type != null);

-      Bpl.LocalVariable frame = new Bpl.LocalVariable(m.tok, new Bpl.TypedIdent(m.tok, theFrame.Name, theFrame.Type));

-      localVariables.Add(frame);

-      // $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: true);

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

-      Bpl.BoundVariable oVar = new Bpl.BoundVariable(m.tok, new Bpl.TypedIdent(m.tok, "$o", predef.RefType));

-      Bpl.BoundVariable fVar = new Bpl.BoundVariable(m.tok, new Bpl.TypedIdent(m.tok, "$f", predef.FieldName(m.tok, alpha)));

-      Bpl.Expr lambda = new Bpl.LambdaExpr(m.tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, Bpl.Expr.True);

-      builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, frame), lambda));

-

-      // assume I($Heap, $Heap)

-      builder.Add(new Bpl.AssumeCmd(m.tok, TrCouplingInvariant(m, heap, "this", heap, that)));

-

-      // assign input formals of m (except "this")

-      for (int i = 0; i < m.Ins.Count; i++) {

-        Bpl.LocalVariable arg = new Bpl.LocalVariable(m.tok, new Bpl.TypedIdent(m.tok, m.Ins[i].UniqueName, TrType(m.Ins[i].Type)));

-        localVariables.Add(arg);

-        Bpl.Variable var = inParams[i+1];

-        Contract.Assert(var != null);

-        builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, arg), new Bpl.IdentifierExpr(m.tok, var)));

-      }

-

-      // set-up method-translator state

-      currentMethod = m;

-      loopHeapVarCount = 0;

-      otherTmpVarCount = 0;

-      _tmpIEs.Clear();

-

-      //  call inlined m;

-      TrStmt(m.Body, builder, localVariables, etran);

-

-      //  $Heap1 := $Heap;

-      Bpl.LocalVariable heap2 = new Bpl.LocalVariable(m.tok, new Bpl.TypedIdent(m.tok, heap.Name+"2", predef.HeapType));

-      localVariables.Add(heap2);

-      builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, heap2), etran.HeapExpr));

-

-      //  $Heap := old($Heap);

-      builder.Add(Bpl.Cmd.SimpleAssign(m.tok, heap, new Bpl.OldExpr(m.tok, heap)));

-

-      //  call inlined r;

-      currentMethod = r;

-      etran = new ExpressionTranslator(this, predef, heap);

-      TrStmt(r.Body, builder, localVariables, etran);

-

-      // clean method-translator state

-      currentMethod = null;

-      loopHeapVarCount = 0;

-      otherTmpVarCount = 0;

-      _tmpIEs.Clear();

-

-      // assert output variables of r and m are pairwise equal

-      Contract.Assert(outParams.Length % 2 == 0);

-      int k = outParams.Length / 2;

-      for (int i = 0; i < k; i++) {

-        Bpl.Variable rOut = outParams[i];

-        Bpl.Variable mOut = outParams[i+k];

-        Contract.Assert(rOut != null && mOut != null);

-        builder.Add(Assert(m.tok, Bpl.Expr.Eq(new Bpl.IdentifierExpr(m.tok, mOut), new Bpl.IdentifierExpr(m.tok, rOut)),

-          "Refinement method may not produce the same value for output variable " + m.Outs[i].Name));

-      }

-

-      // assert I($Heap1, $Heap)

-      builder.Add(Assert(m.tok, TrCouplingInvariant(m, heap, "this", new Bpl.IdentifierExpr(m.tok, heap2), that),

-        "Refinement method may not preserve the coupling invariant"));

-

-      Bpl.StmtList stmts = builder.Collect(m.tok);

-      Bpl.Implementation impl = new Bpl.Implementation(m.tok, proc.Name,

-        typeParams, inParams, outParams,

-        localVariables, stmts);

-      sink.TopLevelDeclarations.Add(impl);

-    }

-

-    private sealed class NominalSubstituter : Duplicator

-    {

-      private readonly Dictionary<string,Bpl.Expr> subst;

-      public NominalSubstituter(Dictionary<string,Bpl.Expr> subst) :base(){

-        Contract.Requires(cce.NonNullDictionaryAndValues(subst));

-        this.subst = subst;

-      }

-

-      [ContractInvariantMethod]

-      void ObjectInvariant() {

-        Contract.Invariant(cce.NonNullDictionaryAndValues(subst));

-      }

-

-

-      public override Expr VisitIdentifierExpr(Bpl.IdentifierExpr node)

-      {

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

-

-        if (node != null && subst.ContainsKey(node.Name))

-          return subst[node.Name];

-        else

-          return base.VisitIdentifierExpr(node);

-      }

-    }

-

-    Bpl.Expr TrCouplingInvariant(MethodRefinement m, Bpl.Expr absHeap, string absThis, Bpl.Expr conHeap, string conThis)

-     {

-      Contract.Requires(m != null);

-      Contract.Requires(absHeap != null);

-      Contract.Requires(absThis != null);

-      Contract.Requires(conHeap != null);

-      Contract.Requires(conThis != null);

-      Contract.Requires(predef != null);

-      Bpl.Expr cond = Bpl.Expr.True;

-      ClassRefinementDecl c = m.EnclosingClass as ClassRefinementDecl;

-      Contract.Assert(c != null);

-      ExpressionTranslator etran = new ExpressionTranslator(this, predef, conHeap, conThis);

-

-      foreach (MemberDecl d in c.Members)

-        if (d is CouplingInvariant) {

-          CouplingInvariant inv = (CouplingInvariant)d;

-

-          Contract.Assert(inv.Refined != null);

-          Contract.Assert(inv.Formals != null);

-

-          // replace formals with field dereferences

-          Dictionary<string,Bpl.Expr> map = new Dictionary<string,Bpl.Expr>();

-          Bpl.Expr absVar = new Bpl.IdentifierExpr(d.tok, absThis, predef.RefType);

-          for (int i = 0; i < inv.Refined.Count; i++) {

-            // TODO: boxing/unboxing?

-            Bpl.Expr result = ExpressionTranslator.ReadHeap(inv.Toks[i], absHeap, absVar, new Bpl.IdentifierExpr(inv.Toks[i], GetField(cce.NonNull(inv.Refined[i]))));

-            map.Add(inv.Formals[i].UniqueName, result);

-          }

-

-          Bpl.Expr e = new NominalSubstituter(map).VisitExpr(etran.TrExpr(inv.Expr));

-          cond = Bpl.Expr.And(cond, e);

-        }

-

-      return cond;

-    }

-

-    #endregion

-

     class BoilerplateTriple {  // a triple that is now a quintuple

       [ContractInvariantMethod]

       void ObjectInvariant() {

diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index 89974290..3811e2c0 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -31,7 +31,7 @@
 

    `(,(dafny-regexp-opt '(

         "class" "datatype" "type" "function" "ghost" "var" "method" "constructor" "unlimited"

-        "module" "imports" "static" "refines" "replaces" "by"

+        "module" "imports" "static" "refines"

         "returns" "requires" "ensures" "modifies" "reads" "free"

         "invariant" "decreases"

         )) . font-lock-builtin-face)

diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
index f2924420..e35383b0 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -18,7 +18,7 @@ namespace Demo
 

         this.MarkReservedWords(  // NOTE: these keywords must also appear once more below

           "class", "ghost", "static", "var", "method", "constructor", "datatype", "type",

-          "assert", "assume", "new", "this", "object", "refines", "replaces", "by",

+          "assert", "assume", "new", "this", "object", "refines",

           "unlimited", "module", "imports",

           "if", "then", "else", "while", "invariant",

           "break", "label", "return", "parallel", "havoc", "print",

@@ -274,8 +274,6 @@ namespace Demo
           | "this"

           | "object"

           | "refines"

-          | "replaces"

-          | "by"

           | "unlimited"

           | "module"

           | "imports"

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
index 23c71d45..78c5f8d9 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
@@ -239,7 +239,6 @@ namespace DafnyLanguage
                 case "assume":

                 case "bool":

                 case "break":

-                case "by":

                 case "case":

                 case "choose":

                 case "class":

@@ -276,7 +275,6 @@ namespace DafnyLanguage
                 case "print":

                 case "reads":

                 case "refines":

-                case "replaces":

                 case "requires":

                 case "result":

                 case "return":

diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index b829985a..28759fd4 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -7,7 +7,7 @@
 \lstdefinelanguage{dafny}{

   morekeywords={class,datatype,type,bool,nat,int,object,set,multiset,seq,array,array2,array3,%

       function,unlimited,

-      ghost,var,static,refines,replaces,by,

+      ghost,var,static,refines,

       method,constructor,returns,module,imports,in,

       requires,modifies,ensures,reads,decreases,free,

       % expressions

diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim
index ab8f120d..faac0cbb 100644
--- a/Util/vim/syntax/dafny.vim
+++ b/Util/vim/syntax/dafny.vim
@@ -10,7 +10,7 @@ syntax keyword dafnyTypeDef class datatype type
 syntax keyword dafnyConditional if then else match case 
 syntax keyword dafnyRepeat while parallel
 syntax keyword dafnyStatement havoc assume assert return new print break label
-syntax keyword dafnyKeyword var ghost returns null static this refines replaces by
+syntax keyword dafnyKeyword var ghost returns null static this refines
 syntax keyword dafnyType bool nat int seq set multiset object array array2 array3
 syntax keyword dafnyLogic requires ensures modifies reads decreases invariant 
 syntax keyword dafnyOperator forall exists old fresh allocated choose