Dafny:

* Beginning of module implementation
* Changed "class" modifier (for functions and methods) to "static"

18 files changed, 1237 insertions, 953 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 33a1d903..3ac46422 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -18,6 +18,7 @@ COMPILER Dafny
 

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

 

+static List<ModuleDecl!>! theModules = new List<ModuleDecl!>();

 static List<TopLevelDecl!>! theClasses = new List<TopLevelDecl!>();    

 

 

@@ -29,7 +30,7 @@ static int anonymousIds = 0;
 

 struct MemberModifiers {

   public bool IsGhost;

-  public bool IsClass;

+  public bool IsStatic;

   public bool IsUse;

 }

 

@@ -57,20 +58,20 @@ private static Expression! ConvertToLocal(Expression! e)
 }

 

 ///<summary>

-/// Parses top level declarations from "filename" and appends them to "classes".

+/// Parses top level declarations from "filename" and appends them to "modules" and "classes".

 /// Returns the number of parsing errors encountered.

 /// Note: first initialize the Scanner.

 ///</summary>

-public static int Parse (string! filename, List<TopLevelDecl!>! classes) /* throws System.IO.IOException */ {

+public static int Parse (string! filename, List<ModuleDecl!>! modules, List<TopLevelDecl!>! classes) /* throws System.IO.IOException */ {

   if (filename == "stdin.dfy") {

     BoogiePL.Buffer.Fill(System.Console.In);

     Scanner.Init(filename);

-    return Parse(classes);

+    return Parse(modules, classes);

   } else {

     using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {

       BoogiePL.Buffer.Fill(reader);

       Scanner.Init(filename);

-      return Parse(classes);

+      return Parse(modules, classes);

     }

   }

 }

@@ -80,10 +81,13 @@ public static int Parse (string! filename, List<TopLevelDecl!>! classes) /* thro
 /// Returns the number of parsing errors encountered.

 /// Note: first initialize the Scanner.

 ///</summary>

-public static int Parse (List<TopLevelDecl!>! classes) {

+public static int Parse (List<ModuleDecl!>! modules, List<TopLevelDecl!>! classes) {

+  List<ModuleDecl!> oldModules = theModules;

   List<TopLevelDecl!> oldClasses = theClasses;

+  theModules = modules;

   theClasses = classes;

   Parse();

+  theModules = oldModules;

   theClasses = oldClasses;

   return Errors.count;

 }

@@ -122,14 +126,27 @@ IGNORE cr + lf + tab
 PRODUCTIONS

 

 Dafny

-= (. ClassDecl! c; DatatypeDecl! dt; .)

-  { ClassDecl<out c>           (. theClasses.Add(c); .)

-  | DatatypeDecl<out dt>       (. theClasses.Add(dt); .)

+= (. ClassDecl! c; DatatypeDecl! dt;

+     ModuleDecl m;  Attributes attrs;  Token! id;  List<string!> theImports;

+  .)

+  { "module"                           (. attrs = null;  theImports = new List<string!>(); .)

+    { Attribute<ref attrs> }

+    Ident<out id>

+    [ "imports" Idents<theImports> ]   (. m = new ModuleDecl(id, id.val, theImports, attrs);

+                                          theModules.Add(m);

+                                       .)

+    "{"

+      { ClassDecl<m, out c>            (. theClasses.Add(c); .)

+      | DatatypeDecl<m, out dt>        (. theClasses.Add(dt); .)

+      }

+    "}"

+  | ClassDecl<null, out c>             (. theClasses.Add(c); .)

+  | DatatypeDecl<null, out dt>         (. theClasses.Add(dt); .)

   }

   EOF

   .

 

-ClassDecl<out ClassDecl! c>

+ClassDecl<ModuleDecl module, out ClassDecl! c>

 = (. Token! id;

      Attributes attrs = null;

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

@@ -142,7 +159,7 @@ ClassDecl<out ClassDecl! c>
   "{"

   { ClassMemberDecl<members>

   }

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

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

   .

 

 ClassMemberDecl<List<MemberDecl!\>! mm>

@@ -151,7 +168,7 @@ ClassMemberDecl<List<MemberDecl!\>! mm>
      MemberModifiers mmod = new MemberModifiers();

   .)

   { "ghost"                                (. mmod.IsGhost = true; .)

-  | "class"                                (. mmod.IsClass = true; .)

+  | "static"                               (. mmod.IsStatic = true; .)

   | "use"                                  (. mmod.IsUse = true; .)

   }

   ( FieldDecl<mmod, mm>

@@ -160,7 +177,7 @@ ClassMemberDecl<List<MemberDecl!\>! mm>
   )

   .

 

-DatatypeDecl<out DatatypeDecl! dt>

+DatatypeDecl<ModuleDecl module, out DatatypeDecl! dt>

 = (. Token! id;

      Attributes attrs = null;

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

@@ -173,7 +190,7 @@ DatatypeDecl<out DatatypeDecl! dt>
   "{"

   { DatatypeMemberDecl<ctors>

   }

-  "}"                                      (. dt = new DatatypeDecl(id, id.val, typeArgs, ctors, attrs); .)

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

   .

 

 DatatypeMemberDecl<List<DatatypeCtor!\>! ctors>

@@ -199,7 +216,7 @@ FieldDecl<MemberModifiers mmod, List<MemberDecl!\>! mm>
   .)

   "var"

   (. if (mmod.IsUse) { SemErr(token, "fields cannot be declared 'use'"); }

-     if (mmod.IsClass) { SemErr(token, "fields cannot be declared 'class'"); }

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

   .)

   { Attribute<ref attrs> }

   IdentType<out id, out ty>                         (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)

@@ -295,7 +312,7 @@ MethodDecl<MemberModifiers mmod, out Method! m>
   )

   

   (. parseVarScope.PopMarker();

-     m = new Method(id, id.val, mmod.IsClass, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);

+     m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);

   .)

   .

 

@@ -419,7 +436,7 @@ FunctionDecl<MemberModifiers mmod, out Function! f>
     FunctionBody<out bb>                (. body = bb; .)

   )

   (. parseVarScope.PopMarker();

-     f = new Function(id, id.val, mmod.IsClass, !isFunctionMethod, mmod.IsUse, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);

+     f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUse, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);

   .)

   .

 

@@ -1115,6 +1132,13 @@ AttributeOrTrigger<ref Attributes attrs, ref Triggers trigs>
 

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

 

+Idents<List<string!\>! ids>

+= (. Token! id; .)

+  Ident<out id>                            (. ids.Add(id.val); .)

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

+  }

+  .

+

 Ident<out Token! x>

 =

   ident            (. x = token; .)

diff --git a/Source/Dafny/DafnyAst.ssc b/Source/Dafny/DafnyAst.ssc
index 2a0fa32c..2e5bd893 100644
--- a/Source/Dafny/DafnyAst.ssc
+++ b/Source/Dafny/DafnyAst.ssc
@@ -12,9 +12,11 @@ namespace Microsoft.Dafny
 {

   public class Program {

     public readonly string! Name;

+    public readonly List<ModuleDecl!>! Modules;

     public readonly List<TopLevelDecl!>! Classes;

-    public Program(string! name, [Captured] List<TopLevelDecl!>! classes) {

+    public Program(string! name, [Captured] List<ModuleDecl!>! modules, [Captured] List<TopLevelDecl!>! classes) {

       Name = name;

+      Modules = modules;

       Classes = classes;

     }

   }

@@ -305,6 +307,11 @@ namespace Microsoft.Dafny
       this.Name = name;

       this.Attributes = attributes;

     }

+    

+    [Pure]

+    public override string! ToString() {

+      return Name;

+    }

   }

   

   public class TypeParameter : Declaration {

@@ -332,30 +339,40 @@ namespace Microsoft.Dafny
     }

   }

   

+  public class ModuleDecl : Declaration {

+    public readonly List<string!>! Imports;

+    public ModuleDecl(Token! tok, string! name, [Captured] List<string!>! imports, Attributes attributes) {

+      Imports = imports;

+      base(tok, name, attributes);

+    }

+  }

+    

   public abstract class TopLevelDecl : Declaration, TypeParameter.ParentType {

+    public readonly ModuleDecl Module;

     public readonly List<TypeParameter!>! TypeArgs;

     

-    public TopLevelDecl(Token! tok, string! name, List<TypeParameter!>! typeArgs, Attributes attributes) {

+    public TopLevelDecl(Token! tok, string! name, ModuleDecl module, List<TypeParameter!>! typeArgs, Attributes attributes) {

+      Module = module;

       TypeArgs = typeArgs;

       base(tok, name, attributes);

     }

   }

-  

+

   public class ClassDecl : TopLevelDecl {

     public readonly List<MemberDecl!>! Members;

 

-    public ClassDecl(Token! tok, string! name, List<TypeParameter!>! typeArgs, [Captured] List<MemberDecl!>! members, Attributes attributes) {

+    public ClassDecl(Token! tok, string! name, ModuleDecl module, List<TypeParameter!>! typeArgs, [Captured] List<MemberDecl!>! members, Attributes attributes) {

       Members = members;

-      base(tok, name, typeArgs, attributes);

+      base(tok, name, module, typeArgs, attributes);

     }

   }

   

   public class DatatypeDecl : TopLevelDecl {

     public readonly List<DatatypeCtor!>! Ctors;

     

-    public DatatypeDecl(Token! tok, string! name, List<TypeParameter!>! typeArgs, [Captured] List<DatatypeCtor!>! ctors, Attributes attributes) {

+    public DatatypeDecl(Token! tok, string! name, ModuleDecl module, List<TypeParameter!>! typeArgs, [Captured] List<DatatypeCtor!>! ctors, Attributes attributes) {

       Ctors = ctors;

-      base(tok, name, typeArgs, attributes);

+      base(tok, name, module, typeArgs, attributes);

     }

   }

   

@@ -473,7 +490,7 @@ namespace Microsoft.Dafny
   }

   

   public class Function : MemberDecl, TypeParameter.ParentType {

-    public readonly bool IsClass;

+    public readonly bool IsStatic;

     public readonly bool IsGhost;  // functions are "ghost" by default; a non-ghost function is called a "function method"

     public readonly bool IsUse;

     public readonly List<TypeParameter!>! TypeArgs;

@@ -484,9 +501,9 @@ namespace Microsoft.Dafny
     public readonly List<Expression!>! Decreases;

     public readonly Expression Body;  // an extended expression

     

-    public Function(Token! tok, string! name, bool isClass, bool isGhost, bool isUse, [Captured] List<TypeParameter!>! typeArgs, [Captured] List<Formal!>! formals, Type! resultType,

+    public Function(Token! tok, string! name, bool isStatic, bool isGhost, bool isUse, [Captured] List<TypeParameter!>! typeArgs, [Captured] List<Formal!>! formals, Type! resultType,

                     List<Expression!>! req, List<Expression!>! reads, List<Expression!>! decreases, Expression body, Attributes attributes) {

-      this.IsClass = isClass;

+      this.IsStatic = isStatic;

       this.IsGhost = isGhost;

       this.IsUse = isUse;

       this.TypeArgs = typeArgs;

@@ -501,7 +518,7 @@ namespace Microsoft.Dafny
   }

   

   public class Method : MemberDecl, TypeParameter.ParentType {

-    public readonly bool IsClass;

+    public readonly bool IsStatic;

     public readonly bool IsGhost;

     public readonly List<TypeParameter!>! TypeArgs;

     public readonly List<Formal!>! Ins;

@@ -513,14 +530,14 @@ namespace Microsoft.Dafny
     public readonly Statement Body;

     

     public Method(Token! tok, string! name,

-                  bool isClass, bool isGhost,

+                  bool isStatic, bool isGhost,

                   [Captured] List<TypeParameter!>! typeArgs,

                   [Captured] List<Formal!>! ins, [Captured] List<Formal!>! outs,

                   [Captured] List<MaybeFreeExpression!>! req, [Captured] List<Expression!>! mod, [Captured] List<MaybeFreeExpression!>! ens,

                   [Captured] List<Expression!>! decreases,

                   [Captured] Statement body,

                   Attributes attributes) {

-      this.IsClass = isClass;

+      this.IsStatic = isStatic;

       this.IsGhost = isGhost;

       this.TypeArgs = typeArgs;

       this.Ins = ins;

diff --git a/Source/Dafny/DafnyMain.ssc b/Source/Dafny/DafnyMain.ssc
index 2cccc08e..36ca4191 100644
--- a/Source/Dafny/DafnyMain.ssc
+++ b/Source/Dafny/DafnyMain.ssc
@@ -19,6 +19,7 @@ namespace Microsoft.Dafny {
     {

       program = null;

       Dafny.Errors.count = 0;

+      List<ModuleDecl!> modules = new List<ModuleDecl!>();

       List<TopLevelDecl!> classes = new List<TopLevelDecl!>();

       foreach (string! dafnyFileName in fileNames){

         if (Bpl.CommandLineOptions.Clo.XmlSink != null && Bpl.CommandLineOptions.Clo.XmlSink.IsOpen) {

@@ -32,7 +33,7 @@ namespace Microsoft.Dafny {
         int errorCount;

         try 

         {

-          errorCount = Dafny.Parser.Parse(dafnyFileName, classes);

+          errorCount = Dafny.Parser.Parse(dafnyFileName, modules, classes);

           if (errorCount != 0) 

           {

             return string.Format("{0} parse errors detected in {1}", Dafny.Errors.count, dafnyFileName);

@@ -44,7 +45,7 @@ namespace Microsoft.Dafny {
         }

       }

 

-      program = new Program(programName, classes);

+      program = new Program(programName, modules, classes);

 

       if (Bpl.CommandLineOptions.Clo.DafnyPrintFile != null) {

         string filename = Bpl.CommandLineOptions.Clo.DafnyPrintFile;

diff --git a/Source/Dafny/Parser.ssc b/Source/Dafny/Parser.ssc
index ca1eed51..b76182e4 100644
--- a/Source/Dafny/Parser.ssc
+++ b/Source/Dafny/Parser.ssc
@@ -6,7 +6,7 @@ using Microsoft.Contracts;
 namespace Microsoft.Dafny {

 

 public class Parser {

-	const int maxT = 93;

+	const int maxT = 96;

 

 	const bool T = true;

 	const bool x = false;

@@ -16,7 +16,8 @@ public class Parser {
 	static Token/*!*/ t;				// lookahead token

 	static int errDist = minErrDist;

 

-	static List<TopLevelDecl!>! theClasses = new List<TopLevelDecl!>();    

+	static List<ModuleDecl!>! theModules = new List<ModuleDecl!>();

+static List<TopLevelDecl!>! theClasses = new List<TopLevelDecl!>();    

 

 

 static Expression! dummyExpr = new LiteralExpr(Token.NoToken);

@@ -27,7 +28,7 @@ static int anonymousIds = 0;
 

 struct MemberModifiers {

   public bool IsGhost;

-  public bool IsClass;

+  public bool IsStatic;

   public bool IsUse;

 }

 

@@ -55,20 +56,20 @@ private static Expression! ConvertToLocal(Expression! e)
 }

 

 ///<summary>

-/// Parses top level declarations from "filename" and appends them to "classes".

+/// Parses top level declarations from "filename" and appends them to "modules" and "classes".

 /// Returns the number of parsing errors encountered.

 /// Note: first initialize the Scanner.

 ///</summary>

-public static int Parse (string! filename, List<TopLevelDecl!>! classes) /* throws System.IO.IOException */ {

+public static int Parse (string! filename, List<ModuleDecl!>! modules, List<TopLevelDecl!>! classes) /* throws System.IO.IOException */ {

   if (filename == "stdin.dfy") {

     BoogiePL.Buffer.Fill(System.Console.In);

     Scanner.Init(filename);

-    return Parse(classes);

+    return Parse(modules, classes);

   } else {

     using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {

       BoogiePL.Buffer.Fill(reader);

       Scanner.Init(filename);

-      return Parse(classes);

+      return Parse(modules, classes);

     }

   }

 }

@@ -78,10 +79,13 @@ public static int Parse (string! filename, List<TopLevelDecl!>! classes) /* thro
 /// Returns the number of parsing errors encountered.

 /// Note: first initialize the Scanner.

 ///</summary>

-public static int Parse (List<TopLevelDecl!>! classes) {

+public static int Parse (List<ModuleDecl!>! modules, List<TopLevelDecl!>! classes) {

+  List<ModuleDecl!> oldModules = theModules;

   List<TopLevelDecl!> oldClasses = theClasses;

+  theModules = modules;

   theClasses = classes;

   Parse();

+  theModules = oldModules;

   theClasses = oldClasses;

   return Errors.count;

 }

@@ -145,85 +149,123 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 	}

 	

 	static void Dafny() {

-		ClassDecl! c; DatatypeDecl! dt; 

-		while (t.kind == 4 || t.kind == 9) {

+		ClassDecl! c; DatatypeDecl! dt;

+		ModuleDecl m;  Attributes attrs;  Token! id;  List<string!> theImports;

+		

+		while (t.kind == 4 || t.kind == 8 || t.kind == 12) {

 			if (t.kind == 4) {

-				ClassDecl(out c);

+				Get();

+				attrs = null;  theImports = new List<string!>(); 

+				while (t.kind == 6) {

+					Attribute(ref attrs);

+				}

+				Ident(out id);

+				if (t.kind == 5) {

+					Get();

+					Idents(theImports);

+				}

+				m = new ModuleDecl(id, id.val, theImports, attrs);

+				theModules.Add(m);

+				

+				Expect(6);

+				while (t.kind == 8 || t.kind == 12) {

+					if (t.kind == 8) {

+						ClassDecl(m, out c);

+						theClasses.Add(c); 

+					} else {

+						DatatypeDecl(m, out dt);

+						theClasses.Add(dt); 

+					}

+				}

+				Expect(7);

+			} else if (t.kind == 8) {

+				ClassDecl(null, out c);

 				theClasses.Add(c); 

 			} else {

-				DatatypeDecl(out dt);

+				DatatypeDecl(null, out dt);

 				theClasses.Add(dt); 

 			}

 		}

 		Expect(0);

 	}

 

-	static void ClassDecl(out ClassDecl! c) {

+	static void Attribute(ref Attributes attrs) {

+		Expect(6);

+		AttributeBody(ref attrs);

+		Expect(7);

+	}

+

+	static void Ident(out Token! x) {

+		Expect(1);

+		x = token; 

+	}

+

+	static void Idents(List<string!>! ids) {

+		Token! id; 

+		Ident(out id);

+		ids.Add(id.val); 

+		while (t.kind == 15) {

+			Get();

+			Ident(out id);

+			ids.Add(id.val); 

+		}

+	}

+

+	static void ClassDecl(ModuleDecl module, out ClassDecl! c) {

 		Token! id;

 		Attributes attrs = null;

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

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

 		

-		Expect(4);

-		while (t.kind == 5) {

+		Expect(8);

+		while (t.kind == 6) {

 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (t.kind == 14) {

+		if (t.kind == 17) {

 			GenericParameters(typeArgs);

 		}

-		Expect(5);

+		Expect(6);

 		while (StartOf(1)) {

 			ClassMemberDecl(members);

 		}

-		Expect(6);

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

+		Expect(7);

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

 	}

 

-	static void DatatypeDecl(out DatatypeDecl! dt) {

+	static void DatatypeDecl(ModuleDecl module, out DatatypeDecl! dt) {

 		Token! id;

 		Attributes attrs = null;

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

 		List<DatatypeCtor!> ctors = new List<DatatypeCtor!>();

 		

-		Expect(9);

-		while (t.kind == 5) {

+		Expect(12);

+		while (t.kind == 6) {

 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (t.kind == 14) {

+		if (t.kind == 17) {

 			GenericParameters(typeArgs);

 		}

-		Expect(5);

-		while (t.kind == 1 || t.kind == 5) {

+		Expect(6);

+		while (t.kind == 1 || t.kind == 6) {

 			DatatypeMemberDecl(ctors);

 		}

-		Expect(6);

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

-	}

-

-	static void Attribute(ref Attributes attrs) {

-		Expect(5);

-		AttributeBody(ref attrs);

-		Expect(6);

-	}

-

-	static void Ident(out Token! x) {

-		Expect(1);

-		x = token; 

+		Expect(7);

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

 	}

 

 	static void GenericParameters(List<TypeParameter!>! typeArgs) {

 		Token! id; 

-		Expect(14);

+		Expect(17);

 		Ident(out id);

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

-		while (t.kind == 12) {

+		while (t.kind == 15) {

 			Get();

 			Ident(out id);

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

 		}

-		Expect(15);

+		Expect(18);

 	}

 

 	static void ClassMemberDecl(List<MemberDecl!>! mm) {

@@ -231,48 +273,48 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		Function! f;

 		MemberModifiers mmod = new MemberModifiers();

 		

-		while (t.kind == 4 || t.kind == 7 || t.kind == 8) {

-			if (t.kind == 7) {

+		while (t.kind == 9 || t.kind == 10 || t.kind == 11) {

+			if (t.kind == 9) {

 				Get();

 				mmod.IsGhost = true; 

-			} else if (t.kind == 4) {

+			} else if (t.kind == 10) {

 				Get();

-				mmod.IsClass = true; 

+				mmod.IsStatic = true; 

 			} else {

 				Get();

 				mmod.IsUse = true; 

 			}

 		}

-		if (t.kind == 11) {

+		if (t.kind == 14) {

 			FieldDecl(mmod, mm);

-		} else if (t.kind == 30) {

+		} else if (t.kind == 33) {

 			FunctionDecl(mmod, out f);

 			mm.Add(f); 

-		} else if (t.kind == 16) {

+		} else if (t.kind == 19) {

 			MethodDecl(mmod, out m);

 			mm.Add(m); 

-		} else Error(94);

+		} else Error(97);

 	}

 

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

 		Attributes attrs = null;

 		Token! id;  Type! ty;

 		

-		Expect(11);

+		Expect(14);

 		if (mmod.IsUse) { SemErr(token, "fields cannot be declared 'use'"); }

-		if (mmod.IsClass) { SemErr(token, "fields cannot be declared 'class'"); }

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

 		

-		while (t.kind == 5) {

+		while (t.kind == 6) {

 			Attribute(ref attrs);

 		}

 		IdentType(out id, out ty);

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

-		while (t.kind == 12) {

+		while (t.kind == 15) {

 			Get();

 			IdentType(out id, out ty);

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

 		}

-		Expect(10);

+		Expect(13);

 	}

 

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

@@ -287,38 +329,38 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		Expression! bb;  Expression body = null;

 		bool isFunctionMethod = false;

 		

-		Expect(30);

-		if (t.kind == 16) {

+		Expect(33);

+		if (t.kind == 19) {

 			Get();

 			isFunctionMethod = true; 

 		}

 		if (mmod.IsGhost) { SemErr(token, "functions cannot be declared 'ghost' (they are ghost by default)"); }

 		

-		while (t.kind == 5) {

+		while (t.kind == 6) {

 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (t.kind == 14) {

+		if (t.kind == 17) {

 			GenericParameters(typeArgs);

 		}

 		parseVarScope.PushMarker(); 

 		Formals(true, false, formals);

-		Expect(13);

+		Expect(16);

 		Type(out returnType);

-		if (t.kind == 10) {

+		if (t.kind == 13) {

 			Get();

-			while (t.kind == 20 || t.kind == 22 || t.kind == 31) {

+			while (t.kind == 23 || t.kind == 25 || t.kind == 34) {

 				FunctionSpec(reqs, reads, decreases);

 			}

 		} else if (StartOf(2)) {

-			while (t.kind == 20 || t.kind == 22 || t.kind == 31) {

+			while (t.kind == 23 || t.kind == 25 || t.kind == 34) {

 				FunctionSpec(reqs, reads, decreases);

 			}

 			FunctionBody(out bb);

 			body = bb; 

-		} else Error(95);

+		} else Error(98);

 		parseVarScope.PopMarker();

-		f = new Function(id, id.val, mmod.IsClass, !isFunctionMethod, mmod.IsUse, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);

+		f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUse, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);

 		

 	}

 

@@ -334,23 +376,23 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		List<Expression!> dec = new List<Expression!>();

 		Statement! bb;  Statement body = null;

 		

-		Expect(16);

+		Expect(19);

 		if (mmod.IsUse) { SemErr(token, "methods cannot be declared 'use'"); }

 		

-		while (t.kind == 5) {

+		while (t.kind == 6) {

 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (t.kind == 14) {

+		if (t.kind == 17) {

 			GenericParameters(typeArgs);

 		}

 		parseVarScope.PushMarker(); 

 		Formals(true, true, ins);

-		if (t.kind == 17) {

+		if (t.kind == 20) {

 			Get();

 			Formals(false, true, outs);

 		}

-		if (t.kind == 10) {

+		if (t.kind == 13) {

 			Get();

 			while (StartOf(3)) {

 				MethodSpec(req, mod, ens, dec);

@@ -361,9 +403,9 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			}

 			BlockStmt(out bb);

 			body = bb; 

-		} else Error(96);

+		} else Error(99);

 		parseVarScope.PopMarker();

-		m = new Method(id, id.val, mmod.IsClass, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);

+		m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);

 		

 	}

 

@@ -373,47 +415,47 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		List<TypeParameter!> typeArgs = new List<TypeParameter!>();

 		List<Formal!> formals = new List<Formal!>();

 		

-		while (t.kind == 5) {

+		while (t.kind == 6) {

 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (t.kind == 14) {

+		if (t.kind == 17) {

 			GenericParameters(typeArgs);

 		}

 		parseVarScope.PushMarker(); 

-		if (t.kind == 23) {

+		if (t.kind == 26) {

 			FormalsOptionalIds(formals);

 		}

 		parseVarScope.PopMarker();

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

 		

-		Expect(10);

+		Expect(13);

 	}

 

 	static void FormalsOptionalIds(List<Formal!>! formals) {

 		Token! id;  Type! ty;  string! name; 

-		Expect(23);

+		Expect(26);

 		if (StartOf(5)) {

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

 			formals.Add(new Formal(id, name, ty, true, false));  parseVarScope.Push(name, name); 

-			while (t.kind == 12) {

+			while (t.kind == 15) {

 				Get();

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

 				formals.Add(new Formal(id, name, ty, true, false));  parseVarScope.Push(name, name); 

 			}

 		}

-		Expect(24);

+		Expect(27);

 	}

 

 	static void IdentType(out Token! id, out Type! ty) {

 		Ident(out id);

-		Expect(13);

+		Expect(16);

 		Type(out ty);

 	}

 

 	static void GIdentType(bool allowGhost, out Token! id, out Type! ty, out bool isGhost) {

 		isGhost = false; 

-		if (t.kind == 7) {

+		if (t.kind == 9) {

 			Get();

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

 		}

@@ -429,7 +471,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		Token! id;  Type! ty;  Type optType = null;

 		

 		Ident(out id);

-		if (t.kind == 13) {

+		if (t.kind == 16) {

 			Get();

 			Type(out ty);

 			optType = ty; 

@@ -440,7 +482,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 	static void TypeIdentOptional(out Token! id, out string! identName, out Type! ty) {

 		string name = null; 

 		TypeAndToken(out id, out ty);

-		if (t.kind == 13) {

+		if (t.kind == 16) {

 			Get();

 			UserDefinedType udt = ty as UserDefinedType;

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

@@ -463,13 +505,13 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

 		List<Type!>! gt;

 		

-		if (t.kind == 25) {

+		if (t.kind == 28) {

 			Get();

 			tok = token; 

-		} else if (t.kind == 26) {

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

 			Get();

 			tok = token;  ty = new IntType(); 

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

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

 			Get();

 			tok = token;  gt = new List<Type!>(); 

 			GenericInstantiation(gt);

@@ -478,7 +520,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			}

 			ty = new SetType(gt[0]);

 			

-		} else if (t.kind == 28) {

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

 			Get();

 			tok = token;  gt = new List<Type!>(); 

 			GenericInstantiation(gt);

@@ -487,63 +529,63 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			}

 			ty = new SeqType(gt[0]);

 			

-		} else if (t.kind == 1 || t.kind == 29) {

+		} else if (t.kind == 1 || t.kind == 32) {

 			ReferenceType(out tok, out ty);

-		} else Error(97);

+		} else Error(100);

 	}

 

 	static void Formals(bool incoming, bool allowGhosts, List<Formal!>! formals) {

 		Token! id;  Type! ty;  bool isGhost; 

-		Expect(23);

-		if (t.kind == 1 || t.kind == 7) {

+		Expect(26);

+		if (t.kind == 1 || t.kind == 9) {

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

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

-			while (t.kind == 12) {

+			while (t.kind == 15) {

 				Get();

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

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

 			}

 		}

-		Expect(24);

+		Expect(27);

 	}

 

 	static void MethodSpec(List<MaybeFreeExpression!>! req, List<Expression!>! mod, List<MaybeFreeExpression!>! ens,

 List<Expression!>! decreases) {

 		Expression! e;  bool isFree = false;

 		

-		if (t.kind == 18) {

+		if (t.kind == 21) {

 			Get();

 			if (StartOf(6)) {

 				Expression(out e);

 				mod.Add(e); 

-				while (t.kind == 12) {

+				while (t.kind == 15) {

 					Get();

 					Expression(out e);

 					mod.Add(e); 

 				}

 			}

-			Expect(10);

-		} else if (t.kind == 19 || t.kind == 20 || t.kind == 21) {

-			if (t.kind == 19) {

+			Expect(13);

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

+			if (t.kind == 22) {

 				Get();

 				isFree = true; 

 			}

-			if (t.kind == 20) {

+			if (t.kind == 23) {

 				Get();

 				Expression(out e);

-				Expect(10);

+				Expect(13);

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

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

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

 				Get();

 				Expression(out e);

-				Expect(10);

+				Expect(13);

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

-			} else Error(98);

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

+			} else Error(101);

+		} else if (t.kind == 25) {

 			Get();

 			PossiblyWildExpressions(decreases);

-			Expect(10);

-		} else Error(99);

+			Expect(13);

+		} else Error(102);

 	}

 

 	static void BlockStmt(out Statement! block) {

@@ -552,12 +594,12 @@ List<Expression!>! decreases) {
 		Statement! s;

 		

 		parseVarScope.PushMarker(); 

-		Expect(5);

+		Expect(6);

 		x = token; 

 		while (StartOf(7)) {

 			Stmt(body);

 		}

-		Expect(6);

+		Expect(7);

 		block = new BlockStmt(x, body); 

 		parseVarScope.PopMarker(); 

 	}

@@ -566,25 +608,25 @@ List<Expression!>! decreases) {
 		Token! x;  Expression! e0;  Expression! e1 = dummyExpr;

 		e = dummyExpr;

 		

-		if (t.kind == 42) {

+		if (t.kind == 45) {

 			Get();

 			x = token; 

 			Expression(out e);

-			Expect(52);

+			Expect(55);

 			Expression(out e0);

-			Expect(43);

+			Expect(46);

 			Expression(out e1);

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

 		} else if (StartOf(8)) {

 			EquivExpression(out e);

-		} else Error(100);

+		} else Error(103);

 	}

 

 	static void PossiblyWildExpressions(List<Expression!>! args) {

 		Expression! e; 

 		PossiblyWildExpression(out e);

 		args.Add(e); 

-		while (t.kind == 12) {

+		while (t.kind == 15) {

 			Get();

 			PossiblyWildExpression(out e);

 			args.Add(e); 

@@ -593,70 +635,70 @@ List<Expression!>! decreases) {
 

 	static void GenericInstantiation(List<Type!>! gt) {

 		Type! ty; 

-		Expect(14);

+		Expect(17);

 		Type(out ty);

 		gt.Add(ty); 

-		while (t.kind == 12) {

+		while (t.kind == 15) {

 			Get();

 			Type(out ty);

 			gt.Add(ty); 

 		}

-		Expect(15);

+		Expect(18);

 	}

 

 	static void ReferenceType(out Token! tok, out Type! ty) {

 		tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

 		List<Type!>! gt;

 		

-		if (t.kind == 29) {

+		if (t.kind == 32) {

 			Get();

 			tok = token;  ty = new ObjectType(); 

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

 			Ident(out tok);

 			gt = new List<Type!>(); 

-			if (t.kind == 14) {

+			if (t.kind == 17) {

 				GenericInstantiation(gt);

 			}

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

-		} else Error(101);

+		} else Error(104);

 	}

 

 	static void FunctionSpec(List<Expression!>! reqs, List<Expression!>! reads, List<Expression!>! decreases) {

 		Expression! e; 

-		if (t.kind == 20) {

+		if (t.kind == 23) {

 			Get();

 			Expression(out e);

-			Expect(10);

+			Expect(13);

 			reqs.Add(e); 

-		} else if (t.kind == 31) {

+		} else if (t.kind == 34) {

 			Get();

 			if (StartOf(9)) {

 				PossiblyWildExpressions(reads);

 			}

-			Expect(10);

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

+			Expect(13);

+		} else if (t.kind == 25) {

 			Get();

 			Expressions(decreases);

-			Expect(10);

-		} else Error(102);

+			Expect(13);

+		} else Error(105);

 	}

 

 	static void FunctionBody(out Expression! e) {

 		e = dummyExpr; 

-		Expect(5);

-		if (t.kind == 33) {

+		Expect(6);

+		if (t.kind == 36) {

 			MatchExpression(out e);

 		} else if (StartOf(6)) {

 			Expression(out e);

-		} else Error(103);

-		Expect(6);

+		} else Error(106);

+		Expect(7);

 	}

 

 	static void Expressions(List<Expression!>! args) {

 		Expression! e; 

 		Expression(out e);

 		args.Add(e); 

-		while (t.kind == 12) {

+		while (t.kind == 15) {

 			Get();

 			Expression(out e);

 			args.Add(e); 

@@ -665,34 +707,34 @@ List<Expression!>! decreases) {
 

 	static void PossiblyWildExpression(out Expression! e) {

 		e = dummyExpr; 

-		if (t.kind == 32) {

+		if (t.kind == 35) {

 			Get();

 			e = new WildcardExpr(token); 

 		} else if (StartOf(6)) {

 			Expression(out e);

-		} else Error(104);

+		} else Error(107);

 	}

 

 	static void MatchExpression(out Expression! e) {

 		Token! x;

 		List<MatchCase!> cases = new List<MatchCase!>();

 		

-		Expect(33);

+		Expect(36);

 		x = token; 

 		Expression(out e);

-		if (t.kind == 5) {

+		if (t.kind == 6) {

 			Get();

 			CaseExpressions(cases);

-			Expect(6);

-		} else if (t.kind == 6 || t.kind == 34) {

+			Expect(7);

+		} else if (t.kind == 7 || t.kind == 37) {

 			CaseExpressions(cases);

-		} else Error(105);

+		} else Error(108);

 		e = new MatchExpr(x, e, cases); 

 	}

 

 	static void CaseExpressions(List<MatchCase!>! cases) {

 		MatchCase! c; 

-		while (t.kind == 34) {

+		while (t.kind == 37) {

 			CaseExpression(out c);

 			cases.Add(c); 

 		}

@@ -703,23 +745,23 @@ List<Expression!>! decreases) {
 		List<BoundVar!> arguments = new List<BoundVar!>();

 		Expression! body;

 		

-		Expect(34);

+		Expect(37);

 		x = token;  parseVarScope.PushMarker(); 

 		Ident(out id);

-		if (t.kind == 23) {

+		if (t.kind == 26) {

 			Get();

 			Ident(out arg);

 			arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));

 			parseVarScope.Push(arg.val, arg.val); 

-			while (t.kind == 12) {

+			while (t.kind == 15) {

 				Get();

 				Ident(out arg);

 				arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));

 				parseVarScope.Push(arg.val, arg.val); 

 			}

-			Expect(24);

+			Expect(27);

 		}

-		Expect(35);

+		Expect(38);

 		Expression(out body);

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

 		parseVarScope.PopMarker(); 

@@ -727,16 +769,16 @@ List<Expression!>! decreases) {
 

 	static void Stmt(List<Statement!>! ss) {

 		Statement! s; 

-		while (t.kind == 5) {

+		while (t.kind == 6) {

 			BlockStmt(out s);

 			ss.Add(s); 

 		}

 		if (StartOf(10)) {

 			OneStmt(out s);

 			ss.Add(s); 

-		} else if (t.kind == 7 || t.kind == 11) {

+		} else if (t.kind == 9 || t.kind == 14) {

 			VarDeclStmts(ss);

-		} else Error(106);

+		} else Error(109);

 	}

 

 	static void OneStmt(out Statement! s) {

@@ -744,113 +786,113 @@ List<Expression!>! decreases) {
 		s = dummyStmt;  /* to please the compiler */

 		

 		switch (t.kind) {

-		case 50: {

+		case 53: {

 			AssertStmt(out s);

 			break;

 		}

-		case 51: {

+		case 54: {

 			AssumeStmt(out s);

 			break;

 		}

-		case 8: {

+		case 11: {

 			UseStmt(out s);

 			break;

 		}

-		case 1: case 23: case 85: case 86: {

+		case 1: case 26: case 88: case 89: {

 			AssignStmt(out s);

 			break;

 		}

-		case 41: {

+		case 44: {

 			HavocStmt(out s);

 			break;

 		}

-		case 46: {

+		case 49: {

 			CallStmt(out s);

 			break;

 		}

-		case 42: {

+		case 45: {

 			IfStmt(out s);

 			break;

 		}

-		case 44: {

+		case 47: {

 			WhileStmt(out s);

 			break;

 		}

-		case 47: {

+		case 50: {

 			ForeachStmt(out s);

 			break;

 		}

-		case 36: {

+		case 39: {

 			Get();

 			x = token; 

 			Ident(out id);

-			Expect(13);

+			Expect(16);

 			s = new LabelStmt(x, id.val); 

 			break;

 		}

-		case 37: {

+		case 40: {

 			Get();

 			x = token; 

 			if (t.kind == 1) {

 				Ident(out id);

 				label = id.val; 

 			}

-			Expect(10);

+			Expect(13);

 			s = new BreakStmt(x, label); 

 			break;

 		}

-		case 38: {

+		case 41: {

 			Get();

 			x = token; 

-			Expect(10);

+			Expect(13);

 			s = new ReturnStmt(x); 

 			break;

 		}

-		default: Error(107); break;

+		default: Error(110); break;

 		}

 	}

 

 	static void VarDeclStmts(List<Statement!>! ss) {

 		VarDecl! d;  bool isGhost = false; 

-		if (t.kind == 7) {

+		if (t.kind == 9) {

 			Get();

 			isGhost = true; 

 		}

-		Expect(11);

+		Expect(14);

 		IdentTypeRhs(out d, isGhost);

 		ss.Add(d);  parseVarScope.Push(d.Name, d.Name); 

-		while (t.kind == 12) {

+		while (t.kind == 15) {

 			Get();

 			IdentTypeRhs(out d, isGhost);

 			ss.Add(d);  parseVarScope.Push(d.Name, d.Name); 

 		}

-		Expect(10);

+		Expect(13);

 	}

 

 	static void AssertStmt(out Statement! s) {

 		Token! x;  Expression! e; 

-		Expect(50);

+		Expect(53);

 		x = token; 

 		Expression(out e);

-		Expect(10);

+		Expect(13);

 		s = new AssertStmt(x, e); 

 	}

 

 	static void AssumeStmt(out Statement! s) {

 		Token! x;  Expression! e; 

-		Expect(51);

+		Expect(54);

 		x = token; 

 		Expression(out e);

-		Expect(10);

+		Expect(13);

 		s = new AssumeStmt(x, e); 

 	}

 

 	static void UseStmt(out Statement! s) {

 		Token! x;  Expression! e; 

-		Expect(8);

+		Expect(11);

 		x = token; 

 		Expression(out e);

-		Expect(10);

+		Expect(13);

 		s = new UseStmt(x, e); 

 	}

 

@@ -862,7 +904,7 @@ List<Expression!>! decreases) {
 		s = dummyStmt;

 		

 		LhsExpr(out lhs);

-		Expect(39);

+		Expect(42);

 		x = token; 

 		AssignRhs(out rhs, out ty);

 		if (rhs != null) {

@@ -872,15 +914,15 @@ List<Expression!>! decreases) {
 		  s = new AssignStmt(x, lhs, ty);

 		}

 		

-		Expect(10);

+		Expect(13);

 	}

 

 	static void HavocStmt(out Statement! s) {

 		Token! x;  Expression! lhs; 

-		Expect(41);

+		Expect(44);

 		x = token; 

 		LhsExpr(out lhs);

-		Expect(10);

+		Expect(13);

 		s = new AssignStmt(x, lhs); 

 	}

 

@@ -890,11 +932,11 @@ List<Expression!>! decreases) {
 		List<IdentifierExpr!> lhs = new List<IdentifierExpr!>();

 		List<AutoVarDecl!> newVars = new List<AutoVarDecl!>();

 		

-		Expect(46);

+		Expect(49);

 		x = token; 

 		CallStmtSubExpr(out e);

-		if (t.kind == 12 || t.kind == 39) {

-			if (t.kind == 12) {

+		if (t.kind == 15 || t.kind == 42) {

+			if (t.kind == 15) {

 				Get();

 				e = ConvertToLocal(e);

 				if (e is IdentifierExpr) {

@@ -907,12 +949,12 @@ List<Expression!>! decreases) {
 				

 				Ident(out id);

 				RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars); 

-				while (t.kind == 12) {

+				while (t.kind == 15) {

 					Get();

 					Ident(out id);

 					RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars); 

 				}

-				Expect(39);

+				Expect(42);

 				CallStmtSubExpr(out e);

 			} else {

 				Get();

@@ -928,7 +970,7 @@ List<Expression!>! decreases) {
 				CallStmtSubExpr(out e);

 			}

 		}

-		Expect(10);

+		Expect(13);

 		if (e is FunctionCallExpr) {

 		 FunctionCallExpr fce = (FunctionCallExpr)e;

 		 s = new CallStmt(x, newVars, lhs, fce.Receiver, fce.Name, fce.Args);  // this actually does an ownership transfer of fce.Args

@@ -946,19 +988,19 @@ List<Expression!>! decreases) {
 		Statement! s;

 		Statement els = null;

 		

-		Expect(42);

+		Expect(45);

 		x = token; 

 		Guard(out guard);

 		BlockStmt(out thn);

-		if (t.kind == 43) {

+		if (t.kind == 46) {

 			Get();

-			if (t.kind == 42) {

+			if (t.kind == 45) {

 				IfStmt(out s);

 				els = s; 

-			} else if (t.kind == 5) {

+			} else if (t.kind == 6) {

 				BlockStmt(out s);

 				els = s; 

-			} else Error(108);

+			} else Error(111);

 		}

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

 	}

@@ -971,25 +1013,25 @@ List<Expression!>! decreases) {
 		List<Expression!> decreases = new List<Expression!>();

 		Statement! body;

 		

-		Expect(44);

+		Expect(47);

 		x = token; 

 		Guard(out guard);

 		assume guard == null || Owner.None(guard); 

-		while (t.kind == 19 || t.kind == 22 || t.kind == 45) {

-			if (t.kind == 19 || t.kind == 45) {

+		while (t.kind == 22 || t.kind == 25 || t.kind == 48) {

+			if (t.kind == 22 || t.kind == 48) {

 				isFree = false; 

-				if (t.kind == 19) {

+				if (t.kind == 22) {

 					Get();

 					isFree = true; 

 				}

-				Expect(45);

+				Expect(48);

 				Expression(out e);

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

-				Expect(10);

+				Expect(13);

 			} else {

 				Get();

 				PossiblyWildExpressions(decreases);

-				Expect(10);

+				Expect(13);

 			}

 		}

 		BlockStmt(out body);

@@ -1005,31 +1047,31 @@ List<Expression!>! decreases) {
 		AssignStmt bodyAssign = null;

 		

 		parseVarScope.PushMarker(); 

-		Expect(47);

+		Expect(50);

 		x = token;

 		range = new LiteralExpr(x, true);

 		ty = new InferredTypeProxy();

 		

-		Expect(23);

+		Expect(26);

 		Ident(out boundVar);

-		if (t.kind == 13) {

+		if (t.kind == 16) {

 			Get();

 			Type(out ty);

 		}

-		Expect(48);

+		Expect(51);

 		Expression(out collection);

 		parseVarScope.Push(boundVar.val, boundVar.val); 

-		if (t.kind == 49) {

+		if (t.kind == 52) {

 			Get();

 			Expression(out range);

 		}

-		Expect(24);

-		Expect(5);

-		while (t.kind == 8 || t.kind == 50 || t.kind == 51) {

-			if (t.kind == 50) {

+		Expect(27);

+		Expect(6);

+		while (t.kind == 11 || t.kind == 53 || t.kind == 54) {

+			if (t.kind == 53) {

 				AssertStmt(out s);

 				if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } 

-			} else if (t.kind == 51) {

+			} else if (t.kind == 54) {

 				AssumeStmt(out s);

 				if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } 

 			} else {

@@ -1040,11 +1082,11 @@ List<Expression!>! decreases) {
 		if (StartOf(11)) {

 			AssignStmt(out s);

 			if (s is AssignStmt) { bodyAssign = (AssignStmt)s; } 

-		} else if (t.kind == 41) {

+		} else if (t.kind == 44) {

 			HavocStmt(out s);

 			if (s is AssignStmt) { bodyAssign = (AssignStmt)s; } 

-		} else Error(109);

-		Expect(6);

+		} else Error(112);

+		Expect(7);

 		if (bodyAssign != null) {

 		 s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);

 		} else {

@@ -1062,14 +1104,14 @@ List<Expression!>! decreases) {
 		Token! x;  Expression! ee;  Type! tt;

 		e = null;  ty = null;

 		

-		if (t.kind == 40) {

+		if (t.kind == 43) {

 			Get();

 			ReferenceType(out x, out tt);

 			ty = tt; 

 		} else if (StartOf(6)) {

 			Expression(out ee);

 			e = ee; 

-		} else Error(110);

+		} else Error(113);

 		if (e == null && ty == null) { e = dummyExpr; } 

 	}

 

@@ -1077,10 +1119,10 @@ List<Expression!>! decreases) {
 		Token! id;  e = dummyExpr; 

 		if (t.kind == 1) {

 			IdentOrFuncExpression(out e);

-		} else if (t.kind == 23 || t.kind == 85 || t.kind == 86) {

+		} else if (t.kind == 26 || t.kind == 88 || t.kind == 89) {

 			ObjectExpression(out e);

-		} else Error(111);

-		while (t.kind == 80 || t.kind == 82) {

+		} else Error(114);

+		while (t.kind == 83 || t.kind == 85) {

 			SelectOrCallSuffix(ref e);

 		}

 	}

@@ -1091,12 +1133,12 @@ List<Expression!>! decreases) {
 		Type optionalType = null;  DeterminedAssignmentRhs optionalRhs = null;

 		

 		Ident(out id);

-		if (t.kind == 13) {

+		if (t.kind == 16) {

 			Get();

 			Type(out ty);

 			optionalType = ty; 

 		}

-		if (t.kind == 39) {

+		if (t.kind == 42) {

 			Get();

 			AssignRhs(out rhs, out newType);

 		}

@@ -1114,26 +1156,26 @@ List<Expression!>! decreases) {
 

 	static void Guard(out Expression e) {

 		Expression! ee;  e = null; 

-		Expect(23);

-		if (t.kind == 32) {

+		Expect(26);

+		if (t.kind == 35) {

 			Get();

 			e = null; 

 		} else if (StartOf(6)) {

 			Expression(out ee);

 			e = ee; 

-		} else Error(112);

-		Expect(24);

+		} else Error(115);

+		Expect(27);

 	}

 

 	static void CallStmtSubExpr(out Expression! e) {

 		e = dummyExpr; 

 		if (t.kind == 1) {

 			IdentOrFuncExpression(out e);

-		} else if (t.kind == 23 || t.kind == 85 || t.kind == 86) {

+		} else if (t.kind == 26 || t.kind == 88 || t.kind == 89) {

 			ObjectExpression(out e);

 			SelectOrCallSuffix(ref e);

-		} else Error(113);

-		while (t.kind == 80 || t.kind == 82) {

+		} else Error(116);

+		while (t.kind == 83 || t.kind == 85) {

 			SelectOrCallSuffix(ref e);

 		}

 	}

@@ -1141,7 +1183,7 @@ List<Expression!>! decreases) {
 	static void EquivExpression(out Expression! e0) {

 		Token! x;  Expression! e1; 

 		ImpliesExpression(out e0);

-		while (t.kind == 53 || t.kind == 54) {

+		while (t.kind == 56 || t.kind == 57) {

 			EquivOp();

 			x = token; 

 			ImpliesExpression(out e1);

@@ -1152,7 +1194,7 @@ List<Expression!>! decreases) {
 	static void ImpliesExpression(out Expression! e0) {

 		Token! x;  Expression! e1; 

 		LogicalExpression(out e0);

-		if (t.kind == 55 || t.kind == 56) {

+		if (t.kind == 58 || t.kind == 59) {

 			ImpliesOp();

 			x = token; 

 			ImpliesExpression(out e1);

@@ -1161,23 +1203,23 @@ List<Expression!>! decreases) {
 	}

 

 	static void EquivOp() {

-		if (t.kind == 53) {

+		if (t.kind == 56) {

 			Get();

-		} else if (t.kind == 54) {

+		} else if (t.kind == 57) {

 			Get();

-		} else Error(114);

+		} else Error(117);

 	}

 

 	static void LogicalExpression(out Expression! e0) {

 		Token! x;  Expression! e1; 

 		RelationalExpression(out e0);

 		if (StartOf(12)) {

-			if (t.kind == 57 || t.kind == 58) {

+			if (t.kind == 60 || t.kind == 61) {

 				AndOp();

 				x = token; 

 				RelationalExpression(out e1);

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

-				while (t.kind == 57 || t.kind == 58) {

+				while (t.kind == 60 || t.kind == 61) {

 					AndOp();

 					x = token; 

 					RelationalExpression(out e1);

@@ -1188,7 +1230,7 @@ List<Expression!>! decreases) {
 				x = token; 

 				RelationalExpression(out e1);

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

-				while (t.kind == 59 || t.kind == 60) {

+				while (t.kind == 62 || t.kind == 63) {

 					OrOp();

 					x = token; 

 					RelationalExpression(out e1);

@@ -1199,11 +1241,11 @@ List<Expression!>! decreases) {
 	}

 

 	static void ImpliesOp() {

-		if (t.kind == 55) {

+		if (t.kind == 58) {

 			Get();

-		} else if (t.kind == 56) {

+		} else if (t.kind == 59) {

 			Get();

-		} else Error(115);

+		} else Error(118);

 	}

 

 	static void RelationalExpression(out Expression! e0) {

@@ -1217,25 +1259,25 @@ List<Expression!>! decreases) {
 	}

 

 	static void AndOp() {

-		if (t.kind == 57) {

+		if (t.kind == 60) {

 			Get();

-		} else if (t.kind == 58) {

+		} else if (t.kind == 61) {

 			Get();

-		} else Error(116);

+		} else Error(119);

 	}

 

 	static void OrOp() {

-		if (t.kind == 59) {

+		if (t.kind == 62) {

 			Get();

-		} else if (t.kind == 60) {

+		} else if (t.kind == 63) {

 			Get();

-		} else Error(117);

+		} else Error(120);

 	}

 

 	static void Term(out Expression! e0) {

 		Token! x;  Expression! e1;  BinaryExpr.Opcode op; 

 		Factor(out e0);

-		while (t.kind == 70 || t.kind == 71) {

+		while (t.kind == 73 || t.kind == 74) {

 			AddOp(out x, out op);

 			Factor(out e1);

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

@@ -1245,74 +1287,74 @@ List<Expression!>! decreases) {
 	static void RelOp(out Token! x, out BinaryExpr.Opcode op) {

 		x = Token.NoToken;  op = BinaryExpr.Opcode.Add/*(dummy)*/; 

 		switch (t.kind) {

-		case 61: {

+		case 64: {

 			Get();

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

 			break;

 		}

-		case 14: {

+		case 17: {

 			Get();

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

 			break;

 		}

-		case 15: {

+		case 18: {

 			Get();

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

 			break;

 		}

-		case 62: {

+		case 65: {

 			Get();

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

 			break;

 		}

-		case 63: {

+		case 66: {

 			Get();

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

 			break;

 		}

-		case 64: {

+		case 67: {

 			Get();

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

 			break;

 		}

-		case 65: {

+		case 68: {

 			Get();

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

 			break;

 		}

-		case 48: {

+		case 51: {

 			Get();

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

 			break;

 		}

-		case 66: {

+		case 69: {

 			Get();

 			x = token;  op = BinaryExpr.Opcode.NotIn; 

 			break;

 		}

-		case 67: {

+		case 70: {

 			Get();

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

 			break;

 		}

-		case 68: {

+		case 71: {

 			Get();

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

 			break;

 		}

-		case 69: {

+		case 72: {

 			Get();

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

 			break;

 		}

-		default: Error(118); break;

+		default: Error(121); break;

 		}

 	}

 

 	static void Factor(out Expression! e0) {

 		Token! x;  Expression! e1;  BinaryExpr.Opcode op; 

 		UnaryExpression(out e0);

-		while (t.kind == 32 || t.kind == 72 || t.kind == 73) {

+		while (t.kind == 35 || t.kind == 75 || t.kind == 76) {

 			MulOp(out x, out op);

 			UnaryExpression(out e1);

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

@@ -1321,23 +1363,23 @@ List<Expression!>! decreases) {
 

 	static void AddOp(out Token! x, out BinaryExpr.Opcode op) {

 		x = Token.NoToken;  op=BinaryExpr.Opcode.Add/*(dummy)*/; 

-		if (t.kind == 70) {

+		if (t.kind == 73) {

 			Get();

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

-		} else if (t.kind == 71) {

+		} else if (t.kind == 74) {

 			Get();

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

-		} else Error(119);

+		} else Error(122);

 	}

 

 	static void UnaryExpression(out Expression! e) {

 		Token! x;  e = dummyExpr; 

-		if (t.kind == 71) {

+		if (t.kind == 74) {

 			Get();

 			x = token; 

 			UnaryExpression(out e);

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

-		} else if (t.kind == 74 || t.kind == 75) {

+		} else if (t.kind == 77 || t.kind == 78) {

 			NegOp();

 			x = token; 

 			UnaryExpression(out e);

@@ -1346,29 +1388,29 @@ List<Expression!>! decreases) {
 			SelectExpression(out e);

 		} else if (StartOf(14)) {

 			ConstAtomExpression(out e);

-		} else Error(120);

+		} else Error(123);

 	}

 

 	static void MulOp(out Token! x, out BinaryExpr.Opcode op) {

 		x = Token.NoToken;  op = BinaryExpr.Opcode.Add/*(dummy)*/; 

-		if (t.kind == 32) {

+		if (t.kind == 35) {

 			Get();

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

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

+		} else if (t.kind == 75) {

 			Get();

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

-		} else if (t.kind == 73) {

+		} else if (t.kind == 76) {

 			Get();

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

-		} else Error(121);

+		} else Error(124);

 	}

 

 	static void NegOp() {

-		if (t.kind == 74) {

+		if (t.kind == 77) {

 			Get();

-		} else if (t.kind == 75) {

+		} else if (t.kind == 78) {

 			Get();

-		} else Error(122);

+		} else Error(125);

 	}

 

 	static void ConstAtomExpression(out Expression! e) {

@@ -1376,17 +1418,17 @@ List<Expression!>! decreases) {
 		e = dummyExpr;  

 		

 		switch (t.kind) {

-		case 76: {

+		case 79: {

 			Get();

 			e = new LiteralExpr(token, false); 

 			break;

 		}

-		case 77: {

+		case 80: {

 			Get();

 			e = new LiteralExpr(token, true); 

 			break;

 		}

-		case 78: {

+		case 81: {

 			Get();

 			e = new LiteralExpr(token); 

 			break;

@@ -1396,61 +1438,61 @@ List<Expression!>! decreases) {
 			e = new LiteralExpr(token, n); 

 			break;

 		}

-		case 79: {

+		case 82: {

 			Get();

 			x = token; 

 			Ident(out dtName);

-			Expect(80);

+			Expect(83);

 			Ident(out id);

 			elements = new List<Expression!>(); 

-			if (t.kind == 23) {

+			if (t.kind == 26) {

 				Get();

 				if (StartOf(6)) {

 					Expressions(elements);

 				}

-				Expect(24);

+				Expect(27);

 			}

 			e = new DatatypeValue(token, dtName.val, id.val, elements); 

 			break;

 		}

-		case 81: {

+		case 84: {

 			Get();

 			x = token; 

-			Expect(23);

+			Expect(26);

 			Expression(out e);

-			Expect(24);

+			Expect(27);

 			e = new FreshExpr(x, e); 

 			break;

 		}

-		case 49: {

+		case 52: {

 			Get();

 			x = token; 

 			Expression(out e);

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

-			Expect(49);

+			Expect(52);

 			break;

 		}

-		case 5: {

+		case 6: {

 			Get();

 			x = token;  elements = new List<Expression!>(); 

 			if (StartOf(6)) {

 				Expressions(elements);

 			}

 			e = new SetDisplayExpr(x, elements); 

-			Expect(6);

+			Expect(7);

 			break;

 		}

-		case 82: {

+		case 85: {

 			Get();

 			x = token;  elements = new List<Expression!>(); 

 			if (StartOf(6)) {

 				Expressions(elements);

 			}

 			e = new SeqDisplayExpr(x, elements); 

-			Expect(83);

+			Expect(86);

 			break;

 		}

-		default: Error(123); break;

+		default: Error(126); break;

 		}

 	}

 

@@ -1468,13 +1510,13 @@ List<Expression!>! decreases) {
 	static void IdentOrFuncExpression(out Expression! e) {

 		Token! id;  e = dummyExpr;  List<Expression!>! args; 

 		Ident(out id);

-		if (t.kind == 23) {

+		if (t.kind == 26) {

 			Get();

 			args = new List<Expression!>(); 

 			if (StartOf(6)) {

 				Expressions(args);

 			}

-			Expect(24);

+			Expect(27);

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

 		}

 		if (e == dummyExpr) {

@@ -1489,25 +1531,25 @@ List<Expression!>! decreases) {
 

 	static void ObjectExpression(out Expression! e) {

 		Token! x;  e = dummyExpr; 

-		if (t.kind == 85) {

+		if (t.kind == 88) {

 			Get();

 			e = new ThisExpr(token); 

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

+		} else if (t.kind == 89) {

 			Get();

 			x = token; 

-			Expect(23);

+			Expect(26);

 			Expression(out e);

-			Expect(24);

+			Expect(27);

 			e = new OldExpr(x, e); 

-		} else if (t.kind == 23) {

+		} else if (t.kind == 26) {

 			Get();

 			if (StartOf(15)) {

 				QuantifierGuts(out e);

 			} else if (StartOf(6)) {

 				Expression(out e);

-			} else Error(124);

-			Expect(24);

-		} else Error(125);

+			} else Error(127);

+			Expect(27);

+		} else Error(128);

 	}

 

 	static void SelectOrCallSuffix(ref Expression! e) {

@@ -1515,27 +1557,27 @@ List<Expression!>! decreases) {
 		Expression e0 = null;  Expression e1 = null;  Expression! ee;  bool anyDots = false;

 		bool func = false;

 		

-		if (t.kind == 80) {

+		if (t.kind == 83) {

 			Get();

 			Ident(out id);

-			if (t.kind == 23) {

+			if (t.kind == 26) {

 				Get();

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

 				if (StartOf(6)) {

 					Expressions(args);

 				}

-				Expect(24);

+				Expect(27);

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

 			}

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

-		} else if (t.kind == 82) {

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

 			Get();

 			x = token; 

 			if (StartOf(6)) {

 				Expression(out ee);

 				e0 = ee; 

-				if (t.kind == 39 || t.kind == 84) {

-					if (t.kind == 84) {

+				if (t.kind == 42 || t.kind == 87) {

+					if (t.kind == 87) {

 						Get();

 						anyDots = true; 

 						if (StartOf(6)) {

@@ -1548,11 +1590,11 @@ List<Expression!>! decreases) {
 						e1 = ee; 

 					}

 				}

-			} else if (t.kind == 84) {

+			} else if (t.kind == 87) {

 				Get();

 				Expression(out ee);

 				anyDots = true;  e1 = ee; 

-			} else Error(126);

+			} else Error(129);

 			assert !anyDots ==> e0 != null;

 			if (anyDots) {

 			  assert e0 != null || e1 != null;

@@ -1565,8 +1607,8 @@ List<Expression!>! decreases) {
 			  e = new SeqUpdateExpr(x, e, e0, e1);

 			}

 			

-			Expect(83);

-		} else Error(127);

+			Expect(86);

+		} else Error(130);

 	}

 

 	static void QuantifierGuts(out Expression! q) {

@@ -1579,22 +1621,22 @@ List<Expression!>! decreases) {
 		Triggers trigs = null;

 		Expression! body;

 		

-		if (t.kind == 87 || t.kind == 88) {

+		if (t.kind == 90 || t.kind == 91) {

 			Forall();

 			x = token;  univ = true; 

-		} else if (t.kind == 89 || t.kind == 90) {

+		} else if (t.kind == 92 || t.kind == 93) {

 			Exists();

 			x = token; 

-		} else Error(128);

+		} else Error(131);

 		parseVarScope.PushMarker(); 

 		IdentTypeOptional(out bv);

 		bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); 

-		while (t.kind == 12) {

+		while (t.kind == 15) {

 			Get();

 			IdentTypeOptional(out bv);

 			bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); 

 		}

-		while (t.kind == 5) {

+		while (t.kind == 6) {

 			AttributeOrTrigger(ref attrs, ref trigs);

 		}

 		QSep();

@@ -1609,41 +1651,41 @@ List<Expression!>! decreases) {
 	}

 

 	static void Forall() {

-		if (t.kind == 87) {

+		if (t.kind == 90) {

 			Get();

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

+		} else if (t.kind == 91) {

 			Get();

-		} else Error(129);

+		} else Error(132);

 	}

 

 	static void Exists() {

-		if (t.kind == 89) {

+		if (t.kind == 92) {

 			Get();

-		} else if (t.kind == 90) {

+		} else if (t.kind == 93) {

 			Get();

-		} else Error(130);

+		} else Error(133);

 	}

 

 	static void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {

 		List<Expression!> es = new List<Expression!>();

 		

-		Expect(5);

-		if (t.kind == 13) {

+		Expect(6);

+		if (t.kind == 16) {

 			AttributeBody(ref attrs);

 		} else if (StartOf(6)) {

 			es = new List<Expression!>(); 

 			Expressions(es);

 			trigs = new Triggers(es, trigs); 

-		} else Error(131);

-		Expect(6);

+		} else Error(134);

+		Expect(7);

 	}

 

 	static void QSep() {

-		if (t.kind == 91) {

+		if (t.kind == 94) {

 			Get();

-		} else if (t.kind == 92) {

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

 			Get();

-		} else Error(132);

+		} else Error(135);

 	}

 

 	static void AttributeBody(ref Attributes attrs) {

@@ -1651,13 +1693,13 @@ List<Expression!>! decreases) {
 		List<Attributes.Argument!> aArgs = new List<Attributes.Argument!>();

 		Attributes.Argument! aArg;

 		

-		Expect(13);

+		Expect(16);

 		Expect(1);

 		aName = token.val; 

 		if (StartOf(16)) {

 			AttributeArg(out aArg);

 			aArgs.Add(aArg); 

-			while (t.kind == 12) {

+			while (t.kind == 15) {

 				Get();

 				AttributeArg(out aArg);

 				aArgs.Add(aArg); 

@@ -1674,7 +1716,7 @@ List<Expression!>! decreases) {
 		} else if (StartOf(6)) {

 			Expression(out e);

 			arg = new Attributes.Argument(e); 

-		} else Error(133);

+		} else Error(136);

 	}

 

 

@@ -1697,136 +1739,139 @@ List<Expression!>! decreases) {
 			case 1: s = "ident expected"; break;

 			case 2: s = "digits expected"; break;

 			case 3: s = "string expected"; break;

-			case 4: s = "class expected"; break;

-			case 5: s = "{ expected"; break;

-			case 6: s = "} expected"; break;

-			case 7: s = "ghost expected"; break;

-			case 8: s = "use expected"; break;

-			case 9: s = "datatype expected"; break;

-			case 10: s = "; expected"; break;

-			case 11: s = "var expected"; break;

-			case 12: s = ", expected"; break;

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

-			case 14: s = "< expected"; break;

-			case 15: s = "> expected"; break;

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

-			case 17: s = "returns expected"; break;

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

-			case 19: s = "free expected"; break;

-			case 20: s = "requires expected"; break;

-			case 21: s = "ensures expected"; break;

-			case 22: s = "decreases expected"; break;

-			case 23: s = "( expected"; break;

-			case 24: s = ") expected"; break;

-			case 25: s = "bool expected"; break;

-			case 26: s = "int expected"; break;

-			case 27: s = "set expected"; break;

-			case 28: s = "seq expected"; break;

-			case 29: s = "object expected"; break;

-			case 30: s = "function expected"; break;

-			case 31: s = "reads expected"; break;

-			case 32: s = "* expected"; break;

-			case 33: s = "match expected"; break;

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

-			case 35: s = "=> expected"; break;

-			case 36: s = "label expected"; break;

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

-			case 38: s = "return expected"; break;

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

-			case 40: s = "new expected"; break;

-			case 41: s = "havoc expected"; break;

-			case 42: s = "if expected"; break;

-			case 43: s = "else expected"; break;

-			case 44: s = "while expected"; break;

-			case 45: s = "invariant expected"; break;

-			case 46: s = "call expected"; break;

-			case 47: s = "foreach expected"; break;

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

-			case 49: s = "| expected"; break;

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

-			case 51: s = "assume expected"; break;

-			case 52: s = "then expected"; break;

-			case 53: s = "<==> expected"; break;

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

-			case 55: s = "==> expected"; break;

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

-			case 57: s = "&& expected"; break;

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

-			case 59: s = "|| expected"; break;

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

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

-			case 62: s = "<= expected"; break;

-			case 63: s = ">= expected"; break;

-			case 64: s = "!= expected"; break;

-			case 65: s = "!! expected"; break;

-			case 66: s = "!in expected"; break;

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

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

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

-			case 70: s = "+ expected"; break;

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

-			case 72: s = "/ expected"; break;

-			case 73: s = "% expected"; break;

-			case 74: s = "! expected"; break;

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

-			case 76: s = "false expected"; break;

-			case 77: s = "true expected"; break;

-			case 78: s = "null expected"; break;

-			case 79: s = "# expected"; break;

-			case 80: s = ". expected"; break;

-			case 81: s = "fresh expected"; break;

-			case 82: s = "[ expected"; break;

-			case 83: s = "] expected"; break;

-			case 84: s = ".. expected"; break;

-			case 85: s = "this expected"; break;

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

-			case 87: s = "forall expected"; break;

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

-			case 89: s = "exists expected"; break;

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

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

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

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

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

-			case 95: s = "invalid FunctionDecl"; break;

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

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

-			case 98: s = "invalid MethodSpec"; break;

-			case 99: s = "invalid MethodSpec"; break;

-			case 100: s = "invalid Expression"; break;

-			case 101: s = "invalid ReferenceType"; break;

-			case 102: s = "invalid FunctionSpec"; break;

-			case 103: s = "invalid FunctionBody"; break;

-			case 104: s = "invalid PossiblyWildExpression"; break;

-			case 105: s = "invalid MatchExpression"; break;

-			case 106: s = "invalid Stmt"; break;

-			case 107: s = "invalid OneStmt"; break;

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

-			case 109: s = "invalid ForeachStmt"; break;

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

-			case 111: s = "invalid SelectExpression"; break;

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

-			case 113: s = "invalid CallStmtSubExpr"; break;

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

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

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

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

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

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

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

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

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

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

-			case 124: s = "invalid ObjectExpression"; break;

-			case 125: s = "invalid ObjectExpression"; break;

-			case 126: s = "invalid SelectOrCallSuffix"; break;

-			case 127: s = "invalid SelectOrCallSuffix"; break;

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

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

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

-			case 131: s = "invalid AttributeOrTrigger"; break;

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

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

+			case 4: s = "module expected"; break;

+			case 5: s = "imports expected"; break;

+			case 6: s = "{ expected"; break;

+			case 7: s = "} expected"; break;

+			case 8: s = "class expected"; break;

+			case 9: s = "ghost expected"; break;

+			case 10: s = "static expected"; break;

+			case 11: s = "use expected"; break;

+			case 12: s = "datatype expected"; break;

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

+			case 14: s = "var expected"; break;

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

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

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

+			case 18: s = "> expected"; break;

+			case 19: s = "method expected"; break;

+			case 20: s = "returns expected"; break;

+			case 21: s = "modifies expected"; break;

+			case 22: s = "free expected"; break;

+			case 23: s = "requires expected"; break;

+			case 24: s = "ensures expected"; break;

+			case 25: s = "decreases expected"; break;

+			case 26: s = "( expected"; break;

+			case 27: s = ") expected"; break;

+			case 28: s = "bool expected"; break;

+			case 29: s = "int expected"; break;

+			case 30: s = "set expected"; break;

+			case 31: s = "seq expected"; break;

+			case 32: s = "object expected"; break;

+			case 33: s = "function expected"; break;

+			case 34: s = "reads expected"; break;

+			case 35: s = "* expected"; break;

+			case 36: s = "match expected"; break;

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

+			case 38: s = "=> expected"; break;

+			case 39: s = "label expected"; break;

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

+			case 41: s = "return expected"; break;

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

+			case 43: s = "new expected"; break;

+			case 44: s = "havoc expected"; break;

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

+			case 46: s = "else expected"; break;

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

+			case 48: s = "invariant expected"; break;

+			case 49: s = "call expected"; break;

+			case 50: s = "foreach expected"; break;

+			case 51: s = "in expected"; break;

+			case 52: s = "| expected"; break;

+			case 53: s = "assert expected"; break;

+			case 54: s = "assume expected"; break;

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

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

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

+			case 58: s = "==> expected"; break;

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

+			case 60: s = "&& expected"; break;

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

+			case 62: s = "|| expected"; break;

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

+			case 64: s = "== expected"; break;

+			case 65: s = "<= expected"; break;

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

+			case 67: s = "!= expected"; break;

+			case 68: s = "!! expected"; break;

+			case 69: s = "!in expected"; break;

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

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

+			case 72: s = "\\u2265 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 = "! expected"; break;

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

+			case 79: s = "false expected"; break;

+			case 80: s = "true expected"; break;

+			case 81: s = "null expected"; break;

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

+			case 83: s = ". expected"; break;

+			case 84: s = "fresh expected"; break;

+			case 85: s = "[ expected"; break;

+			case 86: s = "] expected"; break;

+			case 87: s = ".. expected"; break;

+			case 88: s = "this expected"; break;

+			case 89: s = "old expected"; break;

+			case 90: s = "forall expected"; break;

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

+			case 92: s = "exists expected"; break;

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

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

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

+			case 96: s = "??? expected"; break;

+			case 97: s = "invalid ClassMemberDecl"; break;

+			case 98: s = "invalid FunctionDecl"; break;

+			case 99: s = "invalid MethodDecl"; break;

+			case 100: s = "invalid TypeAndToken"; break;

+			case 101: s = "invalid MethodSpec"; break;

+			case 102: s = "invalid MethodSpec"; break;

+			case 103: s = "invalid Expression"; break;

+			case 104: s = "invalid ReferenceType"; break;

+			case 105: s = "invalid FunctionSpec"; break;

+			case 106: s = "invalid FunctionBody"; break;

+			case 107: s = "invalid PossiblyWildExpression"; break;

+			case 108: s = "invalid MatchExpression"; break;

+			case 109: s = "invalid Stmt"; break;

+			case 110: s = "invalid OneStmt"; break;

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

+			case 112: s = "invalid ForeachStmt"; break;

+			case 113: s = "invalid AssignRhs"; break;

+			case 114: s = "invalid SelectExpression"; break;

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

+			case 116: s = "invalid CallStmtSubExpr"; break;

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

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

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

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

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

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

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

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

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

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

+			case 127: s = "invalid ObjectExpression"; break;

+			case 128: s = "invalid ObjectExpression"; break;

+			case 129: s = "invalid SelectOrCallSuffix"; break;

+			case 130: s = "invalid SelectOrCallSuffix"; break;

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

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

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

+			case 134: s = "invalid AttributeOrTrigger"; break;

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

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

 

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

 		}

@@ -1834,23 +1879,23 @@ List<Expression!>! decreases) {
 	}

 

 	static bool[,]! set = {

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

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

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

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

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

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

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

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

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

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

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

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

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

 

 	};

 

diff --git a/Source/Dafny/Printer.ssc b/Source/Dafny/Printer.ssc
index cf3d8294..88e9d5dc 100644
--- a/Source/Dafny/Printer.ssc
+++ b/Source/Dafny/Printer.ssc
@@ -23,41 +23,69 @@ namespace Microsoft.Dafny {
         wr.WriteLine("// " + Bpl.CommandLineOptions.Clo.Environment);

       }

       wr.WriteLine("// {0}", prog.Name);

+      ModuleDecl currentModule = null;

+      int indent = 0;

       foreach (TopLevelDecl d in prog.Classes) {

+        if (d.Module != currentModule) {

+          if (currentModule != null) {

+            wr.WriteLine("}");

+          }

+          if (d.Module == null) {

+            indent = 0;

+          } else {

+            wr.Write("module ");

+            PrintAttributes(d.Module.Attributes);

+            wr.Write("{0}", d.Module.Name);

+            if (d.Module.Imports.Count != 0) {

+              string sep = "imports ";

+              foreach (string imp in d.Module.Imports) {

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

+                sep = ", ";

+              }

+            }

+            wr.WriteLine("{");

+            indent = IndentAmount;

+          }

+        }

         wr.WriteLine();

         if (d is ClassDecl) {

-          PrintClass((ClassDecl)d);

+          PrintClass((ClassDecl)d, indent);

         } else {

-          PrintDatatype((DatatypeDecl)d);

+          PrintDatatype((DatatypeDecl)d, indent);

         }

       }

+      if (currentModule != null) {

+        wr.WriteLine("}");

+      }

     }

     

-    public void PrintClass(ClassDecl! c) {

+    public void PrintClass(ClassDecl! c, int indent) {

+      Indent(indent);

       PrintClassMethodHelper("class", c.Attributes, c.Name, c.TypeArgs);

       if (c.Members.Count == 0) {

         wr.WriteLine(" { }");

       } else {

         int state = 0;  // 0 - no members yet; 1 - previous member was a field; 2 - previous member was non-field

         wr.WriteLine(" {");

+        int ind = indent + IndentAmount;

         foreach (MemberDecl m in c.Members) {

           if (m is Method) {

             if (state != 0) { wr.WriteLine(); }

-            PrintMethod((Method)m);

+            PrintMethod((Method)m, ind);

             state = 2;

           } else if (m is Field) {

             if (state == 2) { wr.WriteLine(); }

-            PrintField((Field)m);

+            PrintField((Field)m, ind);

             state = 1;

           } else if (m is Function) {

             if (state != 0) { wr.WriteLine(); }

-            PrintFunction((Function)m);

+            PrintFunction((Function)m, ind);

             state = 2;

           } else {

             assert false;  // unexpected member

           }

         }

-        wr.WriteLine("}");

+        Indent(indent);  wr.WriteLine("}");

       }

     }

     

@@ -78,16 +106,18 @@ namespace Microsoft.Dafny {
       }

     }

     

-    public void PrintDatatype(DatatypeDecl! dt) {

+    public void PrintDatatype(DatatypeDecl! dt, int indent) {

+      Indent(indent);

       PrintClassMethodHelper("datatype", dt.Attributes, dt.Name, dt.TypeArgs);

       if (dt.Ctors.Count == 0) {

         wr.WriteLine(" { }");

       } else {

         wr.WriteLine(" {");

+        int ind = indent + IndentAmount;

         foreach (DatatypeCtor ctor in dt.Ctors) {

-          PrintCtor(ctor);

+          PrintCtor(ctor, ind);

         }

-        wr.WriteLine("}");

+        Indent(indent);  wr.WriteLine("}");

       }

     }

     

@@ -111,8 +141,8 @@ namespace Microsoft.Dafny {
       }

     }

     

-    public void PrintField(Field! field) {

-      Indent(IndentAmount);

+    public void PrintField(Field! field, int indent) {

+      Indent(indent);

       if (field.IsGhost) {

         wr.Write("ghost ");

       }

@@ -123,11 +153,11 @@ namespace Microsoft.Dafny {
       wr.WriteLine(";");

     }

     

-    public void PrintFunction(Function! f) {

-      Indent(IndentAmount);

+    public void PrintFunction(Function! f, int indent) {

+      Indent(indent);

       string k = "function";

       if (f.IsUse) { k = "use " + k; }

-      if (f.IsClass) { k = "class " + k; }

+      if (f.IsStatic) { k = "static " + k; }

       if (!f.IsGhost) { k += " method"; }

       PrintClassMethodHelper(k, f.Attributes, f.Name, f.TypeArgs);

       PrintFormals(f.Formals);

@@ -138,20 +168,21 @@ namespace Microsoft.Dafny {
       } else {

         wr.WriteLine();

       }

-      PrintSpec("requires", f.Req, 2 * IndentAmount);

-      PrintSpecLine("reads", f.Reads, 2 * IndentAmount);

-      PrintSpecLine("decreases", f.Decreases, 2 * IndentAmount);

+      int ind = indent + IndentAmount;

+      PrintSpec("requires", f.Req, ind);

+      PrintSpecLine("reads", f.Reads, ind);

+      PrintSpecLine("decreases", f.Decreases, ind);

       if (f.Body != null) {

-        Indent(IndentAmount);

+        Indent(indent);

         wr.WriteLine("{");

-        PrintExtendedExpr(f.Body, IndentAmount + IndentAmount);

-        Indent(IndentAmount);

+        PrintExtendedExpr(f.Body, ind);

+        Indent(indent);

         wr.WriteLine("}");

       }

     }

     

-    public void PrintCtor(DatatypeCtor! ctor) {

-      Indent(IndentAmount);

+    public void PrintCtor(DatatypeCtor! ctor, int indent) {

+      Indent(indent);

       PrintClassMethodHelper("", ctor.Attributes, ctor.Name, ctor.TypeArgs);

       if (ctor.Formals.Count != 0) {

         PrintFormals(ctor.Formals);

@@ -172,10 +203,10 @@ namespace Microsoft.Dafny {
       }

     }

     

-    public void PrintMethod(Method! method) {

-      Indent(IndentAmount);

+    public void PrintMethod(Method! method, int indent) {

+      Indent(indent);

       string k = "method";

-      if (method.IsClass) { k = "class " + k; }

+      if (method.IsStatic) { k = "static " + k; }

       if (method.IsGhost) { k = "ghost " + k; }

       PrintClassMethodHelper(k, method.Attributes, method.Name, method.TypeArgs);

       PrintFormals(method.Ins);

@@ -190,15 +221,16 @@ namespace Microsoft.Dafny {
         PrintFormals(method.Outs);

       }

       wr.WriteLine(method.Body == null ? ";" : ":");

-      

-      PrintSpec("requires", method.Req, 2 * IndentAmount);

-      PrintSpecLine("modifies", method.Mod, 2 * IndentAmount);

-      PrintSpec("ensures", method.Ens, 2 * IndentAmount);

-      PrintSpecLine("decreases", method.Decreases, 2 * IndentAmount);

+

+      int ind = indent + IndentAmount;      

+      PrintSpec("requires", method.Req, ind);

+      PrintSpecLine("modifies", method.Mod, ind);

+      PrintSpec("ensures", method.Ens, ind);

+      PrintSpecLine("decreases", method.Decreases, ind);

       

       if (method.Body != null) {

-        Indent(IndentAmount);

-        PrintStatement(method.Body, IndentAmount);

+        Indent(indent);

+        PrintStatement(method.Body, ind);

         wr.WriteLine();

       }

     }

diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc
index 953f429a..235c9036 100644
--- a/Source/Dafny/Resolver.ssc
+++ b/Source/Dafny/Resolver.ssc
@@ -36,8 +36,44 @@ namespace Microsoft.Dafny {
     readonly Dictionary<string!,TopLevelDecl!>! classes = new Dictionary<string!,TopLevelDecl!>();

     readonly Dictionary<ClassDecl!,Dictionary<string!,MemberDecl!>!>! classMembers = new Dictionary<ClassDecl!,Dictionary<string!,MemberDecl!>!>();

     readonly Dictionary<DatatypeDecl!,Dictionary<string!,DatatypeCtor!>!>! datatypeCtors = new Dictionary<DatatypeDecl!,Dictionary<string!,DatatypeCtor!>!>();

+    readonly Graph<ModuleDecl!>! importGraph = new Graph<ModuleDecl!>();

 

     public void ResolveProgram(Program! prog) {

+      // register modules

+      Dictionary<string,ModuleDecl!> modules = new Dictionary<string,ModuleDecl!>();

+      foreach (ModuleDecl m in prog.Modules) {

+        if (modules.ContainsKey(m.Name)) {

+          Error(m, "Duplicate module name: {0}", m.Name);

+        } else {

+          modules.Add(m.Name, m);

+        }

+      }

+      // resolve imports

+      foreach (ModuleDecl m in prog.Modules) {

+        foreach (string imp in m.Imports) {

+          ModuleDecl other;

+          if (modules.TryGetValue(imp, out other)) {

+            assert other != null;  // follows from postcondition of TryGetValue

+            importGraph.AddEdge(m, other);

+          } else {

+            Error(m, "module {0} named among imports does not exist", imp);

+          }

+        }

+      }

+      // check for cycles in the import graph

+      List<ModuleDecl!> cycle = importGraph.TryFindCycle();

+      if (cycle != null) {

+        string cy = "";

+        string sep = "";

+        foreach (ModuleDecl m in cycle) {

+          cy = m.Name + sep + cy;

+          sep = " -> ";

+        }

+        Error(cycle[0], "import graph contains a cycle: {0}", cy);

+      }

+

+      // Done with modules; now, do classes and datatypes

+      

       foreach (TopLevelDecl d in prog.Classes) {

         // register the class/datatype name

         if (classes.ContainsKey(d.Name)) {

@@ -76,7 +112,7 @@ namespace Microsoft.Dafny {
           }

         }

       }

-

+      

       // resolve each class

       Graph<DatatypeDecl!> datatypeDependencies = new Graph<DatatypeDecl!>();

       foreach (TopLevelDecl d in prog.Classes) {

@@ -324,7 +360,7 @@ namespace Microsoft.Dafny {
     /// </summary>

     void ResolveFunction(Function! f) {

       scope.PushMarker();

-      if (f.IsClass) {

+      if (f.IsStatic) {

         scope.AllowInstance = false;

       }

       foreach (Formal p in f.Formals) {

@@ -394,7 +430,7 @@ namespace Microsoft.Dafny {
     void ResolveMethod(Method! m) {

       // Add in-parameters to the scope, but don't care about any duplication errors, since they have already been reported

       scope.PushMarker();

-      if (m.IsClass) {

+      if (m.IsStatic) {

         scope.AllowInstance = false;

       }

       foreach (Formal p in m.Ins) {

@@ -916,11 +952,11 @@ namespace Microsoft.Dafny {
           Error(s, "wrong number of method result arguments (got {0}, expected {1})", s.Lhs.Count, method.Outs.Count);

         } else {

           assert ctype != null;  // follows from postcondition of ResolveMember above

-          if (!scope.AllowInstance && !method.IsClass && s.Receiver is ThisExpr) {

+          if (!scope.AllowInstance && !method.IsStatic && s.Receiver is ThisExpr) {

             // The call really needs an instance, but that instance is given as 'this', which is not

             // available in this context.  For more details, see comment in the resolution of a

             // FunctionCallExpr.

-            Error(s.Receiver, "'this' is not allowed in a 'class' context");

+            Error(s.Receiver, "'this' is not allowed in a 'static' context");

           }

           // build the type substitution map

           Dictionary<TypeParameter!,Type!> subst = new Dictionary<TypeParameter!,Type!>();

@@ -1363,7 +1399,7 @@ namespace Microsoft.Dafny {
             Error(expr, "wrong number of function arguments (got {0}, expected {1})", e.Args.Count, function.Formals.Count);

           } else {

             assert ctype != null;  // follows from postcondition of ResolveMember

-            if (!scope.AllowInstance && !function.IsClass && e.Receiver is ThisExpr) {

+            if (!scope.AllowInstance && !function.IsStatic && e.Receiver is ThisExpr) {

               // The call really needs an instance, but that instance is given as 'this', which is not

               // available in this context.  In most cases, occurrences of 'this' inside e.Receiver would

               // have been caught in the recursive call to resolve e.Receiver, but not the specific case

@@ -1371,7 +1407,7 @@ namespace Microsoft.Dafny {
               // in the event that a class function calls another class function (and note that we need the

               // type of the receiver in order to find the method, so we could not have made this check

               // earlier).

-              Error(e.Receiver, "'this' is not allowed in a 'class' context");

+              Error(e.Receiver, "'this' is not allowed in a 'static' context");

             }

             // build the type substitution map

             Dictionary<TypeParameter!,Type!> subst = new Dictionary<TypeParameter!,Type!>();

diff --git a/Source/Dafny/Scanner.ssc b/Source/Dafny/Scanner.ssc
index a1895c0c..8c7a1b15 100644
--- a/Source/Dafny/Scanner.ssc
+++ b/Source/Dafny/Scanner.ssc
@@ -133,7 +133,7 @@ public class Scanner {
 		start[8804] = 38;

 		start[8805] = 39;

 	}

-	const int noSym = 93;

+	const int noSym = 96;

 	static short[] start = new short[16385];

 

 

@@ -275,50 +275,53 @@ public class Scanner {
   

   static void CheckLiteral() {

     switch (t.val) {

-			case "class": t.kind = 4; break;

-			case "ghost": t.kind = 7; break;

-			case "use": t.kind = 8; break;

-			case "datatype": t.kind = 9; break;

-			case "var": t.kind = 11; break;

-			case "method": t.kind = 16; break;

-			case "returns": t.kind = 17; break;

-			case "modifies": t.kind = 18; break;

-			case "free": t.kind = 19; break;

-			case "requires": t.kind = 20; break;

-			case "ensures": t.kind = 21; break;

-			case "decreases": t.kind = 22; break;

-			case "bool": t.kind = 25; break;

-			case "int": t.kind = 26; break;

-			case "set": t.kind = 27; break;

-			case "seq": t.kind = 28; break;

-			case "object": t.kind = 29; break;

-			case "function": t.kind = 30; break;

-			case "reads": t.kind = 31; break;

-			case "match": t.kind = 33; break;

-			case "case": t.kind = 34; break;

-			case "label": t.kind = 36; break;

-			case "break": t.kind = 37; break;

-			case "return": t.kind = 38; break;

-			case "new": t.kind = 40; break;

-			case "havoc": t.kind = 41; break;

-			case "if": t.kind = 42; break;

-			case "else": t.kind = 43; break;

-			case "while": t.kind = 44; break;

-			case "invariant": t.kind = 45; break;

-			case "call": t.kind = 46; break;

-			case "foreach": t.kind = 47; break;

-			case "in": t.kind = 48; break;

-			case "assert": t.kind = 50; break;

-			case "assume": t.kind = 51; break;

-			case "then": t.kind = 52; break;

-			case "false": t.kind = 76; break;

-			case "true": t.kind = 77; break;

-			case "null": t.kind = 78; break;

-			case "fresh": t.kind = 81; break;

-			case "this": t.kind = 85; break;

-			case "old": t.kind = 86; break;

-			case "forall": t.kind = 87; break;

-			case "exists": t.kind = 89; break;

+			case "module": t.kind = 4; break;

+			case "imports": t.kind = 5; break;

+			case "class": t.kind = 8; break;

+			case "ghost": t.kind = 9; break;

+			case "static": t.kind = 10; break;

+			case "use": t.kind = 11; break;

+			case "datatype": t.kind = 12; break;

+			case "var": t.kind = 14; break;

+			case "method": t.kind = 19; break;

+			case "returns": t.kind = 20; break;

+			case "modifies": t.kind = 21; break;

+			case "free": t.kind = 22; break;

+			case "requires": t.kind = 23; break;

+			case "ensures": t.kind = 24; break;

+			case "decreases": t.kind = 25; break;

+			case "bool": t.kind = 28; break;

+			case "int": t.kind = 29; break;

+			case "set": t.kind = 30; break;

+			case "seq": t.kind = 31; break;

+			case "object": t.kind = 32; break;

+			case "function": t.kind = 33; break;

+			case "reads": t.kind = 34; break;

+			case "match": t.kind = 36; break;

+			case "case": t.kind = 37; break;

+			case "label": t.kind = 39; break;

+			case "break": t.kind = 40; break;

+			case "return": t.kind = 41; break;

+			case "new": t.kind = 43; break;

+			case "havoc": t.kind = 44; break;

+			case "if": t.kind = 45; break;

+			case "else": t.kind = 46; break;

+			case "while": t.kind = 47; break;

+			case "invariant": t.kind = 48; break;

+			case "call": t.kind = 49; break;

+			case "foreach": t.kind = 50; break;

+			case "in": t.kind = 51; break;

+			case "assert": t.kind = 53; break;

+			case "assume": t.kind = 54; break;

+			case "then": t.kind = 55; break;

+			case "false": t.kind = 79; break;

+			case "true": t.kind = 80; break;

+			case "null": t.kind = 81; break;

+			case "fresh": t.kind = 84; break;

+			case "this": t.kind = 88; break;

+			case "old": t.kind = 89; break;

+			case "forall": t.kind = 90; break;

+			case "exists": t.kind = 92; break;

 			default: break;

 

     }

@@ -348,119 +351,119 @@ public class Scanner {
 			case 4:

 				{t.kind = 3; goto done;}

 			case 5:

-				{t.kind = 5; goto done;}

-			case 6:

 				{t.kind = 6; goto done;}

+			case 6:

+				{t.kind = 7; goto done;}

 			case 7:

-				{t.kind = 10; goto done;}

+				{t.kind = 13; goto done;}

 			case 8:

-				{t.kind = 12; goto done;}

+				{t.kind = 15; goto done;}

 			case 9:

 				if (ch == '=') {buf.Append(ch); NextCh(); goto case 17;}

 				else if (ch == ':') {buf.Append(ch); NextCh(); goto case 52;}

-				else {t.kind = 13; goto done;}

+				else {t.kind = 16; goto done;}

 			case 10:

 				if (ch == '=') {buf.Append(ch); NextCh(); goto case 19;}

-				else {t.kind = 14; goto done;}

+				else {t.kind = 17; goto done;}

 			case 11:

 				if (ch == '=') {buf.Append(ch); NextCh(); goto case 31;}

-				else {t.kind = 15; goto done;}

+				else {t.kind = 18; goto done;}

 			case 12:

-				{t.kind = 23; goto done;}

+				{t.kind = 26; goto done;}

 			case 13:

-				{t.kind = 24; goto done;}

+				{t.kind = 27; goto done;}

 			case 14:

-				{t.kind = 32; goto done;}

+				{t.kind = 35; goto done;}

 			case 15:

 				if (ch == '>') {buf.Append(ch); NextCh(); goto case 16;}

 				else if (ch == '=') {buf.Append(ch); NextCh(); goto case 23;}

 				else {t.kind = noSym; goto done;}

 			case 16:

-				{t.kind = 35; goto done;}

+				{t.kind = 38; goto done;}

 			case 17:

-				{t.kind = 39; goto done;}

+				{t.kind = 42; goto done;}

 			case 18:

 				if (ch == '|') {buf.Append(ch); NextCh(); goto case 29;}

-				else {t.kind = 49; goto done;}

+				else {t.kind = 52; goto done;}

 			case 19:

 				if (ch == '=') {buf.Append(ch); NextCh(); goto case 20;}

-				else {t.kind = 62; goto done;}

+				else {t.kind = 65; goto done;}

 			case 20:

 				if (ch == '>') {buf.Append(ch); NextCh(); goto case 21;}

 				else {t.kind = noSym; goto done;}

 			case 21:

-				{t.kind = 53; goto done;}

+				{t.kind = 56; goto done;}

 			case 22:

-				{t.kind = 54; goto done;}

+				{t.kind = 57; goto done;}

 			case 23:

 				if (ch == '>') {buf.Append(ch); NextCh(); goto case 24;}

-				else {t.kind = 61; goto done;}

+				else {t.kind = 64; goto done;}

 			case 24:

-				{t.kind = 55; goto done;}

+				{t.kind = 58; goto done;}

 			case 25:

-				{t.kind = 56; goto done;}

+				{t.kind = 59; goto done;}

 			case 26:

 				if (ch == '&') {buf.Append(ch); NextCh(); goto case 27;}

 				else {t.kind = noSym; goto done;}

 			case 27:

-				{t.kind = 57; goto done;}

+				{t.kind = 60; goto done;}

 			case 28:

-				{t.kind = 58; goto done;}

+				{t.kind = 61; goto done;}

 			case 29:

-				{t.kind = 59; goto done;}

+				{t.kind = 62; goto done;}

 			case 30:

-				{t.kind = 60; goto done;}

-			case 31:

 				{t.kind = 63; goto done;}

+			case 31:

+				{t.kind = 66; goto done;}

 			case 32:

 				if (ch == '=') {buf.Append(ch); NextCh(); goto case 33;}

 				else if (ch == '!') {buf.Append(ch); NextCh(); goto case 34;}

 				else if (ch == 'i') {buf.Append(ch); NextCh(); goto case 35;}

-				else {t.kind = 74; goto done;}

+				else {t.kind = 77; goto done;}

 			case 33:

-				{t.kind = 64; goto done;}

+				{t.kind = 67; goto done;}

 			case 34:

-				{t.kind = 65; goto done;}

+				{t.kind = 68; goto done;}

 			case 35:

 				if (ch == 'n') {buf.Append(ch); NextCh(); goto case 36;}

 				else {t.kind = noSym; goto done;}

 			case 36:

-				{t.kind = 66; goto done;}

+				{t.kind = 69; goto done;}

 			case 37:

-				{t.kind = 67; goto done;}

+				{t.kind = 70; goto done;}

 			case 38:

-				{t.kind = 68; goto done;}

+				{t.kind = 71; goto done;}

 			case 39:

-				{t.kind = 69; goto done;}

+				{t.kind = 72; goto done;}

 			case 40:

-				{t.kind = 70; goto done;}

+				{t.kind = 73; goto done;}

 			case 41:

-				{t.kind = 71; goto done;}

+				{t.kind = 74; goto done;}

 			case 42:

-				{t.kind = 72; goto done;}

+				{t.kind = 75; goto done;}

 			case 43:

-				{t.kind = 73; goto done;}

+				{t.kind = 76; goto done;}

 			case 44:

-				{t.kind = 75; goto done;}

+				{t.kind = 78; goto done;}

 			case 45:

-				{t.kind = 79; goto done;}

+				{t.kind = 82; goto done;}

 			case 46:

 				if (ch == '.') {buf.Append(ch); NextCh(); goto case 49;}

-				else {t.kind = 80; goto done;}

+				else {t.kind = 83; goto done;}

 			case 47:

-				{t.kind = 82; goto done;}

+				{t.kind = 85; goto done;}

 			case 48:

-				{t.kind = 83; goto done;}

+				{t.kind = 86; goto done;}

 			case 49:

-				{t.kind = 84; goto done;}

+				{t.kind = 87; goto done;}

 			case 50:

-				{t.kind = 88; goto done;}

+				{t.kind = 91; goto done;}

 			case 51:

-				{t.kind = 90; goto done;}

+				{t.kind = 93; goto done;}

 			case 52:

-				{t.kind = 91; goto done;}

+				{t.kind = 94; goto done;}

 			case 53:

-				{t.kind = 92; goto done;}

+				{t.kind = 95; goto done;}

 			case 54: {t.kind = 0; goto done;}

     }

     done:

diff --git a/Source/Dafny/SccGraph.ssc b/Source/Dafny/SccGraph.ssc
index 3705be76..e508d129 100644
--- a/Source/Dafny/SccGraph.ssc
+++ b/Source/Dafny/SccGraph.ssc
@@ -10,8 +10,10 @@ namespace Microsoft.Dafny {
       public readonly List<Vertex!>! Successors = new List<Vertex!>();

       public Vertex SccRepresentative;  // null if not computed or if the vertex represents itself

       public List<Vertex!> SccMembers;  // non-null only for the representative of the SCC

-      // the following fields are used during the computation of SCCs:

+      public Dictionary<Vertex,object> downwardClosure;  // irrefexive, transitive closure;  null if not computed

+      // the following field is used during the computation of SCCs and of reachability

       public VisitedStatus Visited;

+      // the following fields are used during the computation of SCCs:

       public int DfNumber;

       public int LowLink;

       

@@ -155,5 +157,82 @@ namespace Microsoft.Dafny {
         }

       }

     }

+    

+    /// <summary>

+    /// Returns null if the graph has no cycles.  If the graph does contain some cycle, returns the list of

+    /// vertices on one such cycle.

+    /// </summary>

+    public List<Node> TryFindCycle() {

+      // reset all visited information

+      foreach (Vertex v in vertices.Values) {

+        v.Visited = VisitedStatus.Unvisited;

+      }

+      

+      foreach (Vertex v in vertices.Values) {

+        assert v.Visited != VisitedStatus.OnStack;

+        if (v.Visited == VisitedStatus.Unvisited) {

+          List<Vertex!> cycle = CycleSearch(v);

+          if (cycle != null) {

+            List<Node> nodes = new List<Node>();

+            foreach (Vertex v in cycle) {

+              nodes.Add(v.N);

+            }

+            return nodes;  // a cycle is found

+          }

+        }

+      }

+      return null;  // there are no cycles

+    }

+    

+    /// <summary>

+    /// A return of null means there are no cycles involving any vertex in the subtree rooted at v.

+    /// A non-null return means a cycle has been found.  Then:

+    /// If v.Visited == Visited, then the entire cycle is described in the returned list.

+    /// If v.Visited == OnStack, then the cycle consists of the vertices strictly deeper than

+    /// w on the stack followed by the vertices (in reverse order) in the returned list, where

+    /// w is the first vertex in the list returned.

+    /// </summary>

+    List<Vertex!> CycleSearch(Vertex! v)

+      requires v.Visited == VisitedStatus.Unvisited;

+      ensures v.Visited != VisitedStatus.Unvisited;

+      ensures result == null ==> v.Visited == VisitedStatus.Visited;

+      ensures result != null ==> result.Count != 0;

+    {

+      v.Visited = VisitedStatus.OnStack;

+      foreach (Vertex succ in v.Successors) {

+        // todo:  I would use a 'switch' statement, but there seems to be a bug in the Spec# compiler's type checking.

+        if (succ.Visited == VisitedStatus.Visited) {

+          // there is no cycle in the subtree rooted at succ, hence this path does not give rise to any cycles

+        } else if (succ.Visited == VisitedStatus.OnStack) {

+          // we found a cycle!

+          List<Vertex!> cycle = new List<Vertex!>();

+          cycle.Add(succ);

+          if (v == succ) {

+            // entire cycle has been found

+            v.Visited = VisitedStatus.Visited;

+          }

+          return cycle;

+        } else {

+          assert succ.Visited == VisitedStatus.Unvisited;

+          List<Vertex!> cycle = CycleSearch(succ);

+          if (cycle != null) {

+            if (succ.Visited == VisitedStatus.Visited) {

+              // the entire cycle has been collected

+              v.Visited = VisitedStatus.Visited;

+              return cycle;

+            } else {

+              cycle.Add(succ);

+              if (v == cycle[0]) {

+                // the entire cycle has been collected and we are the first to find out

+                v.Visited = VisitedStatus.Visited;

+              }

+              return cycle;

+            }

+          }

+        }

+      }

+      v.Visited = VisitedStatus.Visited;  // there are no cycles from here on

+      return null;

+    }

   }

 }

diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc
index 89a02ce7..fbf9c361 100644
--- a/Source/Dafny/Translator.ssc
+++ b/Source/Dafny/Translator.ssc
@@ -425,7 +425,7 @@ namespace Microsoft.Dafny {
       args.Add(new Bpl.IdentifierExpr(f.tok, bv));

       Bpl.BoundVariable bvThis;

       Bpl.Expr bvThisIdExpr;

-      if (f.IsClass) {

+      if (f.IsStatic) {

         bvThis = null;

         bvThisIdExpr = null;

       } else {

@@ -460,8 +460,8 @@ namespace Microsoft.Dafny {
       }

       

       Bpl.Expr ante = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr);

-      if (!f.IsClass) {

-        assert bvThisIdExpr != null;  // set to non-null value above when !f.IsClass

+      if (!f.IsStatic) {

+        assert bvThisIdExpr != null;  // set to non-null value above when !f.IsStatic

         ante = Bpl.Expr.And(Bpl.Expr.Neq(bvThisIdExpr, predef.Null), ante);

       }

       foreach (Expression req in f.Req) {

@@ -495,7 +495,7 @@ namespace Microsoft.Dafny {
       args.Add(new Bpl.IdentifierExpr(f.tok, bv));

       Bpl.BoundVariable bvThis;

       Bpl.Expr bvThisIdExpr;

-      if (f.IsClass) {

+      if (f.IsStatic) {

         bvThis = null;

         bvThisIdExpr = null;

       } else {

@@ -841,7 +841,7 @@ namespace Microsoft.Dafny {
       bvars.Add(h0Var);  bvars.Add(h1Var);

       f0args.Add(h0);

       f1args.Add(h1);

-      if (!f.IsClass) {

+      if (!f.IsStatic) {

         Bpl.BoundVariable thVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType));

         Bpl.Expr th = new Bpl.IdentifierExpr(f.tok, thVar);

         bvars.Add(thVar);

@@ -932,7 +932,7 @@ namespace Microsoft.Dafny {
       ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);

       // parameters of the procedure

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

-      if (!f.IsClass) {

+      if (!f.IsStatic) {

         Bpl.Expr wh = Bpl.Expr.And(

           Bpl.Expr.Neq(new Bpl.IdentifierExpr(f.tok, "this", predef.RefType), predef.Null),

           etran.GoodRef(f.tok, new Bpl.IdentifierExpr(f.tok, "this", predef.RefType), Resolver.GetThisType(f.tok, (!)f.EnclosingClass)));

@@ -1025,7 +1025,7 @@ namespace Microsoft.Dafny {
         assert e.Function != null;  // follows from the fact that expr has been successfully resolved

         // check well-formedness of receiver

         Bpl.Expr r = IsTotal(e.Receiver, etran);

-        if (!e.Function.IsClass && !(e.Receiver is ThisExpr)) {

+        if (!e.Function.IsStatic && !(e.Receiver is ThisExpr)) {

           r = BplAnd(r, Bpl.Expr.Neq(etran.TrExpr(e.Receiver), predef.Null));

         }

         // check well-formedness of the other parameters

@@ -1180,7 +1180,7 @@ namespace Microsoft.Dafny {
         assert e.Function != null;  // follows from the fact that expr has been successfully resolved

         // check well-formedness of receiver

         CheckWellformed(e.Receiver, func, Position.Neither, locals, builder, etran);

-        if (!e.Function.IsClass && !(e.Receiver is ThisExpr)) {

+        if (!e.Function.IsStatic && !(e.Receiver is ThisExpr)) {

           CheckNonNull(expr.tok, e.Receiver, builder, etran);

         }

         // check well-formedness of the other parameters

@@ -1218,15 +1218,17 @@ namespace Microsoft.Dafny {
           builder.Add(Assert(expr.tok, q, "insufficient reads clause to invoke function"));

   

           // finally, check that the decreases measure goes down

-          List<Expression!> contextDecreases = func.Decreases;

-          if (contextDecreases.Count == 0) {

-            contextDecreases = func.Reads;  // use its reads clause instead

-          }

-          List<Expression!> calleeDecreases = e.Function.Decreases;

-          if (calleeDecreases.Count == 0) {

-            calleeDecreases = e.Function.Reads;  // use its reads clause instead

+          if (((!)e.Function.EnclosingClass).Module == ((!)func.EnclosingClass).Module) {

+            List<Expression!> contextDecreases = func.Decreases;

+            if (contextDecreases.Count == 0) {

+              contextDecreases = func.Reads;  // use its reads clause instead

+            }

+            List<Expression!> calleeDecreases = e.Function.Decreases;

+            if (calleeDecreases.Count == 0) {

+              calleeDecreases = e.Function.Reads;  // use its reads clause instead

+            }

+            CheckCallTermination(expr.tok, contextDecreases, calleeDecreases, e.Receiver, substMap, etran, builder);

           }

-          CheckCallTermination(expr.tok, contextDecreases, calleeDecreases, e.Receiver, substMap, etran, builder);

         }

       } else if (expr is DatatypeValue) {

         DatatypeValue dtv = (DatatypeValue)expr;

@@ -1419,7 +1421,7 @@ namespace Microsoft.Dafny {
       Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);

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

       args.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$heap", predef.HeapType), true));

-      if (!f.IsClass) {

+      if (!f.IsStatic) {

         args.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType), true));

       }

       foreach (Formal p in f.Formals) {

@@ -1450,7 +1452,7 @@ namespace Microsoft.Dafny {
       

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

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

-      if (!m.IsClass) {

+      if (!m.IsStatic) {

         Bpl.Expr wh = Bpl.Expr.And(

           Bpl.Expr.Neq(new Bpl.IdentifierExpr(m.tok, "this", predef.RefType), predef.Null),

           etran.GoodRef(m.tok, new Bpl.IdentifierExpr(m.tok, "this", predef.RefType), Resolver.GetThisType(m.tok, (!)m.EnclosingClass)));

@@ -1786,7 +1788,7 @@ namespace Microsoft.Dafny {
         AddComment(builder, stmt, "call statement");

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

         assert s.Method != null;  // follows from the fact that stmt has been successfully resolved

-        if (!s.Method.IsClass) {

+        if (!s.Method.IsStatic) {

           ins.Add(etran.TrExpr(s.Receiver));

         }

 

@@ -1843,9 +1845,9 @@ namespace Microsoft.Dafny {
         }

 

         // Check termination

-        if (currentMethod.Decreases.Count == 0 || exists{Expression e in currentMethod.Decreases; e is WildcardExpr}) {

+        if (exists{Expression e in currentMethod.Decreases; e is WildcardExpr}) {

           // omit termination checking for calls in this context

-        } else {

+        } else if (((!)currentMethod.EnclosingClass).Module == ((!)s.Method.EnclosingClass).Module) {

           CheckCallTermination(stmt.Tok, currentMethod.Decreases, s.Method.Decreases, s.Receiver, substMap, etran, builder);

         }

 

@@ -2575,7 +2577,7 @@ namespace Microsoft.Dafny {
           Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(expr.tok, nm, translator.TrType((!)e.Type));

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

           args.Add(HeapExpr);

-          if (!e.Function.IsClass) {

+          if (!e.Function.IsStatic) {

             args.Add(TrExpr(e.Receiver));

           }

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

@@ -2795,7 +2797,7 @@ namespace Microsoft.Dafny {
         Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(e.tok, ((!)e.Function).FullName + "#use", translator.TrType((!)e.Type));

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

         args.Add(HeapExpr);

-        if (!e.Function.IsClass) {

+        if (!e.Function.IsStatic) {

           args.Add(TrExpr(e.Receiver));

         }

         foreach (Expression ee in e.Args) {

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 3186ae01..5dadda4b 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -12,23 +12,23 @@ class MyClass<T, U> {
     ensures t == t;

     ensures old(null) != this;

   {

-    x := 12;

-    while (x < 100)

-      invariant x <= 100;

-    {

-      x := x + 17;

-      if (x % 20 == 3) {

-        x := this.x + 1;

-      } else {

-        this.x := x + 0;

+      x := 12;

+      while (x < 100)

+        invariant x <= 100;

+      {

+        x := x + 17;

+        if (x % 20 == 3) {

+          x := this.x + 1;

+        } else {

+          this.x := x + 0;

+        }

+        call t, u, v := M(true, lotsaObjects)

+        var to: MyClass<T,U>;

+        call to, u, v := M(true, lotsaObjects)

+        call to, u, v := to.M(true, lotsaObjects)

+        assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];

       }

-      call t, u, v := M(true, lotsaObjects)

-      var to: MyClass<T,U>;

-      call to, u, v := M(true, lotsaObjects)

-      call to, u, v := to.M(true, lotsaObjects)

-      assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];

     }

-  }

 

   function F(x: int, y: int, h: WildData, k: WildData): WildData

   {

@@ -122,144 +122,154 @@ Execution trace:
     (0,0): anon0

     (0,0): anon4_Else

     (0,0): anon3

-SmallTests.dfy(162,7): Error: possible division by zero

+

+Dafny program verifier finished with 22 verified, 9 errors

+

+-------------------- Definedness.dfy --------------------

+Definedness.dfy(8,7): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(169,16): Error: possible division by zero

+Definedness.dfy(15,16): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(178,16): Error: target object may be null

+Definedness.dfy(24,16): Error: target object may be null

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(179,21): Error: target object may be null

+Definedness.dfy(25,21): Error: target object may be null

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-SmallTests.dfy(180,17): Error: possible division by zero

+Definedness.dfy(26,17): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(187,16): Error: target object may be null

+Definedness.dfy(33,16): Error: target object may be null

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(204,18): Error: target object may be null

+Definedness.dfy(50,18): Error: target object may be null

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(209,18): Error: target object may be null

+Definedness.dfy(55,18): Error: target object may be null

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(231,9): Error: LHS expression must be well defined

+Definedness.dfy(77,9): Error: LHS expression must be well defined

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(232,12): Error: LHS expression must be well defined

+Definedness.dfy(78,12): Error: LHS expression must be well defined

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(233,7): Error: RHS expression must be well defined

+Definedness.dfy(79,7): Error: RHS expression must be well defined

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(238,18): Error: assert condition must be well defined

+Definedness.dfy(84,18): Error: assert condition must be well defined

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(239,5): Error: assume condition must be well defined

+Definedness.dfy(85,5): Error: assume condition must be well defined

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(244,16): Error: if guard must be well defined

+Definedness.dfy(90,16): Error: if guard must be well defined

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(251,19): Error: loop guard must be well defined

+Definedness.dfy(97,19): Error: loop guard must be well defined

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(251,5): anon8_LoopHead

+    Definedness.dfy(97,5): anon8_LoopHead

     (0,0): anon8_LoopBody

-    SmallTests.dfy(251,5): anon9_Else

+    Definedness.dfy(97,5): anon9_Else

     (0,0): anon3

-SmallTests.dfy(260,23): Error: decreases expression must be well defined at top of each loop iteration

+Definedness.dfy(106,23): Error: decreases expression must be well defined at top of each loop iteration

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(259,5): anon13_LoopHead

+    Definedness.dfy(105,5): anon13_LoopHead

     (0,0): anon13_LoopBody

     (0,0): anon14_Then

-SmallTests.dfy(266,17): Error: decreases expression must be well defined at top of each loop iteration

+Definedness.dfy(112,17): Error: decreases expression must be well defined at top of each loop iteration

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(259,5): anon13_LoopHead

+    Definedness.dfy(105,5): anon13_LoopHead

     (0,0): anon13_LoopBody

-    SmallTests.dfy(259,5): anon14_Else

+    Definedness.dfy(105,5): anon14_Else

     (0,0): anon3

     (0,0): anon15_Then

     (0,0): anon6

-    SmallTests.dfy(265,5): anon16_LoopHead

+    Definedness.dfy(111,5): anon16_LoopHead

     (0,0): anon16_LoopBody

     (0,0): anon17_Then

-SmallTests.dfy(276,22): Error: loop invariant must be well defined

+Definedness.dfy(122,22): Error: loop invariant must be well defined

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(275,5): anon7_LoopHead

+    Definedness.dfy(121,5): anon7_LoopHead

     (0,0): anon7_LoopBody

     (0,0): anon8_Then

-SmallTests.dfy(276,22): Error BP5004: This loop invariant might not hold on entry.

+Definedness.dfy(122,22): Error BP5004: This loop invariant might not hold on entry.

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(277,17): Error: decreases expression must be well defined at top of each loop iteration

+Definedness.dfy(123,17): Error: decreases expression must be well defined at top of each loop iteration

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(275,5): anon7_LoopHead

+    Definedness.dfy(121,5): anon7_LoopHead

     (0,0): anon7_LoopBody

     (0,0): anon8_Then

-SmallTests.dfy(286,24): Error: loop guard must be well defined

+Definedness.dfy(132,24): Error: loop guard must be well defined

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(286,5): anon7_LoopHead

+    Definedness.dfy(132,5): anon7_LoopHead

     (0,0): anon7_LoopBody

-    SmallTests.dfy(286,5): anon8_Else

+    Definedness.dfy(132,5): anon8_Else

     (0,0): anon3

-SmallTests.dfy(305,24): Error: loop guard must be well defined

+Definedness.dfy(151,24): Error: loop guard must be well defined

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(299,5): anon13_LoopHead

+    Definedness.dfy(145,5): anon13_LoopHead

     (0,0): anon13_LoopBody

-    SmallTests.dfy(299,5): anon14_Else

+    Definedness.dfy(145,5): anon14_Else

     (0,0): anon3

     (0,0): anon15_Then

     (0,0): anon6

-    SmallTests.dfy(305,5): anon16_LoopHead

+    Definedness.dfy(151,5): anon16_LoopHead

     (0,0): anon16_LoopBody

-    SmallTests.dfy(305,5): anon17_Else

+    Definedness.dfy(151,5): anon17_Else

     (0,0): anon9

-SmallTests.dfy(326,44): Error: loop invariant must be well defined

+Definedness.dfy(172,44): Error: loop invariant must be well defined

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(316,5): anon16_LoopHead

+    Definedness.dfy(162,5): anon16_LoopHead

     (0,0): anon16_LoopBody

-    SmallTests.dfy(316,5): anon17_Else

+    Definedness.dfy(162,5): anon17_Else

     (0,0): anon3

     (0,0): anon18_Then

     (0,0): anon6

-    SmallTests.dfy(324,5): anon19_LoopHead

+    Definedness.dfy(170,5): anon19_LoopHead

     (0,0): anon19_LoopBody

     (0,0): anon20_Then

-SmallTests.dfy(347,21): Error: collection expression must be well defined

+Definedness.dfy(193,21): Error: collection expression must be well defined

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(349,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause

+Definedness.dfy(195,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(351,33): Error: range expression must be well defined

+Definedness.dfy(197,33): Error: range expression must be well defined

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(357,18): Error: RHS of assignment must be well defined

+Definedness.dfy(203,18): Error: RHS of assignment must be well defined

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(366,23): Error: loop invariant must be well defined

+Definedness.dfy(212,23): Error: loop invariant must be well defined

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(364,5): anon7_LoopHead

+    Definedness.dfy(210,5): anon7_LoopHead

     (0,0): anon7_LoopBody

     (0,0): anon8_Then

-SmallTests.dfy(366,23): Error BP5004: This loop invariant might not hold on entry.

+Definedness.dfy(212,23): Error BP5004: This loop invariant might not hold on entry.

 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 43 verified, 38 errors

+Dafny program verifier finished with 21 verified, 29 errors

+

+-------------------- Modules0.dfy --------------------

+Modules0.dfy(13,7): Error: module T named among imports does not exist

+Modules0.dfy(24,7): Error: import graph contains a cycle: H -> I -> J -> G

+Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T

+3 resolution/type errors detected in Modules0.dfy

 

 -------------------- Queue.dfy --------------------

 

diff --git a/Test/dafny0/BinaryTree.dfy b/Test/dafny0/BinaryTree.dfy
index 5f56cf40..276b6c0e 100644
--- a/Test/dafny0/BinaryTree.dfy
+++ b/Test/dafny0/BinaryTree.dfy
@@ -48,7 +48,7 @@ class IntSet {
     footprint := root.footprint + {this};

   }

 

-  class method InsertHelper(x: int, n: Node) returns (m: Node)

+  static method InsertHelper(x: int, n: Node) returns (m: Node)

     requires n == null || n.Valid();

     modifies n.footprint;

     ensures m != null && m.Valid();

diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy
new file mode 100644
index 00000000..4bf6ae30
--- /dev/null
+++ b/Test/dafny0/Definedness.dfy
@@ -0,0 +1,218 @@
+// ----------------- wellformed specifications ----------------------

+

+class SoWellformed {

+  var xyz: int;

+  var next: SoWellformed;

+

+  function F(x: int): int

+  { 5 / x }  // error: possible division by zero

+

+  function G(x: int): int

+    requires 0 < x;

+  { 5 / x }

+

+  function H(x: int): int

+    decreases 5/x;  // error: possible division by zero

+  { 12 }

+

+  function I(x: int): int

+    requires 0 < x;

+    decreases 5/x;

+  { 12 }

+

+  method M(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)

+    requires a.xyz == 7;  // error: not always defined

+    ensures c ==> d.xyz == -7;  // error: not always defined

+    decreases 5 / b;  // error: not always defined

+  {

+    c := false;

+  }

+

+  method N(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)

+    decreases 5 / b;

+    requires a.next != null;  // error: not always defined

+    requires a.next.xyz == 7;  // this is well-defined, given that the previous line is

+    requires b < -2;

+    ensures 0 <= b ==> d.xyz == -7 && !c;

+  {

+    c := true;

+  }

+

+  method O(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)

+    modifies a.next;  // this may not be well-defined, but that's okay for modifies clauses

+  {

+    c := true;

+  }

+

+  method P(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed);

+    requires next != null;

+    modifies this;

+    ensures next.xyz < 100;  // error: may not be well-defined (if body sets next to null)

+

+  method Q(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);

+    requires next != null;

+    modifies s;

+    ensures next.xyz < 100;  // error: may not be well-defined (if this in s and body sets next to null)

+

+  method R(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);

+    requires next != null && this !in s;

+    modifies s;

+    ensures next.xyz < 100;  // fine

+}

+

+// ---------------------- welldefinedness checks for statements -------------------

+

+class StatementTwoShoes {

+  var x: int;

+

+  function method F(b: int): StatementTwoShoes

+    requires 0 <= b;

+  {

+    this

+  }

+

+  method M(p: StatementTwoShoes, a: int)

+    modifies this, p;

+  {

+    p.x := a;  // error: receiver may be null

+    F(a).x := a;  // error: LHS may not be well defined

+    x := F(a-10).x;  // error: RHS may not be well defined

+  }

+

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

+  {

+    assert 5 / a == 5 / a;  // error: expression may not be well defined

+    assume 20 / b == 5;  // error: expression may not be well defined

+  }

+

+  method O(a: int) returns (b: int)

+  {

+    if (20 / a == 5) {  // error: expression may not be well defined

+      b := a;

+    }

+  }

+

+  method P(a: int)

+  {

+    while (20 / a == 5) {  // error: expression may not be well defined

+      break;

+    }

+  }

+

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

+  {

+    var i := 1;

+    while (i < a)

+      decreases F(i), F(a), a - i;  // error: component 1 may not be well defined

+    {

+      i := i + 1;

+    }

+    i := 1;

+    while (i < a)

+      decreases F(b), a - i;  // error: component 0 may not be well defined

+    {

+      i := i + 1;

+    }

+  }

+

+  method R(a: int)

+  {

+    var i := 0;

+    while (i < 100)  // The following produces 3 complaints instead of 1, because loop invariants are not subject to subsumption

+      invariant F(a) != null;  // error: expression may not be well defined, and error: loop invariant may not hold

+      decreases F(a), 100 - i;  // error: component 0 not well defined

+    {

+      i := i + 1;

+    }

+  }

+

+  method S(a: int)

+  {

+    var j := 0;

+    while (20 / a == 5 && j < 100)  // error: guard may not be well defined

+      invariant j <= 100;

+      decreases F(101 - j), 100 - j;

+    {

+      j := j + 1;

+    }

+  }

+

+  method T(a: int)

+    requires a != 0 && 20 / a == 5;

+  {

+    var k := a;

+    var j := 0;

+    while (20 / k == 5 && j < 100)  // fine

+      decreases 100 - j;

+    {

+      j := j + 1;

+    }

+    j := 0;

+    while (20 / k == 5 && j < 100)  // error: guard may not be well defined

+      decreases 100 - j;

+    {

+      havoc k;

+      j := j + 1;

+    }

+  }

+

+  method U()

+  {

+    var i := 0;

+    while (i < 100)

+      invariant i <= 100;

+      decreases 100 - i;

+      invariant F(123 - i) == this;

+    {

+      i := i + 1;

+    }

+    i := 0;

+    while (i < 100)

+      decreases 100 - i;

+      invariant F(if i==77 then -3 else i) == this;  // error: expression may not be well defined

+    {

+      i := i + 1;

+      if (i == 77) { i := i + 1; }

+    }

+  }

+

+  use function G(w: int): int { 5 }

+  function method H(x: int): int;

+

+  method V(s: set<StatementTwoShoes>, a: int, b: int)

+    modifies s;

+  {

+    use G(12 / b);  // fine, because there are no welldefinedness checks on use statements

+    foreach (m in s | m.x < 200)  // s may contain null, but the foreach excludes null

+    {

+      assume 0 <= m.x;

+      assert m.x < 1000;

+      use G(5 / m.x);  // fine, because there are no welldefinedness checks on use statements

+      m.x := m.x + 1;

+    }

+    foreach (m in s + {F(a)})  // error: collection expression may not be well defined

+    {

+      m.x := 5;  // error: possible modifies clause violation

+    }

+    foreach (m in s | F(H(m.x)) == this)  // error: range expression may not be well defined

+    {

+      m.x := H(m.x);

+    }

+    foreach (m in s)

+    {

+      m.x := 100 / m.x;  // error: RhS may not be well defined

+    }

+  }

+

+  method W(x: int)

+  {

+    var i := 0;

+    while (i < 100)

+      // The following line produces two complaints, thanks to the w-encoding of the loop's invariant definedness checking

+      invariant 5 / x != 5 / x;  // error: not well-defined, and error: loop invariant does not hold initially

+      decreases 100 - i;

+    {

+      i := i + 1;

+    }

+  }

+}

diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
new file mode 100644
index 00000000..cf616fba
--- /dev/null
+++ b/Test/dafny0/Modules0.dfy
@@ -0,0 +1,34 @@
+module M {

+  class T { }

+  class U { }

+}

+

+module N {

+  class T { } // error: duplicate class name

+}

+

+module U imports N {  // fine, despite the fact that a class is called U--module names are in their own name space

+}

+

+module V imports T {  // error: T is not a module

+}

+

+module A imports B, M {

+  class Y { }

+}

+

+module B imports N, M {

+  class X { }

+}

+

+module G imports A, M, A, H, B {  // error: cycle in import graph

+}

+

+module H imports A, N, I {

+}

+

+module I imports J {

+}

+

+module J imports G, M {

+}

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 3bf5ed3f..b627df75 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -151,222 +151,3 @@ class Modifies {
     }

   }

 }

-

-// ----------------- wellformed specifications ----------------------

-

-class SoWellformed {

-  var xyz: int;

-  var next: SoWellformed;

-

-  function F(x: int): int

-  { 5 / x }  // error: possible division by zero

-

-  function G(x: int): int

-    requires 0 < x;

-  { 5 / x }

-

-  function H(x: int): int

-    decreases 5/x;  // error: possible division by zero

-  { 12 }

-

-  function I(x: int): int

-    requires 0 < x;

-    decreases 5/x;

-  { 12 }

-

-  method M(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)

-    requires a.xyz == 7;  // error: not always defined

-    ensures c ==> d.xyz == -7;  // error: not always defined

-    decreases 5 / b;  // error: not always defined

-  {

-    c := false;

-  }

-

-  method N(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)

-    decreases 5 / b;

-    requires a.next != null;  // error: not always defined

-    requires a.next.xyz == 7;  // this is well-defined, given that the previous line is

-    requires b < -2;

-    ensures 0 <= b ==> d.xyz == -7 && !c;

-  {

-    c := true;

-  }

-

-  method O(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)

-    modifies a.next;  // this may not be well-defined, but that's okay for modifies clauses

-  {

-    c := true;

-  }

-

-  method P(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed);

-    requires next != null;

-    modifies this;

-    ensures next.xyz < 100;  // error: may not be well-defined (if body sets next to null)

-

-  method Q(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);

-    requires next != null;

-    modifies s;

-    ensures next.xyz < 100;  // error: may not be well-defined (if this in s and body sets next to null)

-

-  method R(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);

-    requires next != null && this !in s;

-    modifies s;

-    ensures next.xyz < 100;  // fine

-}

-

-// ---------------------- welldefinedness checks for statements -------------------

-

-class StatementTwoShoes {

-  var x: int;

-

-  function method F(b: int): StatementTwoShoes

-    requires 0 <= b;

-  {

-    this

-  }

-

-  method M(p: StatementTwoShoes, a: int)

-    modifies this, p;

-  {

-    p.x := a;  // error: receiver may be null

-    F(a).x := a;  // error: LHS may not be well defined

-    x := F(a-10).x;  // error: RHS may not be well defined

-  }

-

-  method N(a: int, b: int)

-  {

-    assert 5 / a == 5 / a;  // error: expression may not be well defined

-    assume 20 / b == 5;  // error: expression may not be well defined

-  }

-

-  method O(a: int) returns (b: int)

-  {

-    if (20 / a == 5) {  // error: expression may not be well defined

-      b := a;

-    }

-  }

-

-  method P(a: int)

-  {

-    while (20 / a == 5) {  // error: expression may not be well defined

-      break;

-    }

-  }

-

-  method Q(a: int, b: int)

-  {

-    var i := 1;

-    while (i < a)

-      decreases F(i), F(a), a - i;  // error: component 1 may not be well defined

-    {

-      i := i + 1;

-    }

-    i := 1;

-    while (i < a)

-      decreases F(b), a - i;  // error: component 0 may not be well defined

-    {

-      i := i + 1;

-    }

-  }

-

-  method R(a: int)

-  {

-    var i := 0;

-    while (i < 100)  // The following produces 3 complaints instead of 1, because loop invariants are not subject to subsumption

-      invariant F(a) != null;  // error: expression may not be well defined, and error: loop invariant may not hold

-      decreases F(a), 100 - i;  // error: component 0 not well defined

-    {

-      i := i + 1;

-    }

-  }

-

-  method S(a: int)

-  {

-    var j := 0;

-    while (20 / a == 5 && j < 100)  // error: guard may not be well defined

-      invariant j <= 100;

-      decreases F(101 - j), 100 - j;

-    {

-      j := j + 1;

-    }

-  }

-

-  method T(a: int)

-    requires a != 0 && 20 / a == 5;

-  {

-    var k := a;

-    var j := 0;

-    while (20 / k == 5 && j < 100)  // fine

-      decreases 100 - j;

-    {

-      j := j + 1;

-    }

-    j := 0;

-    while (20 / k == 5 && j < 100)  // error: guard may not be well defined

-      decreases 100 - j;

-    {

-      havoc k;

-      j := j + 1;

-    }

-  }

-

-  method U()

-  {

-    var i := 0;

-    while (i < 100)

-      invariant i <= 100;

-      decreases 100 - i;

-      invariant F(123 - i) == this;

-    {

-      i := i + 1;

-    }

-    i := 0;

-    while (i < 100)

-      decreases 100 - i;

-      invariant F(if i==77 then -3 else i) == this;  // error: expression may not be well defined

-    {

-      i := i + 1;

-      if (i == 77) { i := i + 1; }

-    }

-  }

-

-  use function G(w: int): int { 5 }

-  function method H(x: int): int;

-

-  method V(s: set<StatementTwoShoes>, a: int, b: int)

-    modifies s;

-  {

-    use G(12 / b);  // fine, because there are no welldefinedness checks on use statements

-    foreach (m in s | m.x < 200)  // s may contain null, but the foreach excludes null

-    {

-      assume 0 <= m.x;

-      assert m.x < 1000;

-      use G(5 / m.x);  // fine, because there are no welldefinedness checks on use statements

-      m.x := m.x + 1;

-    }

-    foreach (m in s + {F(a)})  // error: collection expression may not be well defined

-    {

-      m.x := 5;  // error: possible modifies clause violation

-    }

-    foreach (m in s | F(H(m.x)) == this)  // error: range expression may not be well defined

-    {

-      m.x := H(m.x);

-    }

-    foreach (m in s)

-    {

-      m.x := 100 / m.x;  // error: RhS may not be well defined

-    }

-  }

-

-  method W(x: int)

-  {

-    var i := 0;

-    while (i < 100)

-      // The following line produces two complaints, thanks to the w-encoding of the loop's invariant definedness checking

-      invariant 5 / x != 5 / x;  // error: not well-defined, and error: loop invariant does not hold initially

-      decreases 100 - i;

-    {

-      i := i + 1;

-    }

-  }

-}

diff --git a/Test/dafny0/SumOfCubes.dfy b/Test/dafny0/SumOfCubes.dfy
index 389c885c..42a82fe6 100644
--- a/Test/dafny0/SumOfCubes.dfy
+++ b/Test/dafny0/SumOfCubes.dfy
@@ -1,12 +1,12 @@
 class SumOfCubes {

-  class use function SumEmUp(n: int, m: int): int

+  static use function SumEmUp(n: int, m: int): int

     requires 0 <= n && n <= m;

     decreases m - n;

   {

     if m == n then 0 else n*n*n + SumEmUp(n+1, m)

   }

 

-  class method Socu(n: int, m: int) returns (r: int)

+  static method Socu(n: int, m: int) returns (r: int)

     requires 0 <= n && n <= m;

     ensures r == SumEmUp(n, m);

   {

@@ -16,7 +16,7 @@ class SumOfCubes {
     call Lemma0(n, m);

   }

 

-  class method SocuFromZero(k: int) returns (r: int)

+  static method SocuFromZero(k: int) returns (r: int)

     requires 0 <= k;

     ensures r == SumEmUp(0, k);

   {

@@ -25,7 +25,7 @@ class SumOfCubes {
     call Lemma1(k);

   }

 

-  ghost class method Lemma0(n: int, m: int)

+  ghost static method Lemma0(n: int, m: int)

     requires 0 <= n && n <= m;

     ensures SumEmUp(n, m) == SumEmUp(0, m) - SumEmUp(0, n);

   {

@@ -42,14 +42,14 @@ class SumOfCubes {
     call Lemma3(0, k);

   }

 

-  class use function GSum(k: int): int

+  static use function GSum(k: int): int

     requires 0 <= k;

     decreases k;

   {

     if k == 0 then 0 else GSum(k-1) + k-1

   }

 

-  ghost class method Gauss(k: int) returns (r: int)

+  ghost static method Gauss(k: int) returns (r: int)

     requires 0 <= k;

     ensures r == GSum(k);

   {

@@ -57,7 +57,7 @@ class SumOfCubes {
     call Lemma2(k);

   }

 

-  ghost class method Lemma1(k: int)

+  ghost static method Lemma1(k: int)

     requires 0 <= k;

     ensures SumEmUp(0, k) == GSum(k) * GSum(k);

   {

@@ -73,7 +73,7 @@ class SumOfCubes {
     call Lemma3(0, k);

   }

 

-  ghost class method Lemma2(k: int)

+  ghost static method Lemma2(k: int)

     requires 0 <= k;

     ensures 2 * GSum(k) == k * (k - 1);

   {

@@ -87,14 +87,14 @@ class SumOfCubes {
     }

   }

 

-  class use function SumEmDown(n: int, m: int): int

+  static use function SumEmDown(n: int, m: int): int

     requires 0 <= n && n <= m;

     decreases m;

   {

     if m == n then 0 else SumEmDown(n, m-1) + (m-1)*(m-1)*(m-1)

   }

 

-  ghost class method Lemma3(n: int, m: int)

+  ghost static method Lemma3(n: int, m: int)

     requires 0 <= n && n <= m;

     ensures SumEmUp(n, m) == SumEmDown(n, m);

   {

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index c1837b43..2bec0a4d 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -17,7 +17,8 @@ for %%f in (BQueue.bpl) do (
   %BPLEXE% %* %%f

 )

 

-for %%f in (TypeTests.dfy SmallTests.dfy Queue.dfy ListCopy.dfy

+for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy

+            Modules0.dfy Queue.dfy ListCopy.dfy

             BinaryTree.dfy ListReverse.dfy ListContents.dfy

             SchorrWaite.dfy Termination.dfy Use.dfy DTypes.dfy

             TypeParameters.dfy Datatypes.dfy UnboundedStack.dfy

diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index 3b10c560..da7e59e7 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -31,6 +31,7 @@
 

    `(,(dafny-regexp-opt '(

         "class" "datatype" "function" "frame" "ghost" "var" "method"

+        "module" "imports" "static"

         "returns" "requires" "ensures" "modifies" "reads" "free"

         "invariant" "decreases"

         )) . font-lock-builtin-face)

diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 23ea36fb..641584b6 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -7,8 +7,8 @@
 \lstdefinelanguage{dafny}{

   morekeywords={class,datatype,bool,int,object,set,seq,%

       function,returns,

-      ghost,var,

-      method,in,

+      ghost,var,static,

+      method,module,imports,in,

       requires,modifies,ensures,reads,decreases,free,

       % expressions

       match,case,false,true,null,old,fresh,this,