Dafny: Added if-then-else expressions (replacing and extending the previous boolean-only if-then-else expressions)

Dafny: Added 'class' functions and methods (i.e., functions and methods with a receiver parameter)
Dafny grammar changes:  Tthe 'use' keyword now goes before 'function' (akin to 'ghost' and 'class'), and quantifier triggers now go before the '::'
Dafny: Check for division-by-zero for both '/' and '%'

14 files changed, 661 insertions, 501 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 60de3d84..50433b54 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -153,6 +153,14 @@ axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) }
     Seq#Index(Seq#Drop(s,n), j) == Seq#Index(s, j+n));

 

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

+// -- If then else -----------------------------------------------

+// ---------------------------------------------------------------

+

+function $ite<T>(bool, T, T): T;

+axiom (forall<T> g: bool, a,b: T :: { $ite(g,a,b) }

+  (g ==> $ite(g,a,b) == a) && (!g ==> $ite(g,a,b) == b));

+

+// ---------------------------------------------------------------

 // -- Boxing and unboxing ----------------------------------------

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

 

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index a6eba750..9e30ab85 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -27,6 +27,12 @@ static Attributes.Argument! dummyAttrArg = new Attributes.Argument("dummyAttrArg
 static Scope<string>! parseVarScope = new Scope<string>();

 static int anonymousIds = 0;

 

+struct MemberModifiers {

+  public bool IsGhost;

+  public bool IsClass;

+  public bool IsUse;

+}

+

 // helper routine for parsing call statements

 private static void RecordCallLhs(IdentifierExpr! e,

                                   List<IdentifierExpr!>! lhs,

@@ -135,11 +141,15 @@ ClassDecl<out ClassDecl! c>
 ClassMemberDecl<List<MemberDecl!\>! mm>

 = (. Method! m;

      Function! f;

+     MemberModifiers mmod = new MemberModifiers();

   .)

-  ( FieldDecl<mm>

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

-  | MethodDecl<out m>                      (. mm.Add(m); .)

-  | FrameDecl

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

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

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

+  }

+  ( FieldDecl<mmod, mm>

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

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

   )

   .

 

@@ -176,15 +186,17 @@ DatatypeMemberDecl<List<DatatypeCtor!\>! ctors>
   ";"

   .

 

-FieldDecl<List<MemberDecl!\>! mm>

+FieldDecl<MemberModifiers mmod, List<MemberDecl!\>! mm>

 = (. Attributes attrs = null;

      Token! id;  Type! ty;

   .)

-  [ "ghost" ]

   "var"

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

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

+  .)

   { Attribute<ref attrs> }

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

-  { "," IdentType<out id, out ty>                   (. mm.Add(new Field(id, id.val, ty, attrs)); .)

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

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

   }

   ";"

   .

@@ -237,21 +249,9 @@ GenericParameters<List<TypeParameter!\>! typeArgs>
   ">"

   .

 

-FrameDecl

-= (. Token! id;

-     Attributes attrs = null;

-  .)

-  "frame"

-  { Attribute<ref attrs> }

-  Ident<out id>

-  "{"

-       /* TBD */

-  "}"

-  .

-

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

 

-MethodDecl<out Method! m>

+MethodDecl<MemberModifiers mmod, out Method! m>

 = (. Token! id;

      Attributes attrs = null;

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

@@ -263,6 +263,9 @@ MethodDecl<out Method! m>
      Statement! bb;  Statement body = null;

   .)

   "method"

+  (. if (mmod.IsGhost) { SemErr(token, "methods cannot be declared 'ghost'"); }

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

+  .)

   { Attribute<ref attrs> }

   Ident<out id>

   [ GenericParameters<typeArgs> ]

@@ -277,7 +280,7 @@ MethodDecl<out Method! m>
   )

   

   (. parseVarScope.PopMarker();

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

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

   .)

   .

 

@@ -369,7 +372,7 @@ GenericInstantiation<List<Type!\>! gt>
 

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

 

-FunctionDecl<out Function! f>

+FunctionDecl<MemberModifiers mmod, out Function! f>

 = (. Attributes attrs = null;

      Token! id;

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

@@ -379,11 +382,11 @@ FunctionDecl<out Function! f>
      List<Expression!> reads = new List<Expression!>();

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

      Expression! bb;  Expression body = null;

-     bool use = false;

   .)

   "function"

+  (. if (mmod.IsGhost) { SemErr(token, "functions cannot be declared 'ghost'"); }

+  .)

   { Attribute<ref attrs> }

-  [ "use"   (. use = true; .) ]

   Ident<out id> 

   [ GenericParameters<typeArgs> ]

   (. parseVarScope.PushMarker(); .)

@@ -396,7 +399,7 @@ FunctionDecl<out Function! f>
     FunctionBody<out bb>                (. body = bb; .)

   )

   (. parseVarScope.PopMarker();

-     f = new Function(id, id.val, use, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);

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

   .)

   .

 

@@ -434,33 +437,12 @@ PossiblyWildExpression<out Expression! e>
 FunctionBody<out Expression! e>

 = (. e = dummyExpr; .)

   "{"

-  ( IfThenElseExpr<out e>

-  | MatchExpression<out e>

+  ( MatchExpression<out e>

   | Expression<out e>

   )

   "}"

   .

   

-ExtendedExpr<out Expression! e>

-= (. e = dummyExpr; .)

-  "{"

-  ( IfThenElseExpr<out e>

-  | Expression<out e>

-  )

-  "}"

-  .

-  

-IfThenElseExpr<out Expression! e>

-= (. Token! x;  Expression! e0;  Expression! e1 = dummyExpr; .)

-  "if"                               (. x = token; .)

-  "(" Expression<out e> ")"

-  ExtendedExpr<out e0>

-  "else"

-  ( IfThenElseExpr<out e1>

-  | ExtendedExpr<out e1>

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

-  .

-

 MatchExpression<out Expression! e>

 = (. Token! x;

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

@@ -586,7 +568,7 @@ HavocStmt<out Statement! s>
   .

 

 LhsExpr<out Expression! e>

-= Expression<out e>                    /* TODO: restrict LHS further */

+= SelectExpression<out e>

   .

 

 VarDeclStmts<List<Statement!\>! ss>

@@ -773,8 +755,20 @@ UseStmt<out Statement! s>
   .

 

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

+Expression<out Expression! e>

+= (. Token! x;  Expression! e0;  Expression! e1 = dummyExpr;

+     e = dummyExpr;

+  .)

+  ( "if"                               (. x = token; .)

+    Expression<out e>

+    "then" Expression<out e0>

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

+  | EquivExpression<out e>

+  )

+  .

 

-Expression<out Expression! e0>

+/*------------------------------------------------------------------------*/

+EquivExpression<out Expression! e0>

 = (. Token! x;  Expression! e1; .)

   ImpliesExpression<out e0>

   { EquivOp                                    (. x = token; .)

@@ -908,16 +902,6 @@ ConstAtomExpression<out Expression! e>
   | "|"                                        (. x = token; .)

       Expression<out e>                        (. e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); .)

     "|"

-  /* Note, the following open-curly-brace causes grammar ambiguities that result in two Coco warnings.

-     One of these is the confusion between BlockStmt and AssignStmt, the former starting with an open

-     curly brace and the latter starting with a left-hand side Expression, which syntactically can

-     start with an open curly brace.  The other is the confusion between a quantifier's triggers/attributes

-     and the quantifier's body.  The disamiguation I've chosen involves giving priority to BlockStmt

-     (since no semantically legal AssignStmt can have a set constructor as its left-hand side) and to

-     triggers/attributes (which, unfortunately, changes what programs are syntactically allowed, but there

-     is a simple workaround, which is for a user to put parentheses around any quantifier body that begins

-     with a set constructor.

-  */

   | "{"                                        (. x = token;  elements = new List<Expression!>(); .)

       [ Expressions<elements> ]                (. e = new SetDisplayExpr(x, elements); .)

     "}"

@@ -1042,15 +1026,8 @@ QuantifierGuts<out Expression! q>
   { ","

     IdentTypeOptional<out bv>                  (. bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); .)

   }

-  QSep

-  /* The grammar is ambiguous in how to resolve triggers/attributes versus the expression body.

-     However, the loop generated by Coco for the next two lines of grammar declarations is still

-     fine--it will loop, picking up as many triggers/attributes it can before going on to parse an

-     expression.  This seems good, because there's a simple workaround for quantifier bodies that

-     begin with a set constructor: simply put parentheses around the quantifier body.  See also

-     the Note in production ConstAtomExpression.

-  */

   { AttributeOrTrigger<ref attrs, ref trigs> }

+  QSep

   Expression<out body>

   (. if (univ) {

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

diff --git a/Dafny/DafnyAst.ssc b/Dafny/DafnyAst.ssc
index 38c3b87d..01e55cfd 100644
--- a/Dafny/DafnyAst.ssc
+++ b/Dafny/DafnyAst.ssc
@@ -391,9 +391,11 @@ namespace Microsoft.Dafny
   }

   

   public class Field : MemberDecl {

+    public readonly bool IsGhost;

     public readonly Type! Type;

     

-    public Field(Token! tok, string! name, Type! type, Attributes attributes) {

+    public Field(Token! tok, string! name, bool isGhost, Type! type, Attributes attributes) {

+      IsGhost = isGhost;

       Type = type;

       base(tok, name, attributes);

     }

@@ -458,7 +460,8 @@ namespace Microsoft.Dafny
   }

   

   public class Function : MemberDecl, TypeParameter.ParentType {

-    public readonly bool Use;

+    public readonly bool IsClass;

+    public readonly bool IsUse;

     public readonly List<TypeParameter!>! TypeArgs;

     public readonly List<Formal!>! Formals;

     public readonly Type! ResultType;

@@ -467,9 +470,10 @@ namespace Microsoft.Dafny
     public readonly List<Expression!>! Decreases;

     public readonly Expression Body;  // an extended expression

     

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

+    public Function(Token! tok, string! name, bool isClass, 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.Use = use;

+      this.IsClass = isClass;

+      this.IsUse = isUse;

       this.TypeArgs = typeArgs;

       this.Formals = formals;

       this.ResultType = resultType;

@@ -482,6 +486,7 @@ namespace Microsoft.Dafny
   }

   

   public class Method : MemberDecl, TypeParameter.ParentType {

+    public readonly bool IsClass;

     public readonly List<TypeParameter!>! TypeArgs;

     public readonly List<Formal!>! Ins;

     public readonly List<Formal!>! Outs;

@@ -491,11 +496,13 @@ namespace Microsoft.Dafny
     public readonly Statement Body;

     

     public Method(Token! tok, string! name,

+                  bool isClass,

                   [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] Statement body,

                   Attributes attributes) {

+      this.IsClass = isClass;

       this.TypeArgs = typeArgs;

       this.Ins = ins;

       this.Outs = outs;

@@ -977,7 +984,7 @@ namespace Microsoft.Dafny
   public class UseExpr : FunctionCallExpr {

     [NotDelayed] [Captured]

     public UseExpr(FunctionCallExpr! fce)

-      requires fce.Function != null && fce.Function.Use;

+      requires fce.Function != null && fce.Function.IsUse;

     {

       base(fce.tok, fce.Name, fce.Receiver, new List<Expression!>(fce.Args));

       this.Function = fce.Function;

@@ -1115,7 +1122,7 @@ namespace Microsoft.Dafny
     }

   }

   

-  public class ITEExpr : Expression {  // an ITEExpr is an "extended expression" and is only allowed in certain places

+  public class ITEExpr : Expression {

     public readonly Expression! Test;

     public readonly Expression! Thn;

     public readonly Expression! Els;

diff --git a/Dafny/Parser.ssc b/Dafny/Parser.ssc
index 50079f11..76bb32bc 100644
--- a/Dafny/Parser.ssc
+++ b/Dafny/Parser.ssc
@@ -25,6 +25,12 @@ static Attributes.Argument! dummyAttrArg = new Attributes.Argument("dummyAttrArg
 static Scope<string>! parseVarScope = new Scope<string>();

 static int anonymousIds = 0;

 

+struct MemberModifiers {

+  public bool IsGhost;

+  public bool IsClass;

+  public bool IsUse;

+}

+

 // helper routine for parsing call statements

 private static void RecordCallLhs(IdentifierExpr! e,

                                   List<IdentifierExpr!>! lhs,

@@ -133,7 +139,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 	

 	static void Dafny() {

 		ClassDecl! c; DatatypeDecl! dt; 

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

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

 			if (t.kind == 4) {

 				ClassDecl(out c);

 				theClasses.Add(c); 

@@ -156,7 +162,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (t.kind == 13) {

+		if (t.kind == 14) {

 			GenericParameters(typeArgs);

 		}

 		Expect(5);

@@ -173,12 +179,12 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		List<TypeParameter!> typeArgs = new List<TypeParameter!>();

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

 		

-		Expect(7);

+		Expect(9);

 		while (t.kind == 5) {

 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (t.kind == 13) {

+		if (t.kind == 14) {

 			GenericParameters(typeArgs);

 		}

 		Expect(5);

@@ -202,56 +208,67 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 

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

 		Token! id; 

-		Expect(13);

+		Expect(14);

 		Ident(out id);

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

-		while (t.kind == 11) {

+		while (t.kind == 12) {

 			Get();

 			Ident(out id);

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

 		}

-		Expect(14);

+		Expect(15);

 	}

 

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

 		Method! m;

 		Function! f;

+		MemberModifiers mmod = new MemberModifiers();

 		

-		if (t.kind == 9 || t.kind == 10) {

-			FieldDecl(mm);

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

+			if (t.kind == 7) {

+				Get();

+				mmod.IsGhost = true; 

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

+				Get();

+				mmod.IsClass = true; 

+			} else {

+				Get();

+				mmod.IsUse = true; 

+			}

+		}

+		if (t.kind == 11) {

+			FieldDecl(mmod, mm);

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

-			FunctionDecl(out f);

+			FunctionDecl(mmod, out f);

 			mm.Add(f); 

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

-			MethodDecl(out m);

+			MethodDecl(mmod, out m);

 			mm.Add(m); 

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

-			FrameDecl();

 		} else Error(94);

 	}

 

-	static void FieldDecl(List<MemberDecl!>! mm) {

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

 		Attributes attrs = null;

 		Token! id;  Type! ty;

 		

-		if (t.kind == 9) {

-			Get();

-		}

-		Expect(10);

+		Expect(11);

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

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

+		

 		while (t.kind == 5) {

 			Attribute(ref attrs);

 		}

 		IdentType(out id, out ty);

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

-		while (t.kind == 11) {

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

+		while (t.kind == 12) {

 			Get();

 			IdentType(out id, out ty);

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

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

 		}

-		Expect(8);

+		Expect(10);

 	}

 

-	static void FunctionDecl(out Function! f) {

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

 		Attributes attrs = null;

 		Token! id;

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

@@ -261,42 +278,39 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		List<Expression!> reads = new List<Expression!>();

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

 		Expression! bb;  Expression body = null;

-		bool use = false;

 		

 		Expect(29);

+		if (mmod.IsGhost) { SemErr(token, "functions cannot be declared 'ghost'"); }

+		

 		while (t.kind == 5) {

 			Attribute(ref attrs);

 		}

-		if (t.kind == 30) {

-			Get();

-			use = true; 

-		}

 		Ident(out id);

-		if (t.kind == 13) {

+		if (t.kind == 14) {

 			GenericParameters(typeArgs);

 		}

 		parseVarScope.PushMarker(); 

 		Formals(true, formals);

-		Expect(12);

+		Expect(13);

 		Type(out returnType);

-		if (t.kind == 8) {

+		if (t.kind == 10) {

 			Get();

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

+			while (t.kind == 20 || t.kind == 30 || t.kind == 31) {

 				FunctionSpec(reqs, reads, decreases);

 			}

 		} else if (StartOf(2)) {

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

+			while (t.kind == 20 || t.kind == 30 || t.kind == 31) {

 				FunctionSpec(reqs, reads, decreases);

 			}

 			FunctionBody(out bb);

 			body = bb; 

 		} else Error(95);

 		parseVarScope.PopMarker();

-		f = new Function(id, id.val, use, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);

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

 		

 	}

 

-	static void MethodDecl(out Method! m) {

+	static void MethodDecl(MemberModifiers mmod, out Method! m) {

 		Token! id;

 		Attributes attrs = null;

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

@@ -308,11 +322,14 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		Statement! bb;  Statement body = null;

 		

 		Expect(16);

+		if (mmod.IsGhost) { SemErr(token, "methods cannot be declared 'ghost'"); }

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

+		

 		while (t.kind == 5) {

 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (t.kind == 13) {

+		if (t.kind == 14) {

 			GenericParameters(typeArgs);

 		}

 		parseVarScope.PushMarker(); 

@@ -321,7 +338,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			Get();

 			Formals(false, outs);

 		}

-		if (t.kind == 8) {

+		if (t.kind == 10) {

 			Get();

 			while (StartOf(3)) {

 				MethodSpec(req, mod, ens);

@@ -334,23 +351,10 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			body = bb; 

 		} else Error(96);

 		parseVarScope.PopMarker();

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

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

 		

 	}

 

-	static void FrameDecl() {

-		Token! id;

-		Attributes attrs = null;

-		

-		Expect(15);

-		while (t.kind == 5) {

-			Attribute(ref attrs);

-		}

-		Ident(out id);

-		Expect(5);

-		Expect(6);

-	}

-

 	static void DatatypeMemberDecl(List<DatatypeCtor!>! ctors) {

 		Attributes attrs = null;

 		Token! id;

@@ -361,7 +365,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (t.kind == 13) {

+		if (t.kind == 14) {

 			GenericParameters(typeArgs);

 		}

 		parseVarScope.PushMarker(); 

@@ -371,7 +375,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		parseVarScope.PopMarker();

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

 		

-		Expect(8);

+		Expect(10);

 	}

 

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

@@ -380,7 +384,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		if (StartOf(5)) {

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

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

-			while (t.kind == 11) {

+			while (t.kind == 12) {

 				Get();

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

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

@@ -391,7 +395,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 

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

 		Ident(out id);

-		Expect(12);

+		Expect(13);

 		Type(out ty);

 	}

 

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

 		

 		Ident(out id);

-		if (t.kind == 12) {

+		if (t.kind == 13) {

 			Get();

 			Type(out ty);

 			optType = ty; 

@@ -415,7 +419,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 == 12) {

+		if (t.kind == 13) {

 			Get();

 			UserDefinedType udt = ty as UserDefinedType;

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

@@ -473,7 +477,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		if (t.kind == 1) {

 			IdentType(out id, out ty);

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

-			while (t.kind == 11) {

+			while (t.kind == 12) {

 				Get();

 				IdentType(out id, out ty);

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

@@ -490,13 +494,13 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			if (StartOf(6)) {

 				Expression(out e);

 				mod.Add(e); 

-				while (t.kind == 11) {

+				while (t.kind == 12) {

 					Get();

 					Expression(out e);

 					mod.Add(e); 

 				}

 			}

-			Expect(8);

+			Expect(10);

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

 			if (t.kind == 19) {

 				Get();

@@ -505,12 +509,12 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			if (t.kind == 20) {

 				Get();

 				Expression(out e);

-				Expect(8);

+				Expect(10);

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

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

 				Get();

 				Expression(out e);

-				Expect(8);

+				Expect(10);

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

 			} else Error(98);

 		} else Error(99);

@@ -532,28 +536,35 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		parseVarScope.PopMarker(); 

 	}

 

-	static void Expression(out Expression! e0) {

-		Token! x;  Expression! e1; 

-		ImpliesExpression(out e0);

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

-			EquivOp();

+	static void Expression(out Expression! e) {

+		Token! x;  Expression! e0;  Expression! e1 = dummyExpr;

+		e = dummyExpr;

+		

+		if (t.kind == 42) {

+			Get();

 			x = token; 

-			ImpliesExpression(out e1);

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

-		}

+			Expression(out e);

+			Expect(52);

+			Expression(out e0);

+			Expect(43);

+			Expression(out e1);

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

+		} else if (StartOf(8)) {

+			EquivExpression(out e);

+		} else Error(100);

 	}

 

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

 		Type! ty; 

-		Expect(13);

+		Expect(14);

 		Type(out ty);

 		gt.Add(ty); 

-		while (t.kind == 11) {

+		while (t.kind == 12) {

 			Get();

 			Type(out ty);

 			gt.Add(ty); 

 		}

-		Expect(14);

+		Expect(15);

 	}

 

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

@@ -566,11 +577,11 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		} else if (t.kind == 1) {

 			Ident(out tok);

 			gt = new List<Type!>(); 

-			if (t.kind == 13) {

+			if (t.kind == 14) {

 				GenericInstantiation(gt);

 			}

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

-		} else Error(100);

+		} else Error(101);

 	}

 

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

@@ -578,31 +589,29 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		if (t.kind == 20) {

 			Get();

 			Expression(out e);

-			Expect(8);

+			Expect(10);

 			reqs.Add(e); 

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

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

 			Get();

-			if (StartOf(8)) {

+			if (StartOf(9)) {

 				PossiblyWildExpressions(reads);

 			}

-			Expect(8);

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

+			Expect(10);

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

 			Get();

 			Expressions(decreases);

-			Expect(8);

-		} else Error(101);

+			Expect(10);

+		} else Error(102);

 	}

 

 	static void FunctionBody(out Expression! e) {

 		e = dummyExpr; 

 		Expect(5);

-		if (t.kind == 34) {

-			IfThenElseExpr(out e);

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

+		if (t.kind == 33) {

 			MatchExpression(out e);

 		} else if (StartOf(6)) {

 			Expression(out e);

-		} else Error(102);

+		} else Error(103);

 		Expect(6);

 	}

 

@@ -610,7 +619,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		Expression! e; 

 		PossiblyWildExpression(out e);

 		args.Add(e); 

-		while (t.kind == 11) {

+		while (t.kind == 12) {

 			Get();

 			PossiblyWildExpression(out e);

 			args.Add(e); 

@@ -621,7 +630,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		Expression! e; 

 		Expression(out e);

 		args.Add(e); 

-		while (t.kind == 11) {

+		while (t.kind == 12) {

 			Get();

 			Expression(out e);

 			args.Add(e); 

@@ -630,62 +639,34 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 

 	static void PossiblyWildExpression(out Expression! e) {

 		e = dummyExpr; 

-		if (t.kind == 33) {

+		if (t.kind == 32) {

 			Get();

 			e = new WildcardExpr(token); 

 		} else if (StartOf(6)) {

 			Expression(out e);

-		} else Error(103);

-	}

-

-	static void IfThenElseExpr(out Expression! e) {

-		Token! x;  Expression! e0;  Expression! e1 = dummyExpr; 

-		Expect(34);

-		x = token; 

-		Expect(22);

-		Expression(out e);

-		Expect(23);

-		ExtendedExpr(out e0);

-		Expect(35);

-		if (t.kind == 34) {

-			IfThenElseExpr(out e1);

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

-			ExtendedExpr(out e1);

 		} else Error(104);

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

 	}

 

 	static void MatchExpression(out Expression! e) {

 		Token! x;

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

 		

-		Expect(36);

+		Expect(33);

 		x = token; 

 		Expression(out e);

 		if (t.kind == 5) {

 			Get();

 			CaseExpressions(cases);

 			Expect(6);

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

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

 			CaseExpressions(cases);

 		} else Error(105);

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

 	}

 

-	static void ExtendedExpr(out Expression! e) {

-		e = dummyExpr; 

-		Expect(5);

-		if (t.kind == 34) {

-			IfThenElseExpr(out e);

-		} else if (StartOf(6)) {

-			Expression(out e);

-		} else Error(106);

-		Expect(6);

-	}

-

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

 		MatchCase! c; 

-		while (t.kind == 37) {

+		while (t.kind == 34) {

 			CaseExpression(out c);

 			cases.Add(c); 

 		}

@@ -696,7 +677,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		List<BoundVar!> arguments = new List<BoundVar!>();

 		Expression! body;

 		

-		Expect(37);

+		Expect(34);

 		x = token;  parseVarScope.PushMarker(); 

 		Ident(out id);

 		if (t.kind == 22) {

@@ -704,7 +685,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			Ident(out arg);

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

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

-			while (t.kind == 11) {

+			while (t.kind == 12) {

 				Get();

 				Ident(out arg);

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

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

 			Expect(23);

 		}

-		Expect(38);

+		Expect(35);

 		Expression(out body);

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

 		parseVarScope.PopMarker(); 

@@ -724,12 +705,12 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			BlockStmt(out s);

 			ss.Add(s); 

 		}

-		if (StartOf(9)) {

+		if (StartOf(10)) {

 			OneStmt(out s);

 			ss.Add(s); 

-		} else if (t.kind == 9 || t.kind == 10) {

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

 			VarDeclStmts(ss);

-		} else Error(107);

+		} else Error(106);

 	}

 

 	static void OneStmt(out Statement! s) {

@@ -737,112 +718,112 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		s = dummyStmt;  /* to please the compiler */

 		

 		switch (t.kind) {

-		case 51: {

+		case 50: {

 			AssertStmt(out s);

 			break;

 		}

-		case 52: {

+		case 51: {

 			AssumeStmt(out s);

 			break;

 		}

-		case 30: {

+		case 8: {

 			UseStmt(out s);

 			break;

 		}

-		case 1: case 2: case 5: case 22: case 50: case 71: case 74: case 75: case 76: case 77: case 78: case 79: case 81: case 82: case 85: case 86: {

+		case 1: case 22: case 85: case 86: {

 			AssignStmt(out s);

 			break;

 		}

-		case 44: {

+		case 41: {

 			HavocStmt(out s);

 			break;

 		}

-		case 47: {

+		case 46: {

 			CallStmt(out s);

 			break;

 		}

-		case 34: {

+		case 42: {

 			IfStmt(out s);

 			break;

 		}

-		case 45: {

+		case 44: {

 			WhileStmt(out s);

 			break;

 		}

-		case 48: {

+		case 47: {

 			ForeachStmt(out s);

 			break;

 		}

-		case 39: {

+		case 36: {

 			Get();

 			x = token; 

 			Ident(out id);

-			Expect(12);

+			Expect(13);

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

 			break;

 		}

-		case 40: {

+		case 37: {

 			Get();

 			x = token; 

 			if (t.kind == 1) {

 				Ident(out id);

 				label = id.val; 

 			}

-			Expect(8);

+			Expect(10);

 			s = new BreakStmt(x, label); 

 			break;

 		}

-		case 41: {

+		case 38: {

 			Get();

 			x = token; 

-			Expect(8);

+			Expect(10);

 			s = new ReturnStmt(x); 

 			break;

 		}

-		default: Error(108); break;

+		default: Error(107); break;

 		}

 	}

 

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

 		VarDecl! d; 

-		if (t.kind == 9) {

+		if (t.kind == 7) {

 			Get();

 		}

-		Expect(10);

+		Expect(11);

 		IdentTypeRhs(out d);

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

-		while (t.kind == 11) {

+		while (t.kind == 12) {

 			Get();

 			IdentTypeRhs(out d);

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

 		}

-		Expect(8);

+		Expect(10);

 	}

 

 	static void AssertStmt(out Statement! s) {

 		Token! x;  Expression! e; 

-		Expect(51);

+		Expect(50);

 		x = token; 

 		Expression(out e);

-		Expect(8);

+		Expect(10);

 		s = new AssertStmt(x, e); 

 	}

 

 	static void AssumeStmt(out Statement! s) {

 		Token! x;  Expression! e; 

-		Expect(52);

+		Expect(51);

 		x = token; 

 		Expression(out e);

-		Expect(8);

+		Expect(10);

 		s = new AssumeStmt(x, e); 

 	}

 

 	static void UseStmt(out Statement! s) {

 		Token! x;  Expression! e; 

-		Expect(30);

+		Expect(8);

 		x = token; 

 		Expression(out e);

-		Expect(8);

+		Expect(10);

 		s = new UseStmt(x, e); 

 	}

 

@@ -854,7 +835,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		s = dummyStmt;

 		

 		LhsExpr(out lhs);

-		Expect(42);

+		Expect(39);

 		x = token; 

 		AssignRhs(out rhs, out ty);

 		if (rhs != null) {

@@ -864,15 +845,15 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		  s = new AssignStmt(x, lhs, ty);

 		}

 		

-		Expect(8);

+		Expect(10);

 	}

 

 	static void HavocStmt(out Statement! s) {

 		Token! x;  Expression! lhs; 

-		Expect(44);

+		Expect(41);

 		x = token; 

 		LhsExpr(out lhs);

-		Expect(8);

+		Expect(10);

 		s = new AssignStmt(x, lhs); 

 	}

 

@@ -882,11 +863,11 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		List<IdentifierExpr!> lhs = new List<IdentifierExpr!>();

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

 		

-		Expect(47);

+		Expect(46);

 		x = token; 

 		CallStmtSubExpr(out e);

-		if (t.kind == 11 || t.kind == 42) {

-			if (t.kind == 11) {

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

+			if (t.kind == 12) {

 				Get();

 				e = ConvertToLocal(e);

 				if (e is IdentifierExpr) {

@@ -899,12 +880,12 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 				

 				Ident(out id);

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

-				while (t.kind == 11) {

+				while (t.kind == 12) {

 					Get();

 					Ident(out id);

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

 				}

-				Expect(42);

+				Expect(39);

 				CallStmtSubExpr(out e);

 			} else {

 				Get();

@@ -920,7 +901,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 				CallStmtSubExpr(out e);

 			}

 		}

-		Expect(8);

+		Expect(10);

 		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

@@ -938,19 +919,19 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		Statement! s;

 		Statement els = null;

 		

-		Expect(34);

+		Expect(42);

 		x = token; 

 		Guard(out guard);

 		BlockStmt(out thn);

-		if (t.kind == 35) {

+		if (t.kind == 43) {

 			Get();

-			if (t.kind == 34) {

+			if (t.kind == 42) {

 				IfStmt(out s);

 				els = s; 

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

 				BlockStmt(out s);

 				els = s; 

-			} else Error(109);

+			} else Error(108);

 		}

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

 	}

@@ -963,25 +944,25 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		List<Expression!> decreases = new List<Expression!>();

 		Statement! body;

 		

-		Expect(45);

+		Expect(44);

 		x = token; 

 		Guard(out guard);

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

-		while (t.kind == 19 || t.kind == 32 || t.kind == 46) {

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

+		while (t.kind == 19 || t.kind == 31 || t.kind == 45) {

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

 				isFree = false; 

 				if (t.kind == 19) {

 					Get();

 					isFree = true; 

 				}

-				Expect(46);

+				Expect(45);

 				Expression(out e);

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

-				Expect(8);

+				Expect(10);

 			} else {

 				Get();

 				PossiblyWildExpressions(decreases);

-				Expect(8);

+				Expect(10);

 			}

 		}

 		BlockStmt(out body);

@@ -997,31 +978,31 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		AssignStmt bodyAssign = null;

 		

 		parseVarScope.PushMarker(); 

-		Expect(48);

+		Expect(47);

 		x = token;

 		range = new LiteralExpr(x, true);

 		ty = new InferredTypeProxy();

 		

 		Expect(22);

 		Ident(out boundVar);

-		if (t.kind == 12) {

+		if (t.kind == 13) {

 			Get();

 			Type(out ty);

 		}

-		Expect(49);

+		Expect(48);

 		Expression(out collection);

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

-		if (t.kind == 50) {

+		if (t.kind == 49) {

 			Get();

 			Expression(out range);

 		}

 		Expect(23);

 		Expect(5);

-		while (t.kind == 30 || t.kind == 51 || t.kind == 52) {

-			if (t.kind == 51) {

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

+			if (t.kind == 50) {

 				AssertStmt(out s);

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

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

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

 				AssumeStmt(out s);

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

 			} else {

@@ -1029,49 +1010,61 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 				if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } 

 			}

 		}

-		if (StartOf(6)) {

+		if (StartOf(11)) {

 			AssignStmt(out s);

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

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

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

 			HavocStmt(out s);

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

-		} else Error(110);

+		} else Error(109);

 		Expect(6);

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

 		parseVarScope.PopMarker(); 

 	}

 

 	static void LhsExpr(out Expression! e) {

-		Expression(out e);

+		SelectExpression(out e);

 	}

 

 	static void AssignRhs(out Expression e, out Type ty) {

 		Token! x;  Expression! ee;  Type! tt;

 		e = null;  ty = null;

 		

-		if (t.kind == 43) {

+		if (t.kind == 40) {

 			Get();

 			ReferenceType(out x, out tt);

 			ty = tt; 

 		} else if (StartOf(6)) {

 			Expression(out ee);

 			e = ee; 

-		} else Error(111);

+		} else Error(110);

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

 	}

 

+	static void SelectExpression(out Expression! e) {

+		Token! id;  e = dummyExpr; 

+		if (t.kind == 1) {

+			IdentOrFuncExpression(out e);

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

+			ObjectExpression(out e);

+		} else Error(111);

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

+			SelectOrCallSuffix(ref e);

+		}

+	}

+

 	static void IdentTypeRhs(out VarDecl! d) {

 		Token! id;  Type! ty;  Expression! e;

 		Expression rhs = null;  Type newType = null;

 		Type optionalType = null;  DeterminedAssignmentRhs optionalRhs = null;

 		

 		Ident(out id);

-		if (t.kind == 12) {

+		if (t.kind == 13) {

 			Get();

 			Type(out ty);

 			optionalType = ty; 

 		}

-		if (t.kind == 42) {

+		if (t.kind == 39) {

 			Get();

 			AssignRhs(out rhs, out newType);

 		}

@@ -1090,7 +1083,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 	static void Guard(out Expression e) {

 		Expression! ee;  e = null; 

 		Expect(22);

-		if (t.kind == 33) {

+		if (t.kind == 32) {

 			Get();

 			e = null; 

 		} else if (StartOf(6)) {

@@ -1113,6 +1106,17 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		}

 	}

 

+	static void EquivExpression(out Expression! e0) {

+		Token! x;  Expression! e1; 

+		ImpliesExpression(out e0);

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

+			EquivOp();

+			x = token; 

+			ImpliesExpression(out e1);

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

+		}

+	}

+

 	static void ImpliesExpression(out Expression! e0) {

 		Token! x;  Expression! e1; 

 		LogicalExpression(out e0);

@@ -1135,7 +1139,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 	static void LogicalExpression(out Expression! e0) {

 		Token! x;  Expression! e1; 

 		RelationalExpression(out e0);

-		if (StartOf(10)) {

+		if (StartOf(12)) {

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

 				AndOp();

 				x = token; 

@@ -1173,7 +1177,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 	static void RelationalExpression(out Expression! e0) {

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

 		Term(out e0);

-		if (StartOf(11)) {

+		if (StartOf(13)) {

 			RelOp(out x, out op);

 			Term(out e1);

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

@@ -1214,12 +1218,12 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			x = token;  op = BinaryExpr.Opcode.Eq; 

 			break;

 		}

-		case 13: {

+		case 14: {

 			Get();

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

 			break;

 		}

-		case 14: {

+		case 15: {

 			Get();

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

 			break;

@@ -1244,7 +1248,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			x = token;  op = BinaryExpr.Opcode.Disjoint; 

 			break;

 		}

-		case 49: {

+		case 48: {

 			Get();

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

 			break;

@@ -1276,7 +1280,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 	static void Factor(out Expression! e0) {

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

 		UnaryExpression(out e0);

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

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

 			MulOp(out x, out op);

 			UnaryExpression(out e1);

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

@@ -1306,16 +1310,16 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			x = token; 

 			UnaryExpression(out e);

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

-		} else if (StartOf(12)) {

+		} else if (StartOf(11)) {

 			SelectExpression(out e);

-		} else if (StartOf(13)) {

+		} else if (StartOf(14)) {

 			ConstAtomExpression(out e);

 		} else Error(120);

 	}

 

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

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

-		if (t.kind == 33) {

+		if (t.kind == 32) {

 			Get();

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

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

@@ -1335,18 +1339,6 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		} else Error(122);

 	}

 

-	static void SelectExpression(out Expression! e) {

-		Token! id;  e = dummyExpr; 

-		if (t.kind == 1) {

-			IdentOrFuncExpression(out e);

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

-			ObjectExpression(out e);

-		} else Error(123);

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

-			SelectOrCallSuffix(ref e);

-		}

-	}

-

 	static void ConstAtomExpression(out Expression! e) {

 		Token! x, dtName, id;  BigInteger n;  List<Expression!>! elements;

 		e = dummyExpr;  

@@ -1398,12 +1390,12 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			e = new FreshExpr(x, e); 

 			break;

 		}

-		case 50: {

+		case 49: {

 			Get();

 			x = token; 

 			Expression(out e);

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

-			Expect(50);

+			Expect(49);

 			break;

 		}

 		case 5: {

@@ -1426,7 +1418,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			Expect(83);

 			break;

 		}

-		default: Error(124); break;

+		default: Error(123); break;

 		}

 	}

 

@@ -1477,13 +1469,13 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			e = new OldExpr(x, e); 

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

 			Get();

-			if (StartOf(14)) {

+			if (StartOf(15)) {

 				QuantifierGuts(out e);

 			} else if (StartOf(6)) {

 				Expression(out e);

-			} else Error(125);

+			} else Error(124);

 			Expect(23);

-		} else Error(126);

+		} else Error(125);

 	}

 

 	static void SelectOrCallSuffix(ref Expression! e) {

@@ -1510,7 +1502,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			if (StartOf(6)) {

 				Expression(out ee);

 				e0 = ee; 

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

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

 					if (t.kind == 84) {

 						Get();

 						anyDots = true; 

@@ -1528,7 +1520,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 				Get();

 				Expression(out ee);

 				anyDots = true;  e1 = ee; 

-			} else Error(127);

+			} else Error(126);

 			assert !anyDots ==> e0 != null;

 			if (anyDots) {

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

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

 			

 			Expect(83);

-		} else Error(128);

+		} else Error(127);

 	}

 

 	static void QuantifierGuts(out Expression! q) {

@@ -1561,19 +1553,19 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		} else if (t.kind == 89 || t.kind == 90) {

 			Exists();

 			x = token; 

-		} else Error(129);

+		} else Error(128);

 		parseVarScope.PushMarker(); 

 		IdentTypeOptional(out bv);

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

-		while (t.kind == 11) {

+		while (t.kind == 12) {

 			Get();

 			IdentTypeOptional(out bv);

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

 		}

-		QSep();

 		while (t.kind == 5) {

 			AttributeOrTrigger(ref attrs, ref trigs);

 		}

+		QSep();

 		Expression(out body);

 		if (univ) {

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

@@ -1589,7 +1581,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			Get();

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

 			Get();

-		} else Error(130);

+		} else Error(129);

 	}

 

 	static void Exists() {

@@ -1597,43 +1589,43 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			Get();

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

 			Get();

-		} else Error(131);

-	}

-

-	static void QSep() {

-		if (t.kind == 91) {

-			Get();

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

-			Get();

-		} else Error(132);

+		} else Error(130);

 	}

 

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

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

 		

 		Expect(5);

-		if (t.kind == 12) {

+		if (t.kind == 13) {

 			AttributeBody(ref attrs);

 		} else if (StartOf(6)) {

 			es = new List<Expression!>(); 

 			Expressions(es);

 			trigs = new Triggers(es, trigs); 

-		} else Error(133);

+		} else Error(131);

 		Expect(6);

 	}

 

+	static void QSep() {

+		if (t.kind == 91) {

+			Get();

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

+			Get();

+		} else Error(132);

+	}

+

 	static void AttributeBody(ref Attributes attrs) {

 		string aName;

 		List<Attributes.Argument!> aArgs = new List<Attributes.Argument!>();

 		Attributes.Argument! aArg;

 		

-		Expect(12);

+		Expect(13);

 		Expect(1);

 		aName = token.val; 

-		if (StartOf(15)) {

+		if (StartOf(16)) {

 			AttributeArg(out aArg);

 			aArgs.Add(aArg); 

-			while (t.kind == 11) {

+			while (t.kind == 12) {

 				Get();

 				AttributeArg(out aArg);

 				aArgs.Add(aArg); 

@@ -1650,7 +1642,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		} else if (StartOf(6)) {

 			Expression(out e);

 			arg = new Attributes.Argument(e); 

-		} else Error(134);

+		} else Error(133);

 	}

 

 

@@ -1676,15 +1668,15 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			case 4: s = "class expected"; break;

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

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

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

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

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

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

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

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

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

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

-			case 15: s = "frame 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;

@@ -1699,29 +1691,29 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			case 27: s = "seq expected"; break;

 			case 28: s = "object expected"; break;

 			case 29: s = "function expected"; break;

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

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

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

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

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

-			case 35: s = "else 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 = "while expected"; break;

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

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

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

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

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

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

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

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

+			case 31: s = "decreases 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;

@@ -1769,18 +1761,18 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			case 97: s = "invalid TypeAndToken"; break;

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

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

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

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

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

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

-			case 104: s = "invalid IfThenElseExpr"; 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 ExtendedExpr"; break;

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

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

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

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

-			case 111: s = "invalid AssignRhs"; 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;

@@ -1792,18 +1784,17 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			case 120: s = "invalid UnaryExpression"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

-			case 131: s = "invalid Exists"; 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 AttributeOrTrigger"; break;

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

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

 

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

 		}

@@ -1812,21 +1803,22 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 

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

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

 	{x,T,x,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,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,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,T,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,T, T,T,x,x, T,T,x,T, T,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,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,T,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,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,T,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,T, T,T,x,x, T,T,x,T, T,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,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,x,x,x, x,x,x,x, x,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,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,T,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,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T,x, 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,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,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,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,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,T,x, 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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,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,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, 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,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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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/Dafny/Printer.ssc b/Dafny/Printer.ssc
index d0a6b3c9..89b9f62e 100644
--- a/Dafny/Printer.ssc
+++ b/Dafny/Printer.ssc
@@ -34,7 +34,7 @@ namespace Microsoft.Dafny {
     }

     

     public void PrintClass(ClassDecl! c) {

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

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

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

         wr.WriteLine(" { }");

       } else {

@@ -61,12 +61,11 @@ namespace Microsoft.Dafny {
       }

     }

     

-    void PrintClassMethodHelper(string! kind, Attributes attrs, string! modifiers, string! name, List<TypeParameter!>! typeArgs) {

+    void PrintClassMethodHelper(string! kind, Attributes attrs, string! name, List<TypeParameter!>! typeArgs) {

       if (kind.Length != 0) {

         wr.Write("{0} ", kind);

       }

       PrintAttributes(attrs);

-      wr.Write(modifiers);

       wr.Write(name);

       if (typeArgs.Count != 0) {

         wr.Write("<");

@@ -80,7 +79,7 @@ namespace Microsoft.Dafny {
     }

     

     public void PrintDatatype(DatatypeDecl! dt) {

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

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

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

         wr.WriteLine(" { }");

       } else {

@@ -114,6 +113,9 @@ namespace Microsoft.Dafny {
     

     public void PrintField(Field! field) {

       Indent(IndentAmount);

+      if (field.IsGhost) {

+        wr.Write("ghost ");

+      }

       wr.Write("var ");

       PrintAttributes(field.Attributes);

       wr.Write("{0}: ", field.Name);

@@ -123,7 +125,10 @@ namespace Microsoft.Dafny {
     

     public void PrintFunction(Function! f) {

       Indent(IndentAmount);

-      PrintClassMethodHelper("function", f.Attributes, f.Use ? "use " : "", f.Name, f.TypeArgs);

+      string k = "function";

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

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

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

       PrintFormals(f.Formals);

       wr.Write(": ");

       PrintType(f.ResultType);

@@ -152,14 +157,16 @@ namespace Microsoft.Dafny {
       }

       if (f.Body != null) {

         Indent(IndentAmount);

-        PrintExtendedExpr(f.Body, IndentAmount);

-        wr.WriteLine();

+        wr.WriteLine("{");

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

+        Indent(IndentAmount);

+        wr.WriteLine("}");

       }

     }

     

     public void PrintCtor(DatatypeCtor! ctor) {

       Indent(IndentAmount);

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

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

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

         PrintFormals(ctor.Formals);

       }

@@ -181,7 +188,9 @@ namespace Microsoft.Dafny {
     

     public void PrintMethod(Method! method) {

       Indent(IndentAmount);

-      PrintClassMethodHelper("method", method.Attributes, "", method.Name, method.TypeArgs);

+      string k = "method";

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

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

       PrintFormals(method.Ins);

       if (method.Outs.Count != 0) {

         if (method.Ins.Count + method.Outs.Count <= 3) {

@@ -431,27 +440,32 @@ namespace Microsoft.Dafny {
     // ----------------------------- PrintExpression -----------------------------

 

     public void PrintExtendedExpr(Expression! expr, int indent) {

-      wr.WriteLine("{");

-      int ind = indent + IndentAmount;

-      Indent(ind);

+      Indent(indent);

       if (expr is ITEExpr) {

-        Expression els = expr;  // bogus assignment, just to please the compiler

-        for (ITEExpr ite = (ITEExpr)expr; ite != null; ite = els as ITEExpr) {

-          wr.Write("if (");

+        while (true) {

+          ITEExpr ite = (ITEExpr)expr;

+          wr.Write("if ");

           PrintExpression(ite.Test);

-          wr.Write(") ");

-          PrintExtendedExpr(ite.Thn, ind);

-          wr.Write(" else ");

-          els = ite.Els;

+          wr.WriteLine(" then");

+          PrintExtendedExpr(ite.Thn, indent + IndentAmount);

+          expr = ite.Els;

+          if (expr is ITEExpr) {

+            Indent(indent);  wr.Write("else ");

+          } else {

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

+            Indent(indent + IndentAmount);

+            PrintExpression(expr);

+            wr.WriteLine();

+            return;

+          }

         }

-        PrintExtendedExpr(els, ind);

       } else if (expr is MatchExpr) {

         MatchExpr me = (MatchExpr)expr;

         wr.Write("match ");

         PrintExpression(me.Source);

         bool needsCurlies = exists{MatchCase mc in me.Cases; mc.Body is MatchExpr};

         wr.WriteLine(needsCurlies ? " {" : "");

-        int caseInd = ind + (needsCurlies ? IndentAmount : 0);

+        int caseInd = indent + (needsCurlies ? IndentAmount : 0);

         foreach (MatchCase mc in me.Cases) {

           Indent(caseInd);

           wr.Write("case {0}", mc.Id);

@@ -464,20 +478,16 @@ namespace Microsoft.Dafny {
             wr.Write(")");

           }

           wr.WriteLine(" =>");

-          Indent(caseInd + IndentAmount);

-          PrintExpression(mc.Body);

-          wr.WriteLine();

+          PrintExtendedExpr(mc.Body, caseInd + IndentAmount);

         }

         if (needsCurlies) {

-          Indent(ind);

+          Indent(indent);

           wr.WriteLine("}");

         }

       } else {

-        PrintExpression(expr, ind);

+        PrintExpression(expr, indent);

         wr.WriteLine();

       }

-      Indent(indent);

-      wr.Write("}");

     }

     

     public void PrintExpression(Expression! expr) {

@@ -552,7 +562,7 @@ namespace Microsoft.Dafny {
           (fragileContext && opBindingStrength == contextBindingStrength);

         

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

-        PrintExpr(e.Seq, 00, false, indent);  // BOGUS: fix me

+        PrintExpr(e.Seq, 0x00, false, indent);  // BOGUS: fix me

         wr.Write("[");

         if (e.SelectOne) {

           assert e.E0 != null;

@@ -674,12 +684,12 @@ namespace Microsoft.Dafny {
           case BinaryExpr.Opcode.Imp:

             opBindingStrength = 0x10; fragileLeftContext = true; break;

           case BinaryExpr.Opcode.Iff:

-            opBindingStrength = 0x00; break;

+            opBindingStrength = 0x08; break;

           default:

             assert false;  // unexpected binary operator

         }

-        int opBS = opBindingStrength & 0xF0;

-        int ctxtBS = contextBindingStrength & 0xF0;

+        int opBS = opBindingStrength & 0xF8;

+        int ctxtBS = contextBindingStrength & 0xF8;

         bool parensNeeded = opBS < ctxtBS ||

           (opBS == ctxtBS && (opBindingStrength != contextBindingStrength || fragileContext));

 

@@ -729,7 +739,21 @@ namespace Microsoft.Dafny {
         wr.Write("*");

         

       } else if (expr is ITEExpr) {

-        assert false;  // ITE is an extended expression and should be printed only using PrintExtendedExpr

+        ITEExpr ite = (ITEExpr)expr;

+        // determine if parens are needed

+        int opBindingStrength = 0x00;

+        bool parensNeeded = opBindingStrength < contextBindingStrength ||

+          (fragileContext && opBindingStrength == contextBindingStrength);

+        

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

+        wr.Write("if ");

+        PrintExpression(ite.Test);

+        wr.Write(" then ");

+        PrintExpression(ite.Thn);

+        wr.Write(" else ");

+        PrintExpr(ite.Els, opBindingStrength, false, indent);

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

+        

       } else if (expr is MatchExpr) {

         assert false;  // MatchExpr is an extended expression and should be printed only using PrintExtendedExpr

       } else {

diff --git a/Dafny/Resolver.ssc b/Dafny/Resolver.ssc
index 31f51424..8bbc1d29 100644
--- a/Dafny/Resolver.ssc
+++ b/Dafny/Resolver.ssc
@@ -243,6 +243,9 @@ namespace Microsoft.Dafny {
     /// </summary>

     void ResolveFunction(Function! f) {

       scope.PushMarker();

+      if (f.IsClass) {

+        scope.AllowInstance = false;

+      }

       foreach (Formal p in f.Formals) {

         scope.Push(p.Name, p);

       }

@@ -310,6 +313,9 @@ 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) {

+        scope.AllowInstance = false;

+      }

       foreach (Formal p in m.Ins) {

         scope.Push(p.Name, p);

       }

@@ -647,7 +653,7 @@ namespace Microsoft.Dafny {
           }

         }

         FunctionCallExpr fce = expr as FunctionCallExpr;

-        if (fce == null || fce.Function == null || !fce.Function.Use) {

+        if (fce == null || fce.Function == null || !fce.Function.IsUse) {

           Error(s.Expr, "use statement must indicate a function declared as use");

         }

       } else if (stmt is PredicateStmt) {

@@ -767,7 +773,7 @@ namespace Microsoft.Dafny {
           }

         }

         // resolve receiver

-        ResolveExpression(s.Receiver, true);

+        ResolveReceiver(s.Receiver, true);

         assert s.Receiver.Type != null;  // follows from postcondition of ResolveExpression

         // resolve arguments

         foreach (Expression e in s.Args) {

@@ -790,6 +796,12 @@ 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

+            if (!scope.AllowInstance && !method.IsClass && 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");

+            }

             // build the type substitution map

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

             for (int i = 0; i < ctype.TypeArgs.Count; i++) {

@@ -1031,7 +1043,10 @@ namespace Microsoft.Dafny {
         }

         

       } else if (expr is ThisExpr) {

-        expr.Type = GetThisType(expr.tok, currentClass);

+        if (!scope.AllowInstance) {

+          Error(expr, "'this' is not allowed in a 'class' context");

+        }

+        expr.Type = GetThisType(expr.tok, currentClass);  // do this regardless of scope.AllowInstance, for better error reporting

         

       } else if (expr is IdentifierExpr) {

         IdentifierExpr e = (IdentifierExpr)expr;

@@ -1185,7 +1200,7 @@ namespace Microsoft.Dafny {
         

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

-        ResolveExpression(e.Receiver, twoState);

+        ResolveReceiver(e.Receiver, twoState);

         assert e.Receiver.Type != null;  // follows from postcondition of ResolveExpression

         UserDefinedType ctype;

         MemberDecl member = ResolveMember(expr.tok, e.Receiver.Type, e.Name, out ctype);

@@ -1200,6 +1215,16 @@ 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) {

+              // 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

+              // of e.Receiver being 'this' (explicitly or implicitly), for that case needs to be allowed

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

+            }

             // build the type substitution map

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

             for (int i = 0; i < ctype.TypeArgs.Count; i++) {

@@ -1403,7 +1428,6 @@ namespace Microsoft.Dafny {
         

       } else if (expr is ITEExpr) {

         ITEExpr e = (ITEExpr)expr;

-        assert !twoState;

         ResolveExpression(e.Test, twoState);

         assert e.Test.Type != null;  // follows from postcondition of ResolveExpression

         ResolveExpression(e.Thn, twoState);

@@ -1413,13 +1437,11 @@ namespace Microsoft.Dafny {
         if (!UnifyTypes(e.Test.Type, Type.Bool)) {

           Error(expr, "guard condition in if-then-else expression must be a boolean (instead got {0})", e.Test.Type);

         }

-        if (!UnifyTypes(e.Thn.Type, Type.Bool)) {

-          Error(expr, "the then branch of an if-then-else expression must be a boolean (instead got {0})", e.Thn.Type);

-        }

-        if (!UnifyTypes(e.Els.Type, Type.Bool)) {

-          Error(expr, "the else branch of an if-then-else expression must be a boolean (instead got {0})", e.Els.Type);

+        if (UnifyTypes(e.Thn.Type, e.Els.Type)) {

+          expr.Type = e.Thn.Type;

+        } else {

+          Error(expr, "the two branches of an if-then-else expression must have the same type (got {0} and {1})", e.Thn.Type, e.Els.Type);

         }

-        expr.Type = Type.Bool;

       

       } else if (expr is MatchExpr) {

         MatchExpr me = (MatchExpr)expr;

@@ -1516,6 +1538,19 @@ namespace Microsoft.Dafny {
       }

     }

     

+    void ResolveReceiver(Expression! expr, bool twoState)

+      requires currentClass != null;

+      ensures expr.Type != null;

+    {

+      if (expr is ThisExpr) {

+        // Allow 'this' here, regardless of scope.AllowInstance.  The caller is responsible for

+        // making sure 'this' does not really get used when it's not available.

+        expr.Type = GetThisType(expr.tok, currentClass);

+      } else {

+        ResolveExpression(expr, twoState);

+      }

+    }

+    

     /// <summary>

     /// Note: this method is allowed to be called even if "type" does not make sense for "op", as might be the case if

     /// resolution of the binary expression failed.  If so, an arbitrary resolved opcode is returned.

@@ -1615,7 +1650,18 @@ namespace Microsoft.Dafny {
     [Rep] readonly List<string>! names = new List<string>();  // a null means a marker

     [Rep] readonly List<Thing?>! things = new List<Thing?>();

     invariant names.Count == things.Count;

+    int scopeSizeWhereInstancesWereDisallowed = -1;

+    invariant -1 <= scopeSizeWhereInstancesWereDisallowed && scopeSizeWhereInstancesWereDisallowed <= names.Count;

     

+    public bool AllowInstance {

+      get { return scopeSizeWhereInstancesWereDisallowed == -1; }

+      set

+        requires AllowInstance && !value;  // only allowed to change from true to false (that's all that's currently needed in Dafny); Pop is what can make the change in the other direction

+      {

+        scopeSizeWhereInstancesWereDisallowed = names.Count;

+      }

+    }

+

     public void PushMarker() {

       names.Add(null);

       things.Add(null);

@@ -1631,6 +1677,9 @@ namespace Microsoft.Dafny {
       }

       names.RemoveRange(n, names.Count - n);

       things.RemoveRange(n, things.Count - n);

+      if (names.Count < scopeSizeWhereInstancesWereDisallowed) {

+        scopeSizeWhereInstancesWereDisallowed = -1;

+      }

     }

     

     // Pushes name-->var association and returns "true", if name has not already been pushed since the last marker.

diff --git a/Dafny/Scanner.ssc b/Dafny/Scanner.ssc
index c134acf9..921ef4f6 100644
--- a/Dafny/Scanner.ssc
+++ b/Dafny/Scanner.ssc
@@ -276,10 +276,10 @@ public class Scanner {
   static void CheckLiteral() {

     switch (t.val) {

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

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

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

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

-			case "frame": t.kind = 15; 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;

@@ -292,25 +292,25 @@ public class Scanner {
 			case "seq": t.kind = 27; break;

 			case "object": t.kind = 28; break;

 			case "function": t.kind = 29; break;

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

-			case "reads": t.kind = 31; break;

-			case "decreases": t.kind = 32; break;

-			case "if": t.kind = 34; break;

-			case "else": t.kind = 35; 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 "while": t.kind = 45; break;

-			case "invariant": t.kind = 46; break;

-			case "call": t.kind = 47; break;

-			case "foreach": t.kind = 48; break;

-			case "in": t.kind = 49; break;

-			case "assert": t.kind = 51; break;

-			case "assume": t.kind = 52; break;

+			case "reads": t.kind = 30; break;

+			case "decreases": 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;

@@ -352,36 +352,36 @@ public class Scanner {
 			case 6:

 				{t.kind = 6; goto done;}

 			case 7:

-				{t.kind = 8; goto done;}

+				{t.kind = 10; goto done;}

 			case 8:

-				{t.kind = 11; goto done;}

+				{t.kind = 12; 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 = 12; goto done;}

+				else {t.kind = 13; goto done;}

 			case 10:

 				if (ch == '=') {buf.Append(ch); NextCh(); goto case 19;}

-				else {t.kind = 13; goto done;}

+				else {t.kind = 14; goto done;}

 			case 11:

 				if (ch == '=') {buf.Append(ch); NextCh(); goto case 31;}

-				else {t.kind = 14; goto done;}

+				else {t.kind = 15; goto done;}

 			case 12:

 				{t.kind = 22; goto done;}

 			case 13:

 				{t.kind = 23; goto done;}

 			case 14:

-				{t.kind = 33; goto done;}

+				{t.kind = 32; 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 = 38; goto done;}

+				{t.kind = 35; goto done;}

 			case 17:

-				{t.kind = 42; goto done;}

+				{t.kind = 39; goto done;}

 			case 18:

 				if (ch == '|') {buf.Append(ch); NextCh(); goto case 29;}

-				else {t.kind = 50; goto done;}

+				else {t.kind = 49; goto done;}

 			case 19:

 				if (ch == '=') {buf.Append(ch); NextCh(); goto case 20;}

 				else {t.kind = 62; goto done;}

diff --git a/Dafny/Translator.ssc b/Dafny/Translator.ssc
index 85a09b1f..4a8d7ebf 100644
--- a/Dafny/Translator.ssc
+++ b/Dafny/Translator.ssc
@@ -439,10 +439,17 @@ namespace Microsoft.Dafny {
       Bpl.BoundVariable bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType));

       formals.Add(bv);

       args.Add(new Bpl.IdentifierExpr(f.tok, bv));

-      Bpl.BoundVariable bvThis = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType));

-      formals.Add(bvThis);

-      Bpl.Expr bvThisIdExpr = new Bpl.IdentifierExpr(f.tok, bvThis);

-      args.Add(bvThisIdExpr);

+      Bpl.BoundVariable bvThis;

+      Bpl.Expr bvThisIdExpr;

+      if (f.IsClass) {

+        bvThis = null;

+        bvThisIdExpr = null;

+      } else {

+        bvThis = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType));

+        formals.Add(bvThis);

+        bvThisIdExpr = new Bpl.IdentifierExpr(f.tok, bvThis);

+        args.Add(bvThisIdExpr);

+      }

       DatatypeValue r = null;

       if (specializationReplacementFormals != null) {

         assert ctor != null;  // follows from if guard and the precondition

@@ -468,16 +475,18 @@ namespace Microsoft.Dafny {
         }

       }

       

-      Bpl.Expr ante = Bpl.Expr.And(

-        Bpl.Expr.Neq(bvThisIdExpr, predef.Null),

-        FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr));

+      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

+        ante = Bpl.Expr.And(Bpl.Expr.Neq(bvThisIdExpr, predef.Null), ante);

+      }

       foreach (Expression req in f.Req) {

         ante = Bpl.Expr.And(ante, etran.TrExpr(req));

       }

       Bpl.FunctionCall funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType)));

       Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, funcID, args);

       Bpl.Trigger tr;

-      if (f.Use) {

+      if (f.IsUse) {

         Bpl.FunctionCall useID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName + "#use", TrType(f.ResultType)));

         Bpl.Expr useAppl = new Bpl.NAryExpr(f.tok, useID, args);

         ante = Bpl.Expr.And(useAppl, ante);

@@ -727,16 +736,21 @@ namespace Microsoft.Dafny {
       Bpl.VariableSeq bvars = new Bpl.VariableSeq();

       Bpl.ExprSeq f0args = new Bpl.ExprSeq();

       Bpl.ExprSeq f1args = new Bpl.ExprSeq();

-      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(h0Var);  bvars.Add(h1Var);  bvars.Add(thVar);

-      f0args.Add(h0);  f0args.Add(th);

-      f1args.Add(h1);  f1args.Add(th);

+      bvars.Add(h0Var);  bvars.Add(h1Var);

+      f0args.Add(h0);

+      f1args.Add(h1);

+      if (!f.IsClass) {

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

+        f0args.Add(th);

+        f1args.Add(th);

 

-      Type thisType = Resolver.GetThisType(f.tok, (!)f.EnclosingClass);

-      Bpl.Expr wh = Bpl.Expr.And(Bpl.Expr.Neq(th, predef.Null),

-        Bpl.Expr.And(etran0.GoodRef(f.tok, th, thisType), etran1.GoodRef(f.tok, th, thisType)));

-      wellFormed = Bpl.Expr.And(wellFormed, wh);

+        Type thisType = Resolver.GetThisType(f.tok, (!)f.EnclosingClass);

+        Bpl.Expr wh = Bpl.Expr.And(Bpl.Expr.Neq(th, predef.Null),

+          Bpl.Expr.And(etran0.GoodRef(f.tok, th, thisType), etran1.GoodRef(f.tok, th, thisType)));

+        wellFormed = Bpl.Expr.And(wellFormed, wh);

+      }

 

       foreach (Formal p in f.Formals) {

         Bpl.BoundVariable bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));

@@ -744,7 +758,7 @@ namespace Microsoft.Dafny {
         Bpl.Expr formal = new Bpl.IdentifierExpr(p.tok, bv);

         f0args.Add(formal);

         f1args.Add(formal);

-        wh = GetWhereClause(p.tok, formal, p.Type, etran0);

+        Bpl.Expr wh = GetWhereClause(p.tok, formal, p.Type, etran0);

         if (wh != null) { wellFormed = Bpl.Expr.And(wellFormed, wh); }

         wh = GetWhereClause(p.tok, formal, p.Type, etran1);

         if (wh != null) { wellFormed = Bpl.Expr.And(wellFormed, wh); }

@@ -816,14 +830,16 @@ namespace Microsoft.Dafny {
       ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);

       // parameters of the procedure

       Bpl.VariableSeq inParams = new Bpl.VariableSeq();

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

-      Bpl.Formal thVar = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType, wh), true);

-      inParams.Add(thVar);

+      if (!f.IsClass) {

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

+        Bpl.Formal thVar = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType, wh), true);

+        inParams.Add(thVar);

+      }

       foreach (Formal p in f.Formals) {

         Bpl.Type varType = TrType(p.Type);

-        wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);

+        Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);

         inParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), true));

       }

       Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);

@@ -901,8 +917,9 @@ namespace Microsoft.Dafny {
         return total;

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

+        assert e.Function != null;  // follows from the fact that expr has been successfully resolved

         Bpl.Expr r = IsTotal(e.Receiver, etran);

-        if (!(e.Receiver is ThisExpr)) {

+        if (!e.Function.IsClass && !(e.Receiver is ThisExpr)) {

           r = BplAnd(r, Bpl.Expr.Neq(etran.TrExpr(e.Receiver), predef.Null));

         }

         // TODO: check reads permissions and check preconditions

@@ -1046,7 +1063,9 @@ 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);

-        CheckNonNull(expr.tok, e.Receiver, builder, etran);

+        if (!e.Function.IsClass && !(e.Receiver is ThisExpr)) {

+          CheckNonNull(expr.tok, e.Receiver, builder, etran);

+        }

         // check well-formedness of the other parameters

         foreach (Expression arg in e.Args) {

           CheckWellformed(arg, func, Position.Neither, locals, builder, etran);

@@ -1164,6 +1183,11 @@ namespace Microsoft.Dafny {
               builder.Add(new Bpl.IfCmd(expr.tok, Bpl.Expr.Not(etran.TrExpr(e.E0)), b.Collect(expr.tok), null, null));

             }

             break;

+          case BinaryExpr.ResolvedOpcode.Div:

+          case BinaryExpr.ResolvedOpcode.Mod:

+            CheckWellformed(e.E1, func, pos, locals, builder, etran);

+            builder.Add(Assert(expr.tok, Bpl.Expr.Neq(etran.TrExpr(e.E1), Bpl.Expr.Literal(0)), "possible division by zero"));

+            break;

           default:

             CheckWellformed(e.E1, func, pos, locals, builder, etran);

             break;

@@ -1319,7 +1343,9 @@ 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));

-        args.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType), true));

+        if (!f.IsClass) {

+          args.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType), true));

+        }

         foreach (Formal p in f.Formals) {

           args.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)), true));

         }

@@ -1328,7 +1354,7 @@ namespace Microsoft.Dafny {
         

         functions.Add(f, func);

         

-        if (f.Use) {

+        if (f.IsUse) {

           Bpl.Formal boolRes = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);

           useF = new Bpl.Function(f.tok, f.FullName + "#use", args, boolRes);

         }

@@ -1347,19 +1373,21 @@ namespace Microsoft.Dafny {
         

         Bpl.VariableSeq inParams = new Bpl.VariableSeq();

         Bpl.VariableSeq outParams = new Bpl.VariableSeq();

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

-        Bpl.Formal thVar = new Bpl.Formal(m.tok, new Bpl.TypedIdent(m.tok, "this", predef.RefType, wh), true);

-        inParams.Add(thVar);

+        if (!m.IsClass) {

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

+          Bpl.Formal thVar = new Bpl.Formal(m.tok, new Bpl.TypedIdent(m.tok, "this", predef.RefType, wh), true);

+          inParams.Add(thVar);

+        }

         foreach (Formal p in m.Ins) {

           Bpl.Type varType = TrType(p.Type);

-          wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);

+          Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);

           inParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), true));

         }

         foreach (Formal p in m.Outs) {

           Bpl.Type varType = TrType(p.Type);

-          wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);

+          Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);

           outParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), false));

         }

         

@@ -1666,17 +1694,20 @@ namespace Microsoft.Dafny {
           TrStmt(local, builder, locals, etran);

         }

         Bpl.ExprSeq ins = new Bpl.ExprSeq();

-        ins.Add(etran.TrExpr(s.Receiver));

+        assert s.Method != null;  // follows from the fact that stmt has been successfully resolved

+        if (!s.Method.IsClass) {

+          ins.Add(etran.TrExpr(s.Receiver));

+        }

         for (int i = 0; i < s.Args.Count; i++) {

           Expression e = s.Args[i];

-          Type t = ((!)s.Method).Ins[i].Type;

+          Type t = s.Method.Ins[i].Type;

           ins.Add(etran.CondApplyBox(stmt.Tok, etran.TrExpr(e), (!)e.Type, t));

         }

         Bpl.IdentifierExprSeq outs = new Bpl.IdentifierExprSeq();

         List<Bpl.IdentifierExpr> tmpOuts = new List<Bpl.IdentifierExpr>(s.Lhs.Count);

         for (int i = 0; i < s.Lhs.Count; i++) {

           Expression e = s.Lhs[i];

-          if (ExpressionTranslator.ModeledAsBoxType(((!)s.Method).Outs[i].Type) && !ExpressionTranslator.ModeledAsBoxType((!)e.Type)) {

+          if (ExpressionTranslator.ModeledAsBoxType(s.Method.Outs[i].Type) && !ExpressionTranslator.ModeledAsBoxType((!)e.Type)) {

             // we need an Unbox

             Bpl.LocalVariable var = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$tmp#" + otherTmpVarCount, predef.BoxType));

             otherTmpVarCount++;

@@ -1690,7 +1721,7 @@ namespace Microsoft.Dafny {
           }

         }

         

-        Bpl.CallCmd call = new Bpl.CallCmd(stmt.Tok, ((!)s.Method).FullName, ins, outs);

+        Bpl.CallCmd call = new Bpl.CallCmd(stmt.Tok, s.Method.FullName, ins, outs);

         builder.Add(call);

         for (int i = 0; i < s.Lhs.Count; i++) {

           Bpl.IdentifierExpr tmpVarIdE = tmpOuts[i];

@@ -2293,7 +2324,9 @@ 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);

-          args.Add(TrExpr(e.Receiver));

+          if (!e.Function.IsClass) {

+            args.Add(TrExpr(e.Receiver));

+          }

           for (int i = 0; i < e.Args.Count; i++) {

             Expression ee = e.Args[i];

             Type t = e.Function.Formals[i].Type;

@@ -2487,9 +2520,7 @@ namespace Microsoft.Dafny {
           Bpl.Expr g = TrExpr(e.Test);

           Bpl.Expr thn = TrExpr(e.Thn);

           Bpl.Expr els = TrExpr(e.Els);

-          Bpl.Expr yea = Bpl.Expr.Imp(g, thn);

-          Bpl.Expr nay = Bpl.Expr.Imp(Bpl.Expr.Not(g), els);

-          return Bpl.Expr.And(yea, nay);

+          return translator.FunctionCall(expr.tok, BuiltinFunction.IfThenElse, translator.TrType((!)expr.Type), g, thn, els);

            

         } else {

           assert false;  // unexpected expression

@@ -2513,7 +2544,9 @@ 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);

-        args.Add(TrExpr(e.Receiver));

+        if (!e.Function.IsClass) {

+          args.Add(TrExpr(e.Receiver));

+        }

         foreach (Expression ee in e.Args) {

           args.Add(TrExpr(ee));

         }

@@ -2734,6 +2767,8 @@ namespace Microsoft.Dafny {
       SeqEqual,

       SeqSameUntil,

       

+      IfThenElse,

+      

       Box,

       Unbox,

       

@@ -2842,6 +2877,11 @@ namespace Microsoft.Dafny {
           assert args.Length == 3;

           assert typeInstantiation == null;

           return FunctionCall(tok, "Seq#SameUntil", Bpl.Type.Bool, args);

+          

+        case BuiltinFunction.IfThenElse:

+          assert args.Length == 3;

+          assert typeInstantiation != null;

+          return FunctionCall(tok, "$ite", typeInstantiation, args);

 

         case BuiltinFunction.Box:

           assert args.Length == 1;

@@ -2993,7 +3033,7 @@ namespace Microsoft.Dafny {
           Expression body = Substitute(fexp.Function.Body, fexp.Receiver, substMap);

           foreach (Expression se in SplitExpr(body, false)) {

             assert fexp != null && fexp.Function != null;  // already checked above, but the compiler seems to have forgotten that

-            if (fexp.Function.Use) {

+            if (fexp.Function.IsUse) {

               BinaryExpr imp = new BinaryExpr(expr.tok, BinaryExpr.Opcode.Imp, new UseExpr(fexp), se);

               imp.ResolvedOp = BinaryExpr.ResolvedOpcode.Imp;

               imp.Type = Type.Bool;

@@ -3003,7 +3043,7 @@ namespace Microsoft.Dafny {
             }

           }

           assert fexp != null && fexp.Function != null;  // already checked above, but the compiler seems to have forgotten that

-          if (fexp.Function.Use) {

+          if (fexp.Function.IsUse) {

             UnaryExpr ue = new UnaryExpr(expr.tok, UnaryExpr.Opcode.Not, new UseExpr(fexp));

             ue.Type = Type.Bool;

             BinaryExpr imp = new BinaryExpr(expr.tok, BinaryExpr.Opcode.Imp, ue, expr);

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 043a4cfd..d1584333 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -30,6 +30,21 @@ class MyClass<T, U> {
       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

+  {

+    if x < 0 then

+      h

+    else if x == 0 then

+      if if h == k then true else false then

+        h

+      else if y == 0 then

+        k

+      else

+        h

+    else

+      k

+  }

 }

 

 datatype List<T> {

@@ -70,8 +85,25 @@ TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 1 (expected C
 SmallTests.dfy(30,7): Error: RHS expression must be well defined

 Execution trace:

     (0,0): anon0

+SmallTests.dfy(61,36): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+    (0,0): anon10_Then

+SmallTests.dfy(62,51): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+    (0,0): anon10_Else

+    (0,0): anon3

+    (0,0): anon11_Else

+SmallTests.dfy(63,22): Error: target object may be null

+Execution trace:

+    (0,0): anon0

+    (0,0): anon10_Then

+    (0,0): anon3

+    (0,0): anon11_Then

+    (0,0): anon6

 

-Dafny program verifier finished with 4 verified, 1 error

+Dafny program verifier finished with 6 verified, 4 errors

 

 -------------------- Queue.dfy --------------------

 

diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy
index a224ed91..c5599529 100644
--- a/Test/dafny0/Simple.dfy
+++ b/Test/dafny0/Simple.dfy
@@ -27,6 +27,14 @@ class MyClass<T,U> {
       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

+  {

+    if x < 0 then h else

+    if (x == 0) then

+      if if h==k then true else false then h else if y == 0 then k else h

+    else k

+  }

 }

 

 // some datatype stuff:

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 17f0168a..6ac9879d 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -43,4 +43,27 @@ class Node {
       t := s[..j] + [b] + s[j+1..];

     }

   }

+

+  method Max0(x: int, y: int) returns (r: int)

+    ensures r == (if x < y then y else x);

+  {

+    if (x < y) { r := y; } else { r := x; }

+  }

+

+  method Max1(x: int, y: int) returns (r: int)

+    ensures r == x || r == y;

+    ensures x <= r && y <= r;

+  {

+    r := if x < y then y else x;

+  }

+

+  function PoorlyDefined(x: int): int

+    requires if next == null then 5/x < 20 else true;  // ill-defined then branch

+    requires if next == null then true else 0 <= 5/x;  // ill-defined then branch

+    requires if next.next == null then true else true;  // ill-defined guard

+    requires 10/x != 8;  // this is well-defined, because we get here only if x is non-0

+    reads this;

+  {

+    12

+  }

 }

diff --git a/Test/dafny0/Use.dfy b/Test/dafny0/Use.dfy
index 1d2d264f..8b7eafc1 100644
--- a/Test/dafny0/Use.dfy
+++ b/Test/dafny0/Use.dfy
@@ -1,7 +1,7 @@
 class T {

   var x: int;

 

-  function use F(y: int): int {

+  use function F(y: int): int {

     2*y

   }

 

@@ -12,7 +12,7 @@ class T {
     assert F(7) == 14;  // error (definition not engaged)

   }

 

-  function use G(y: int): bool {

+  use function G(y: int): bool {

     0 <= y

   }

 

@@ -25,7 +25,7 @@ class T {
     assert G(7);  // error (definition not engaged)

   }

 

-  function use H(): int

+  use function H(): int

     reads this;

   {

     x

diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index d8fe3052..3b10c560 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -35,7 +35,7 @@
         "invariant" "decreases"

         )) . font-lock-builtin-face)

    `(,(dafny-regexp-opt '(

-        "assert" "assume" "break" "call" "else" "havoc" "if" "label" "return" "while"

+        "assert" "assume" "break" "call" "then" "else" "havoc" "if" "label" "return" "while"

         "old" "forall" "exists" "new" "foreach" "in" "this" "fresh" "use"

         "match" "case" "false" "true" "null")) . font-lock-keyword-face)

    `(,(dafny-regexp-opt '("bool" "int" "object" "set" "seq")) . font-lock-type-face)

diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index f88c3b54..23ea36fb 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -13,7 +13,7 @@
       % expressions

       match,case,false,true,null,old,fresh,this,

       % statements

-      assert,assume,new,havoc,call,if,else,while,invariant,break,return,foreach,

+      assert,assume,new,havoc,call,if,then,else,while,invariant,break,return,foreach,

       },

   literate=%

     {:}{$\colon$}1