Dafny:

* Enforce ghost vs. non-ghost separation
* Allow ghost parameters and ghost locals
* Functions are ghost, but allow the non-ghost "function method"

6 files changed, 355 insertions, 159 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index d6f3aeae..069c88c3 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -36,10 +36,11 @@ struct MemberModifiers {
 // helper routine for parsing call statements

 private static void RecordCallLhs(IdentifierExpr! e,

                                   List<IdentifierExpr!>! lhs,

-                                  List<VarDecl!>! newVars) {

+                                  List<AutoVarDecl!>! newVars) {

+  int index = lhs.Count;

   lhs.Add(e);

   if (parseVarScope.Find(e.Name) == null) {

-    VarDecl d = new VarDecl(e.tok, e.Name, new InferredTypeProxy(), null);

+    AutoVarDecl d = new AutoVarDecl(e.tok, e.Name, new InferredTypeProxy(), index);

     newVars.Add(d);

     parseVarScope.Push(e.Name, e.Name);

   }

@@ -207,6 +208,14 @@ FieldDecl<MemberModifiers mmod, List<MemberDecl!\>! mm>
   ";"

   .

 

+GIdentType<bool allowGhost, out Token! id, out Type! ty, out bool isGhost>

+/* isGhost always returns as false if allowGhost is false */

+= (. isGhost = false; .)

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

+  ]

+  IdentType<out id, out ty>

+  .

+

 IdentType<out Token! id, out Type! ty>

 = Ident<out id>

   ":"

@@ -276,9 +285,9 @@ MethodDecl<MemberModifiers mmod, out Method! m>
   Ident<out id>

   [ GenericParameters<typeArgs> ]

   (. parseVarScope.PushMarker(); .)

-  Formals<true, ins>

+  Formals<true, true, ins>

   [ "returns"

-    Formals<false, outs>

+    Formals<false, true, outs>

   ]

 

   ( ";" { MethodSpec<req, mod, ens, dec> }

@@ -307,12 +316,12 @@ MethodSpec<List<MaybeFreeExpression!\>! req, List<Expression!\>! mod, List<Maybe
   )

   .

 

-Formals<bool incoming, List<Formal!\>! formals> 

-= (. Token! id;  Type! ty; .)

+Formals<bool incoming, bool allowGhosts, List<Formal!\>! formals> 

+= (. Token! id;  Type! ty;  bool isGhost; .)

   "("

   [

-    IdentType<out id, out ty>                       (. formals.Add(new Formal(id, id.val, ty, incoming));  parseVarScope.Push(id.val, id.val); .)

-    { "," IdentType<out id, out ty>                 (. formals.Add(new Formal(id, id.val, ty, incoming));  parseVarScope.Push(id.val, id.val); .)

+    GIdentType<allowGhosts, out id, out ty, out isGhost>         (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost));  parseVarScope.Push(id.val, id.val); .)

+    { "," GIdentType<allowGhosts, out id, out ty, out isGhost>   (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost));  parseVarScope.Push(id.val, id.val); .)

     }

   ]

   ")"

@@ -322,8 +331,8 @@ FormalsOptionalIds<List<Formal!\>! formals>
 = (. Token! id;  Type! ty;  string! name; .)

   "("

   [

-    TypeIdentOptional<out id, out name, out ty>        (. formals.Add(new Formal(id, name, ty, true));  parseVarScope.Push(name, name); .)

-    { "," TypeIdentOptional<out id, out name, out ty>  (. formals.Add(new Formal(id, name, ty, true));  parseVarScope.Push(name, name); .)

+    TypeIdentOptional<out id, out name, out ty>        (. formals.Add(new Formal(id, name, ty, true, false));  parseVarScope.Push(name, name); .)

+    { "," TypeIdentOptional<out id, out name, out ty>  (. formals.Add(new Formal(id, name, ty, true, false));  parseVarScope.Push(name, name); .)

     }

   ]

   ")"

@@ -390,15 +399,18 @@ FunctionDecl<MemberModifiers mmod, out Function! f>
      List<Expression!> reads = new List<Expression!>();

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

      Expression! bb;  Expression body = null;

+     bool isFunctionMethod = false;

   .)

   "function"

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

+  [ "method"                 (. isFunctionMethod = true; .)

+  ]

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

   .)

   { Attribute<ref attrs> }

   Ident<out id> 

   [ GenericParameters<typeArgs> ]

   (. parseVarScope.PushMarker(); .)

-  Formals<true, formals>

+  Formals<true, false, formals>

   ":"

   Type<out returnType>

   ( ";"

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

   )

   (. parseVarScope.PopMarker();

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

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

   .)

   .

 

@@ -580,16 +592,17 @@ LhsExpr<out Expression! e>
   .

 

 VarDeclStmts<List<Statement!\>! ss>

-= (. VarDecl! d; .)

-  [ "ghost" ]

+= (. VarDecl! d;  bool isGhost = false; .)

+  [ "ghost"                            (. isGhost = true; .)

+  ]

   "var"

-  IdentTypeRhs<out d>                  (. ss.Add(d);  parseVarScope.Push(d.Name, d.Name); .)

-  { "," IdentTypeRhs<out d>            (. ss.Add(d);  parseVarScope.Push(d.Name, d.Name); .)

+  IdentTypeRhs<out d, isGhost>         (. ss.Add(d);  parseVarScope.Push(d.Name, d.Name); .)

+  { "," IdentTypeRhs<out d, isGhost>   (. ss.Add(d);  parseVarScope.Push(d.Name, d.Name); .)

   }

   ";"

   .

 

-IdentTypeRhs<out VarDecl! d>

+IdentTypeRhs<out VarDecl! d, bool isGhost>

 = (. Token! id;  Type! ty;  Expression! e;

      Expression rhs = null;  Type newType = null;

      Type optionalType = null;  DeterminedAssignmentRhs optionalRhs = null;

@@ -608,7 +621,7 @@ IdentTypeRhs<out VarDecl! d>
      } else if (optionalType == null) {

        optionalType = new InferredTypeProxy();

      }

-     d = new VarDecl(id, id.val, optionalType, optionalRhs);

+     d = new VarDecl(id, id.val, optionalType, isGhost, optionalRhs);

   .)

   .

 

@@ -664,7 +677,7 @@ CallStmt<out Statement! s>
 = (. Token! x, id;

      Expression! e;

      List<IdentifierExpr!> lhs = new List<IdentifierExpr!>();

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

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

   .)

   "call"                       (. x = token; .)

   CallStmtSubExpr<out e>

diff --git a/Source/Dafny/DafnyAst.ssc b/Source/Dafny/DafnyAst.ssc
index ca49e940..b73bacc9 100644
--- a/Source/Dafny/DafnyAst.ssc
+++ b/Source/Dafny/DafnyAst.ssc
@@ -415,6 +415,7 @@ namespace Microsoft.Dafny
     string! UniqueName { get; }

     Type! Type { get; }

     bool IsMutable { get; }

+    bool IsGhost { get; }

   }

   

   public abstract class NonglobalVariable : IVariable {

@@ -440,11 +441,14 @@ namespace Microsoft.Dafny
       }

     } }

     public abstract bool IsMutable { get; }

+    readonly bool isGhost;

+    public bool IsGhost { get { return isGhost; } }

     

-    public NonglobalVariable(Token! tok, string! name, Type! type) {

+    public NonglobalVariable(Token! tok, string! name, Type! type, bool isGhost) {

       this.tok = tok;

       this.name = name;

       this.type = type;

+      this.isGhost = isGhost;

     }

     

     internal static int varIdCount;  // this varIdCount is used for both NonglobalVariable's and VarDecl's.

@@ -454,9 +458,9 @@ namespace Microsoft.Dafny
     public readonly bool InParam;  // true to in-parameter, false for out-parameter

     public override bool IsMutable { get { return !InParam; } }

     

-    public Formal(Token! tok, string! name, Type! type, bool inParam) {

+    public Formal(Token! tok, string! name, Type! type, bool inParam, bool isGhost) {

       InParam = inParam;

-      base(tok, name, type);

+      base(tok, name, type, isGhost);

     }

   }

   

@@ -464,12 +468,13 @@ namespace Microsoft.Dafny
     public override bool IsMutable { get { return false; } }

     

     public BoundVar(Token! tok, string! name, Type! type) {

-      base(tok, name, type);

+      base(tok, name, type, false);

     }

   }

   

   public class Function : MemberDecl, TypeParameter.ParentType {

     public readonly bool IsClass;

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

     public readonly bool IsUse;

     public readonly List<TypeParameter!>! TypeArgs;

     public readonly List<Formal!>! Formals;

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

     public readonly Expression Body;  // an extended expression

     

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

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

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

       this.IsClass = isClass;

+      this.IsGhost = isGhost;

       this.IsUse = isUse;

       this.TypeArgs = typeArgs;

       this.Formals = formals;

@@ -698,29 +704,47 @@ namespace Microsoft.Dafny
       }

     } }

     public bool IsMutable { get { return true; } }

+    protected bool isGhost;

+    public bool IsGhost { get { return isGhost; } }

 

     public readonly DeterminedAssignmentRhs Rhs;

     invariant OptionalType != null || Rhs != null;

     

-    public VarDecl(Token! tok, string! name, Type type, DeterminedAssignmentRhs rhs)

+    public VarDecl(Token! tok, string! name, Type type, bool isGhost, DeterminedAssignmentRhs rhs)

       requires type != null || rhs != null;

     {

       this.name = name;

       this.OptionalType = type;

+      this.isGhost = isGhost;

       this.Rhs = rhs;

       base(tok);

     }

   }

   

+  public class AutoVarDecl : VarDecl {

+    public readonly int Index;

+    public AutoVarDecl(Token! tok, string! name, Type! type, int index)

+    {

+      Index = index;

+      base(tok, name, type, false, null);

+    }

+    /// <summary>

+    /// This method retrospectively makes the VarDecl a ghost.  It is to be used only during resolution.

+    /// </summary>

+    public void MakeGhost() {

+      isGhost = true;

+    }

+  }

+  

   public class CallStmt : Statement {

-    public readonly List<VarDecl!>! NewVars;

+    public readonly List<AutoVarDecl!>! NewVars;

     public readonly List<IdentifierExpr!>! Lhs;

     public readonly Expression! Receiver;

     public readonly string! MethodName;

     public readonly List<Expression!>! Args;

     public Method Method;  // filled in by resolution

     

-    public CallStmt(Token! tok, List<VarDecl!>! newVars, List<IdentifierExpr!>! lhs, Expression! receiver, string! methodName, List<Expression!>! args) {

+    public CallStmt(Token! tok, List<AutoVarDecl!>! newVars, List<IdentifierExpr!>! lhs, Expression! receiver, string! methodName, List<Expression!>! args) {

       this.NewVars = newVars;

       this.Lhs = lhs;

       this.Receiver = receiver;

diff --git a/Source/Dafny/Parser.ssc b/Source/Dafny/Parser.ssc
index 0560a45b..3a349f43 100644
--- a/Source/Dafny/Parser.ssc
+++ b/Source/Dafny/Parser.ssc
@@ -34,10 +34,11 @@ struct MemberModifiers {
 // helper routine for parsing call statements

 private static void RecordCallLhs(IdentifierExpr! e,

                                   List<IdentifierExpr!>! lhs,

-                                  List<VarDecl!>! newVars) {

+                                  List<AutoVarDecl!>! newVars) {

+  int index = lhs.Count;

   lhs.Add(e);

   if (parseVarScope.Find(e.Name) == null) {

-    VarDecl d = new VarDecl(e.tok, e.Name, new InferredTypeProxy(), null);

+    AutoVarDecl d = new AutoVarDecl(e.tok, e.Name, new InferredTypeProxy(), index);

     newVars.Add(d);

     parseVarScope.Push(e.Name, e.Name);

   }

@@ -284,9 +285,14 @@ 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 isFunctionMethod = false;

 		

 		Expect(30);

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

+		if (t.kind == 16) {

+			Get();

+			isFunctionMethod = true; 

+		}

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

 		

 		while (t.kind == 5) {

 			Attribute(ref attrs);

@@ -296,7 +302,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			GenericParameters(typeArgs);

 		}

 		parseVarScope.PushMarker(); 

-		Formals(true, formals);

+		Formals(true, false, formals);

 		Expect(13);

 		Type(out returnType);

 		if (t.kind == 10) {

@@ -312,7 +318,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			body = bb; 

 		} else Error(95);

 		parseVarScope.PopMarker();

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

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

 		

 	}

 

@@ -339,10 +345,10 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			GenericParameters(typeArgs);

 		}

 		parseVarScope.PushMarker(); 

-		Formals(true, ins);

+		Formals(true, true, ins);

 		if (t.kind == 17) {

 			Get();

-			Formals(false, outs);

+			Formals(false, true, outs);

 		}

 		if (t.kind == 10) {

 			Get();

@@ -389,11 +395,11 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		Expect(23);

 		if (StartOf(5)) {

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

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

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

 			while (t.kind == 12) {

 				Get();

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

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

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

 			}

 		}

 		Expect(24);

@@ -405,6 +411,15 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		Type(out ty);

 	}

 

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

+		isGhost = false; 

+		if (t.kind == 7) {

+			Get();

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

+		}

+		IdentType(out id, out ty);

+	}

+

 	static void Type(out Type! ty) {

 		Token! tok; 

 		TypeAndToken(out tok, out ty);

@@ -477,16 +492,16 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		} else Error(97);

 	}

 

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

-		Token! id;  Type! ty; 

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

+		Token! id;  Type! ty;  bool isGhost; 

 		Expect(23);

-		if (t.kind == 1) {

-			IdentType(out id, out ty);

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

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

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

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

 			while (t.kind == 12) {

 				Get();

-				IdentType(out id, out ty);

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

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

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

 			}

 		}

 		Expect(24);

@@ -796,16 +811,17 @@ List<Expression!>! decreases) {
 	}

 

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

-		VarDecl! d; 

+		VarDecl! d;  bool isGhost = false; 

 		if (t.kind == 7) {

 			Get();

+			isGhost = true; 

 		}

 		Expect(11);

-		IdentTypeRhs(out d);

+		IdentTypeRhs(out d, isGhost);

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

 		while (t.kind == 12) {

 			Get();

-			IdentTypeRhs(out d);

+			IdentTypeRhs(out d, isGhost);

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

 		}

 		Expect(10);

@@ -872,7 +888,7 @@ List<Expression!>! decreases) {
 		Token! x, id;

 		Expression! e;

 		List<IdentifierExpr!> lhs = new List<IdentifierExpr!>();

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

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

 		

 		Expect(46);

 		x = token; 

@@ -1064,7 +1080,7 @@ List<Expression!>! decreases) {
 		}

 	}

 

-	static void IdentTypeRhs(out VarDecl! d) {

+	static void IdentTypeRhs(out VarDecl! d, bool isGhost) {

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

 		Expression rhs = null;  Type newType = null;

 		Type optionalType = null;  DeterminedAssignmentRhs optionalRhs = null;

@@ -1087,7 +1103,7 @@ List<Expression!>! decreases) {
 		} else if (optionalType == null) {

 		  optionalType = new InferredTypeProxy();

 		}

-		d = new VarDecl(id, id.val, optionalType, optionalRhs);

+		d = new VarDecl(id, id.val, optionalType, isGhost, optionalRhs);

 		

 	}

 

diff --git a/Source/Dafny/Printer.ssc b/Source/Dafny/Printer.ssc
index 23e6dfce..93b793f2 100644
--- a/Source/Dafny/Printer.ssc
+++ b/Source/Dafny/Printer.ssc
@@ -128,6 +128,7 @@ namespace Microsoft.Dafny {
       string k = "function";

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

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

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

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

       PrintFormals(f.Formals);

       wr.Write(": ");

@@ -175,6 +176,7 @@ namespace Microsoft.Dafny {
       Indent(IndentAmount);

       string k = "method";

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

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

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

       PrintFormals(method.Ins);

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

@@ -213,6 +215,9 @@ namespace Microsoft.Dafny {
     }

     

     void PrintFormal(Formal! f) {

+      if (f.IsGhost) {

+        wr.Write("ghost ");

+      }

       if (!f.Name.StartsWith("#")) {

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

       }

@@ -303,6 +308,9 @@ namespace Microsoft.Dafny {
         

       } else if (stmt is VarDecl) {

         VarDecl s = (VarDecl)stmt;

+        if (s.IsGhost) {

+          wr.Write("ghost ");

+        }

         wr.Write("var {0}", s.Name);

         if (s.OptionalType != null) {

           wr.Write(": ");

diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc
index df93aece..11dabf9d 100644
--- a/Source/Dafny/Resolver.ssc
+++ b/Source/Dafny/Resolver.ssc
@@ -276,7 +276,7 @@ namespace Microsoft.Dafny {
       for (; attrs != null; attrs = attrs.Prev) {

         foreach (Attributes.Argument aa in attrs.Args) {

           if (aa.E != null) {

-            ResolveExpression(aa.E, twoState);

+            ResolveExpression(aa.E, twoState, true);

           }

         }

       }

@@ -286,7 +286,7 @@ namespace Microsoft.Dafny {
       // order does not matter for resolution, so resolve them in reverse order

       for (; trigs != null; trigs = trigs.Prev) {

         foreach (Expression e in trigs.Terms) {

-          ResolveExpression(e, twoState);

+          ResolveExpression(e, twoState, true);

         }

       }

     }

@@ -331,14 +331,14 @@ namespace Microsoft.Dafny {
         scope.Push(p.Name, p);

       }

       foreach (Expression r in f.Req) {

-        ResolveExpression(r, false);

+        ResolveExpression(r, false, true);

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

         if (!UnifyTypes(r.Type, Type.Bool)) {

           Error(r, "Precondition must be a boolean (got {0})", r.Type);

         }

       }

       foreach (Expression r in f.Reads) {

-        ResolveExpression(r, false);

+        ResolveExpression(r, false, true);

         Type t = r.Type;

         assert t != null;  // follows from postcondition of ResolveExpression

         if (t is CollectionType) {

@@ -353,11 +353,11 @@ namespace Microsoft.Dafny {
         }

       }

       foreach (Expression r in f.Decreases) {

-        ResolveExpression(r, false);

+        ResolveExpression(r, false, true);

         // any type is fine

       }

       if (f.Body != null) {

-        ResolveExpression(f.Body, false);

+        ResolveExpression(f.Body, false, f.IsGhost);

         assert f.Body.Type != null;  // follows from postcondition of ResolveExpression

         if (!UnifyTypes(f.Body.Type, f.ResultType)) {

           Error(f, "Function body type mismatch (expected {0}, got {1})", f.ResultType, f.Body.Type);

@@ -403,14 +403,14 @@ namespace Microsoft.Dafny {
       

       // Start resolving specification...

       foreach (MaybeFreeExpression e in m.Req) {

-        ResolveExpression(e.E, false);

+        ResolveExpression(e.E, false, true);

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

         if (!UnifyTypes(e.E.Type, Type.Bool)) {

           Error(e.E, "Precondition must be a boolean (got {0})", e.E.Type);

         }

       }

       foreach (Expression e in m.Mod) {

-        ResolveExpression(e, false);

+        ResolveExpression(e, false, true);

         Type t = e.Type;

         assert t != null;  // follows from postcondition of ResolveExpression

         if (t is CollectionType) {

@@ -425,7 +425,7 @@ namespace Microsoft.Dafny {
         }

       }

       foreach (Expression e in m.Decreases) {

-        ResolveExpression(e, false);

+        ResolveExpression(e, false, true);

         // any type is fine

       }

       

@@ -436,7 +436,7 @@ namespace Microsoft.Dafny {
 

       // ... continue resolving specification

       foreach (MaybeFreeExpression e in m.Ens) {

-        ResolveExpression(e.E, true);

+        ResolveExpression(e.E, true, true);

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

         if (!UnifyTypes(e.E.Type, Type.Bool)) {

           Error(e.E, "Postcondition must be a boolean (got {0})", e.E.Type);

@@ -445,7 +445,7 @@ namespace Microsoft.Dafny {
       

       // Resolve body

       if (m.Body != null) {

-        ResolveStatement(m.Body);

+        ResolveStatement(m.Body, m.IsGhost);

       }

       

       scope.PopMarker();

@@ -722,12 +722,12 @@ namespace Microsoft.Dafny {
       }

     }

     

-    public void ResolveStatement(Statement! stmt)

+    public void ResolveStatement(Statement! stmt, bool specContextOnly)

       requires !(stmt is LabelStmt);  // these should be handled inside lists of statements

     {

       if (stmt is UseStmt) {

         UseStmt s = (UseStmt)stmt;

-        ResolveExpression(s.Expr, true);

+        ResolveExpression(s.Expr, true, true);

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

         Expression expr = s.Expr;

         while (true) {

@@ -743,7 +743,7 @@ namespace Microsoft.Dafny {
         }

       } else if (stmt is PredicateStmt) {

         PredicateStmt s = (PredicateStmt)stmt;

-        ResolveExpression(s.Expr, true);

+        ResolveExpression(s.Expr, true, true);

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

         if (!UnifyTypes(s.Expr.Type, Type.Bool)) {

           Error(s.Expr, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Expr.Type);

@@ -765,20 +765,40 @@ namespace Microsoft.Dafny {
         

       } else if (stmt is AssignStmt) {

         AssignStmt s = (AssignStmt)stmt;

-        ResolveExpression(s.Lhs, true);

+        int prevErrorCount = ErrorCount;

+        ResolveExpression(s.Lhs, true, true);  // allow ghosts for now, but see FieldSelectExpr LHS case below

+        bool lhsResolvedSuccessfully = ErrorCount == prevErrorCount;

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

         // check that LHS denotes a mutable variable or a field

+        bool lvalueIsGhost = true;

         if (s.Lhs is IdentifierExpr) {

           IVariable var = ((IdentifierExpr)s.Lhs).Var;

           if (var == null) {

             // the LHS didn't resolve correctly; some error would already have been reported

-          } else if (!var.IsMutable) {

-            Error(stmt, "LHS of assignment must denote a mutable variable or field");

+          } else {

+            lvalueIsGhost = var.IsGhost;

+            if (!var.IsMutable) {

+              Error(stmt, "LHS of assignment must denote a mutable variable or field");

+            }

           }

         } else if (s.Lhs is FieldSelectExpr) {

           // LHS is fine, but restrict the RHS to ExprRhs

           if (!(s.Rhs is ExprRhs)) {

             Error(stmt, "Assignment to field must have an expression RHS; try using a temporary local variable");

+          } else {

+            FieldSelectExpr fse = (FieldSelectExpr)s.Lhs;

+            lvalueIsGhost = ((!)fse.Field).IsGhost;

+            if (!lvalueIsGhost) {

+              if (specContextOnly) {

+                Error(stmt, "Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");

+              } else {

+                // It is now that we wish we would have resolved s.Lhs to not allow ghosts.  Too late, so we do

+                // the next best thing.

+                if (lhsResolvedSuccessfully && UsesSpecFeatures(fse.Obj)) {

+                  Error(stmt, "Assignment to non-ghost field is not allowed to use specification-only expressions in the receiver");

+                }

+              }

+            }

           }

         } else {

           Error(stmt, "LHS of assignment must denote a mutable variable or field");

@@ -786,7 +806,7 @@ namespace Microsoft.Dafny {
         

         if (s.Rhs is ExprRhs) {

           ExprRhs rr = (ExprRhs)s.Rhs;

-          ResolveExpression(rr.Expr, true);

+          ResolveExpression(rr.Expr, true, lvalueIsGhost);

           assert rr.Expr.Type != null;  // follows from postcondition of ResolveExpression

           if (!UnifyTypes(s.Lhs.Type, rr.Expr.Type)) {

             Error(stmt, "RHS (of type {0}) not assignable to LHS (of type {1})", rr.Expr.Type, s.Lhs.Type);

@@ -815,7 +835,7 @@ namespace Microsoft.Dafny {
           Type! rhsType;

           if (s.Rhs is ExprRhs) {

             ExprRhs rr = (ExprRhs)s.Rhs;

-            ResolveExpression(rr.Expr, true);

+            ResolveExpression(rr.Expr, true, s.IsGhost);

             assert rr.Expr.Type != null;  // follows from postcondition of ResolveExpression

             rhsType = rr.Expr.Type;

           } else if (s.Rhs is TypeRhs) {

@@ -841,72 +861,89 @@ namespace Microsoft.Dafny {
       

       } else if (stmt is CallStmt) {

         CallStmt s = (CallStmt)stmt;

-        

+

+        // resolve receiver

+        ResolveReceiver(s.Receiver, true, false);

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

+        // resolve the method name

+        UserDefinedType ctype;

+        MemberDecl member = ResolveMember(s.Tok, s.Receiver.Type, s.MethodName, out ctype);

+        Method method = null;

+        if (member == null) {

+          // error has already been reported by ResolveMember

+        } else if (!(member is Method)) {

+          Error(s, "member {0} in class {1} does not refer to a method", s.MethodName, ((!)ctype).Name);

+        } else {

+          method = (Method)member;

+          s.Method = method;

+          if (specContextOnly && !method.IsGhost) {

+            Error(s, "only ghost methods can be called from this context");

+          }

+        }

+

         // resolve any local variables declared here

-        foreach (VarDecl local in s.NewVars) {

-          ResolveStatement(local);

+        foreach (AutoVarDecl local in s.NewVars) {

+          // first, fix up the local variables to be ghost variable if the corresponding formal out-parameter is a ghost

+          if (method != null && local.Index < method.Outs.Count && method.Outs[local.Index].IsGhost) {

+            local.MakeGhost();

+          }

+          ResolveStatement(local, specContextOnly);

         }

         

         // resolve left-hand side

         Dictionary<string!,object> lhsNameSet = new Dictionary<string!,object>();

         foreach (IdentifierExpr lhs in s.Lhs) {

-          ResolveExpression(lhs, true);

+          ResolveExpression(lhs, true, true);

           if (lhsNameSet.ContainsKey(lhs.Name)) {

             Error(s, "Duplicate variable in left-hand side of call statement: {0}", lhs.Name);

           } else {

             lhsNameSet.Add(lhs.Name, null);

           }

         }

-        // resolve receiver

-        ResolveReceiver(s.Receiver, true);

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

         // resolve arguments

+        int j = 0;

         foreach (Expression e in s.Args) {

-          ResolveExpression(e, true);

+          bool allowGhost = method == null || method.Ins.Count <= j || method.Ins[j].IsGhost;

+          ResolveExpression(e, true, allowGhost);

+          j++;

         }

         

-        // resolve the method name

-        UserDefinedType ctype;

-        MemberDecl member = ResolveMember(s.Tok, s.Receiver.Type, s.MethodName, out ctype);

-        if (member == null) {

-          // error has already been reported by ResolveMember

-        } else if (!(member is Method)) {

-          Error(s, "member {0} in class {1} does not refer to a method", s.MethodName, ((!)ctype).Name);

+        if (method == null) {

+          // error has been reported above

+        } else if (method.Ins.Count != s.Args.Count) {

+          Error(s, "wrong number of method arguments (got {0}, expected {1})", s.Args.Count, method.Ins.Count);

+        } else if (method.Outs.Count != s.Lhs.Count) {

+          Error(s, "wrong number of method result arguments (got {0}, expected {1})", s.Lhs.Count, method.Outs.Count);

         } else {

-          Method method = (Method)member;

-          s.Method = method;

-          if (method.Ins.Count != s.Args.Count) {

-            Error(s, "wrong number of method arguments (got {0}, expected {1})", s.Args.Count, method.Ins.Count);

-          } else if (method.Outs.Count != s.Lhs.Count) {

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

-              subst.Add(((!)ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);

-            }

-            foreach (TypeParameter p in method.TypeArgs) {

-              subst.Add(p, new ParamTypeProxy(p));

-            }

-            // type check the arguments

-            for (int i = 0; i < method.Ins.Count; i++) {

-              Type st = SubstType(method.Ins[i].Type, subst);

-              if (!UnifyTypes((!)s.Args[i].Type, st)) {

-                Error(s, "incorrect type of method in-parameter {0} (expected {1}, got {2})", i, st, s.Args[i].Type);

-              }

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

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

+            subst.Add(((!)ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);

+          }

+          foreach (TypeParameter p in method.TypeArgs) {

+            subst.Add(p, new ParamTypeProxy(p));

+          }

+          // type check the arguments

+          for (int i = 0; i < method.Ins.Count; i++) {

+            Type st = SubstType(method.Ins[i].Type, subst);

+            if (!UnifyTypes((!)s.Args[i].Type, st)) {

+              Error(s, "incorrect type of method in-parameter {0} (expected {1}, got {2})", i, st, s.Args[i].Type);

             }

-            for (int i = 0; i < method.Outs.Count; i++) {

-              Type st = SubstType(method.Outs[i].Type, subst);

-              if (!UnifyTypes((!)s.Lhs[i].Type, st)) {

-                Error(s, "incorrect type of method out-parameter {0} (expected {1}, got {2})", i, st, s.Lhs[i].Type);

-              }

+          }

+          for (int i = 0; i < method.Outs.Count; i++) {

+            Type st = SubstType(method.Outs[i].Type, subst);

+            IdentifierExpr lhs = s.Lhs[i];

+            if (!UnifyTypes((!)lhs.Type, st)) {

+              Error(s, "incorrect type of method out-parameter {0} (expected {1}, got {2})", i, st, lhs.Type);

+            } else if (!specContextOnly && !((!)lhs.Var).IsGhost && method.Outs[i].IsGhost) {

+              Error(s, "actual out-parameter {0} is required to be a ghost variable", i);

             }

           }

         }

@@ -922,7 +959,7 @@ namespace Microsoft.Dafny {
             assert b;  // since we just pushed a marker, we expect the Push to succeed

             labelsToPop++;

           } else {

-            ResolveStatement(ss);

+            ResolveStatement(ss, specContextOnly);

             for (; 0 < labelsToPop; labelsToPop--) { labeledStatements.PopMarker(); }

           }

         }

@@ -931,39 +968,51 @@ namespace Microsoft.Dafny {
       

       } else if (stmt is IfStmt) {

         IfStmt s = (IfStmt)stmt;

+        bool branchesAreSpecOnly = specContextOnly;

         if (s.Guard != null) {

-          ResolveExpression(s.Guard, true);

+          int prevErrorCount = ErrorCount;

+          ResolveExpression(s.Guard, true, true);

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

+          bool successfullyResolved = ErrorCount == prevErrorCount;

           if (!UnifyTypes(s.Guard.Type, Type.Bool)) {

             Error(s.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Guard.Type);

           }

+          if (!specContextOnly && successfullyResolved) {

+            branchesAreSpecOnly = UsesSpecFeatures(s.Guard);

+          }

         }

-        ResolveStatement(s.Thn);

+        ResolveStatement(s.Thn, branchesAreSpecOnly);

         if (s.Els != null) {

-          ResolveStatement(s.Els);

+          ResolveStatement(s.Els, branchesAreSpecOnly);

         }

       

       } else if (stmt is WhileStmt) {

         WhileStmt s = (WhileStmt)stmt;

+        bool bodyIsSpecOnly = specContextOnly;

         if (s.Guard != null) {

-          ResolveExpression(s.Guard, true);

+          int prevErrorCount = ErrorCount;

+          ResolveExpression(s.Guard, true, true);

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

+          bool successfullyResolved = ErrorCount == prevErrorCount;

           if (!UnifyTypes(s.Guard.Type, Type.Bool)) {

             Error(s.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Guard.Type);

           }

+          if (!specContextOnly && successfullyResolved) {

+            bodyIsSpecOnly = UsesSpecFeatures(s.Guard);

+          }

         }

         foreach (MaybeFreeExpression inv in s.Invariants) {

-          ResolveExpression(inv.E, true);

+          ResolveExpression(inv.E, true, true);

           assert inv.E.Type != null;  // follows from postcondition of ResolveExpression

           if (!UnifyTypes(inv.E.Type, Type.Bool)) {

             Error(inv.E, "invariant is expected to be of type {0}, but is {1}", Type.Bool, inv.E.Type);

           }

         }

         foreach (Expression e in s.Decreases) {

-          ResolveExpression(e, true);

+          ResolveExpression(e, true, true);

           // any type is fine

         }

-        ResolveStatement(s.Body);

+        ResolveStatement(s.Body, bodyIsSpecOnly);

       

       } else if (stmt is ForeachStmt) {

         ForeachStmt s = (ForeachStmt)stmt;

@@ -971,24 +1020,28 @@ namespace Microsoft.Dafny {
         bool b = scope.Push(s.BoundVar.Name, s.BoundVar);

         assert b;  // since we just pushed a marker, we expect the Push to succeed

         ResolveType(s.BoundVar.Type);

+        int prevErrorCount = ErrorCount;

         

-        ResolveExpression(s.Collection, true);

+        ResolveExpression(s.Collection, true, true);

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

         if (!UnifyTypes(s.Collection.Type, new CollectionTypeProxy(s.BoundVar.Type))) {

           Error(s.Collection, "The type is expected to be a collection of {0} (instead got {1})", s.BoundVar.Type, s.Collection.Type);

         }

         

-        ResolveExpression(s.Range, true);

+        ResolveExpression(s.Range, true, true);

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

         if (!UnifyTypes(s.Range.Type, Type.Bool)) {

           Error(s.Range, "range condition is expected to be of type {0}, but is {1}", Type.Bool, s.Range.Type);

         }

+        bool successfullyResolvedCollectionAndRange = ErrorCount == prevErrorCount;

         

         foreach (PredicateStmt ss in s.BodyPrefix) {

-          ResolveStatement(ss);

+          ResolveStatement(ss, specContextOnly);

         }

         if (s.BodyAssign != null) {

-          ResolveStatement(s.BodyAssign);

+          bool specOnly = specContextOnly ||

+                          (successfullyResolvedCollectionAndRange && (UsesSpecFeatures(s.Collection) || UsesSpecFeatures(s.Range)));

+          ResolveStatement(s.BodyAssign, specOnly);

           // check for correct usage of BoundVar in LHS and RHS of this assignment

           FieldSelectExpr lhs = s.BodyAssign.Lhs as FieldSelectExpr;

           IdentifierExpr obj = lhs == null ? null : lhs.Obj as IdentifierExpr;

@@ -1101,7 +1154,7 @@ namespace Microsoft.Dafny {
     /// <summary>

     /// "twoState" implies that "old" and "fresh" expressions are allowed

     /// </summary>

-    void ResolveExpression(Expression! expr, bool twoState)

+    void ResolveExpression(Expression! expr, bool twoState, bool specContext)

       requires currentClass != null;

       ensures expr.Type != null;

     {

@@ -1140,6 +1193,9 @@ namespace Microsoft.Dafny {
           Error(expr, "Identifier does not denote a local variable, parameter, or bound variable: {0}", e.Name);

         } else {

           expr.Type = e.Var.Type;

+          if (!specContext && e.Var.IsGhost) {

+            Error(expr, "ghost variables are allowed only in specification contexts");

+          }

         }

       

       } else if (expr is DatatypeValue) {

@@ -1178,7 +1234,7 @@ namespace Microsoft.Dafny {
           }

           int j = 0;

           foreach (Expression arg in dtv.Arguments) {

-            ResolveExpression(arg, twoState);

+            ResolveExpression(arg, twoState, specContext);

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

             if (ctor != null && j < ctor.Formals.Count) {

               Type st = SubstType(ctor.Formals[j].Type, subst);

@@ -1194,7 +1250,7 @@ namespace Microsoft.Dafny {
         DisplayExpression e = (DisplayExpression)expr;

         Type elementType = new InferredTypeProxy();

         foreach (Expression ee in e.Elements) {

-          ResolveExpression(ee, twoState);

+          ResolveExpression(ee, twoState, specContext);

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

           if (!UnifyTypes(elementType, ee.Type)) {

             Error(ee, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", ee.Type, elementType); 

@@ -1208,7 +1264,7 @@ namespace Microsoft.Dafny {
         

       } else if (expr is FieldSelectExpr) {

         FieldSelectExpr e = (FieldSelectExpr)expr;

-        ResolveExpression(e.Obj, twoState);

+        ResolveExpression(e.Obj, twoState, specContext);

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

         UserDefinedType ctype;

         MemberDecl member = ResolveMember(expr.tok, e.Obj.Type, e.FieldName, out ctype);

@@ -1225,12 +1281,15 @@ namespace Microsoft.Dafny {
             subst.Add(ctype.ResolvedClass.TypeArgs[i], ctype.TypeArgs[i]);

           }

           e.Type = SubstType(e.Field.Type, subst);

+          if (!specContext && e.Field.IsGhost) {

+            Error(expr, "ghost fields are allowed only in specification contexts");

+          }

         }

       

       } else if (expr is SeqSelectExpr) {

         SeqSelectExpr e = (SeqSelectExpr)expr;

         bool seqErr = false;

-        ResolveExpression(e.Seq, twoState);

+        ResolveExpression(e.Seq, twoState, specContext);

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

         Type elementType = new InferredTypeProxy();

         if (!UnifyTypes(e.Seq.Type, new SeqType(elementType))) {

@@ -1238,14 +1297,14 @@ namespace Microsoft.Dafny {
           seqErr = true;

         }

         if (e.E0 != null) {

-          ResolveExpression(e.E0, twoState);

+          ResolveExpression(e.E0, twoState, specContext);

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

           if (!UnifyTypes(e.E0.Type, Type.Int)) {

             Error(e.E0, "sequence selection requires integer indices (got {0})", e.E0.Type);

           }

         }

         if (e.E1 != null) {

-          ResolveExpression(e.E1, twoState);

+          ResolveExpression(e.E1, twoState, specContext);

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

           if (!UnifyTypes(e.E1.Type, Type.Int)) {

             Error(e.E1, "sequence selection requires integer indices (got {0})", e.E1.Type);

@@ -1262,19 +1321,19 @@ namespace Microsoft.Dafny {
       } else if (expr is SeqUpdateExpr) {

         SeqUpdateExpr e = (SeqUpdateExpr)expr;

         bool seqErr = false;

-        ResolveExpression(e.Seq, twoState);

+        ResolveExpression(e.Seq, twoState, specContext);

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

         Type elementType = new InferredTypeProxy();

         if (!UnifyTypes(e.Seq.Type, new SeqType(elementType))) {

           Error(expr, "sequence update requires a sequence (got {0})", e.Seq.Type);

           seqErr = true;

         }

-        ResolveExpression(e.Index, twoState);

+        ResolveExpression(e.Index, twoState, specContext);

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

         if (!UnifyTypes(e.Index.Type, Type.Int)) {

           Error(e.Index, "sequence update requires integer index (got {0})", e.Index.Type);

         }

-        ResolveExpression(e.Value, twoState);

+        ResolveExpression(e.Value, twoState, specContext);

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

         if (!UnifyTypes(e.Value.Type, elementType)) {

           Error(e.Value, "sequence update requires the value to have the element type of the sequence (got {0})", e.Value.Type);

@@ -1285,7 +1344,7 @@ namespace Microsoft.Dafny {
         

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

-        ResolveReceiver(e.Receiver, twoState);

+        ResolveReceiver(e.Receiver, twoState, specContext);

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

         UserDefinedType ctype;

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

@@ -1296,6 +1355,9 @@ namespace Microsoft.Dafny {
         } else {

           Function function = (Function)member;

           e.Function = function;

+          if (!specContext && function.IsGhost) {

+            Error(expr, "function calls are allowed only in specification contexts (consider declaring the function a 'function method')");

+          }

           if (function.Formals.Count != e.Args.Count) {

             Error(expr, "wrong number of function arguments (got {0}, expected {1})", e.Args.Count, function.Formals.Count);

           } else {

@@ -1321,7 +1383,7 @@ namespace Microsoft.Dafny {
             // type check the arguments

             for (int i = 0; i < function.Formals.Count; i++) {

               Expression farg = e.Args[i];

-              ResolveExpression(farg, twoState);

+              ResolveExpression(farg, twoState, specContext);

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

               Type s = SubstType(function.Formals[i].Type, subst);

               if (!UnifyTypes(farg.Type, s)) {

@@ -1337,7 +1399,7 @@ namespace Microsoft.Dafny {
         if (!twoState) {

           Error(expr, "old expressions are not allowed in this context");

         }

-        ResolveExpression(e.E, twoState);

+        ResolveExpression(e.E, twoState, specContext);

         expr.Type = e.E.Type;

         

       } else if (expr is FreshExpr) {

@@ -1345,7 +1407,7 @@ namespace Microsoft.Dafny {
         if (!twoState) {

           Error(expr, "fresh expressions are not allowed in this context");

         }

-        ResolveExpression(e.E, twoState);

+        ResolveExpression(e.E, twoState, specContext);

         // the type of e.E must be either an object or a collection of objects

         Type t = e.E.Type;

         assert t != null;  // follows from postcondition of ResolveExpression

@@ -1363,7 +1425,7 @@ namespace Microsoft.Dafny {
         

       } else if (expr is UnaryExpr) {

         UnaryExpr e = (UnaryExpr)expr;

-        ResolveExpression(e.E, twoState);

+        ResolveExpression(e.E, twoState, specContext);

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

         switch (e.Op) {

           case UnaryExpr.Opcode.Not:

@@ -1384,9 +1446,9 @@ namespace Microsoft.Dafny {
         

       } else if (expr is BinaryExpr) {

         BinaryExpr e = (BinaryExpr)expr;

-        ResolveExpression(e.E0, twoState);

+        ResolveExpression(e.E0, twoState, specContext);

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

-        ResolveExpression(e.E1, twoState);

+        ResolveExpression(e.E1, twoState, specContext);

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

         switch (e.Op) {

           case BinaryExpr.Opcode.Iff:

@@ -1490,13 +1552,16 @@ namespace Microsoft.Dafny {
       } else if (expr is QuantifierExpr) {

         QuantifierExpr e = (QuantifierExpr)expr;

         scope.PushMarker();

+        if (!specContext) {

+          Error(expr, "quantifiers are allowed only in specification contexts");

+        }

         foreach (BoundVar v in e.BoundVars) {

           if (!scope.Push(v.Name, v)) {

-            Error(v, "Duplicate parameter name: {0}", v.Name);

+            Error(v, "Duplicate bound-variable name: {0}", v.Name);

           }

           ResolveType(v.Type);

         }

-        ResolveExpression(e.Body, twoState);

+        ResolveExpression(e.Body, twoState, specContext);

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

         if (!UnifyTypes(e.Body.Type, Type.Bool)) {

           Error(expr, "body of quantifier must be of type bool (instead got {0})", e.Body.Type);

@@ -1513,11 +1578,11 @@ namespace Microsoft.Dafny {
         

       } else if (expr is ITEExpr) {

         ITEExpr e = (ITEExpr)expr;

-        ResolveExpression(e.Test, twoState);

+        ResolveExpression(e.Test, twoState, specContext);

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

-        ResolveExpression(e.Thn, twoState);

+        ResolveExpression(e.Thn, twoState, specContext);

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

-        ResolveExpression(e.Els, twoState);

+        ResolveExpression(e.Els, twoState, specContext);

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

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

@@ -1531,7 +1596,7 @@ namespace Microsoft.Dafny {
       } else if (expr is MatchExpr) {

         MatchExpr me = (MatchExpr)expr;

         assert !twoState;  // currently, match expressions are allowed only at the outermost level of function bodies

-        ResolveExpression(me.Source, twoState);

+        ResolveExpression(me.Source, twoState, specContext);

         assert me.Source.Type != null;  // follows from postcondition of ResolveExpression

         UserDefinedType sourceType = null;

         DatatypeDecl dtd = null;

@@ -1602,7 +1667,7 @@ namespace Microsoft.Dafny {
             }

             i++;

           }

-          ResolveExpression(mc.Body, twoState);

+          ResolveExpression(mc.Body, twoState, specContext);

           assert mc.Body.Type != null;  // follows from postcondition of ResolveExpression

           if (!UnifyTypes(expr.Type, mc.Body.Type)) {

             Error(mc.Body.tok, "type of case bodies do not agree (found {0}, previous types {1})", mc.Body.Type, expr.Type);

@@ -1623,7 +1688,7 @@ namespace Microsoft.Dafny {
       }

     }

     

-    void ResolveReceiver(Expression! expr, bool twoState)

+    void ResolveReceiver(Expression! expr, bool twoState, bool specContext)

       requires currentClass != null;

       ensures expr.Type != null;

     {

@@ -1632,7 +1697,7 @@ namespace Microsoft.Dafny {
         // making sure 'this' does not really get used when it's not available.

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

       } else {

-        ResolveExpression(expr, twoState);

+        ResolveExpression(expr, twoState, specContext);

       }

     }

     

@@ -1729,8 +1794,78 @@ namespace Microsoft.Dafny {
           assert false;  // unexpected operator

       }

     }

+

+    /// <summary>

+    /// Returns whether or not 'expr' has any subexpression that uses some feature (like a ghost or quantifier)

+    /// that is allowed only in specification contexts.

+    /// Requires 'expr' to be a successfully resolved expression.

+    /// </summary>

+    bool UsesSpecFeatures(Expression! expr)

+      requires currentClass != null;

+    {

+      if (expr is LiteralExpr) {

+        return false;

+      } else if (expr is ThisExpr) {

+        return false;

+      } else if (expr is IdentifierExpr) {

+        IdentifierExpr e = (IdentifierExpr)expr;

+        return ((!)e.Var).IsGhost;

+      } else if (expr is DatatypeValue) {

+        DatatypeValue dtv = (DatatypeValue)expr;

+        return exists{Expression arg in dtv.Arguments; UsesSpecFeatures(arg)};

+      } else if (expr is DisplayExpression) {

+        DisplayExpression e = (DisplayExpression)expr;

+        return exists{Expression ee in e.Elements; UsesSpecFeatures(ee)};

+      } else if (expr is FieldSelectExpr) {

+        FieldSelectExpr e = (FieldSelectExpr)expr;

+        return ((!)e.Field).IsGhost || UsesSpecFeatures(e.Obj);

+      } else if (expr is SeqSelectExpr) {

+        SeqSelectExpr e = (SeqSelectExpr)expr;

+        return UsesSpecFeatures(e.Seq) ||

+               (e.E0 != null && UsesSpecFeatures(e.E0)) ||

+               (e.E1 != null && UsesSpecFeatures(e.E1));

+      } else if (expr is SeqUpdateExpr) {

+        SeqUpdateExpr e = (SeqUpdateExpr)expr;

+        return UsesSpecFeatures(e.Seq) ||

+               (e.Index != null && UsesSpecFeatures(e.Index)) ||

+               (e.Value != null && UsesSpecFeatures(e.Value));

+      } else if (expr is FunctionCallExpr) {

+        FunctionCallExpr e = (FunctionCallExpr)expr;

+        if (((!)e.Function).IsGhost) {

+          return true;

+        }

+        return exists{Expression arg in e.Args; UsesSpecFeatures(arg)};

+      } else if (expr is OldExpr) {

+        OldExpr e = (OldExpr)expr;

+        return UsesSpecFeatures(e.E);

+      } else if (expr is FreshExpr) {

+        FreshExpr e = (FreshExpr)expr;

+        return UsesSpecFeatures(e.E);

+      } else if (expr is UnaryExpr) {

+        UnaryExpr e = (UnaryExpr)expr;

+        return UsesSpecFeatures(e.E);

+      } else if (expr is BinaryExpr) {

+        BinaryExpr e = (BinaryExpr)expr;

+        return UsesSpecFeatures(e.E0) || UsesSpecFeatures(e.E1);

+      } else if (expr is QuantifierExpr) {

+        return true;

+      } else if (expr is WildcardExpr) {

+        return false;

+      } else if (expr is ITEExpr) {

+        ITEExpr e = (ITEExpr)expr;

+        return UsesSpecFeatures(e.Test) || UsesSpecFeatures(e.Thn) || UsesSpecFeatures(e.Els);

+      } else if (expr is MatchExpr) {

+        MatchExpr me = (MatchExpr)expr;

+        if (UsesSpecFeatures(me.Source)) {

+          return true;

+        }

+        return exists{MatchCase mc in me.Cases; UsesSpecFeatures(mc.Body)};

+      } else {

+        assert false;  // unexpected expression

+      }

+    }

   }

-    

+

   class Scope<Thing> where Thing : class {

     [Rep] readonly List<string>! names = new List<string>();  // a null means a marker

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

diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc
index 185a81ee..0615f644 100644
--- a/Source/Dafny/Translator.ssc
+++ b/Source/Dafny/Translator.ssc
@@ -1127,7 +1127,7 @@ namespace Microsoft.Dafny {
         Dictionary<IVariable,Expression!> substMap = new Dictionary<IVariable,Expression!>();

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

           Formal p = e.Function.Formals[i];

-          VarDecl local = new VarDecl(p.tok, p.Name, p.Type, null);

+          VarDecl local = new VarDecl(p.tok, p.Name, p.Type, p.IsGhost, null);

           local.type = local.OptionalType;  // resolve local here

           IdentifierExpr ie = new IdentifierExpr(local.Tok, local.UniqueName);

           ie.Var = local;  ie.Type = ie.Var.Type;  // resolve ie here

@@ -1207,7 +1207,7 @@ namespace Microsoft.Dafny {
         QuantifierExpr e = (QuantifierExpr)expr;

         Dictionary<IVariable,Expression!> substMap = new Dictionary<IVariable,Expression!>();

         foreach (BoundVar bv in e.BoundVars) {

-          VarDecl local = new VarDecl(bv.tok, bv.Name, bv.Type, null);

+          VarDecl local = new VarDecl(bv.tok, bv.Name, bv.Type, bv.IsGhost, null);

           local.type = local.OptionalType;  // resolve local here

           IdentifierExpr ie = new IdentifierExpr(local.Tok, local.UniqueName);

           ie.Var = local;  ie.Type = ie.Var.Type;  // resolve ie here

@@ -1742,7 +1742,7 @@ namespace Microsoft.Dafny {
           Dictionary<IVariable,Expression!> substMap = new Dictionary<IVariable,Expression!>();

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

             Formal p = s.Method.Ins[i];

-            VarDecl local = new VarDecl(p.tok, p.Name, p.Type, null);

+            VarDecl local = new VarDecl(p.tok, p.Name, p.Type, p.IsGhost, null);

             local.type = local.OptionalType;  // resolve local here

             IdentifierExpr ie = new IdentifierExpr(local.Tok, local.UniqueName);

             ie.Var = local;  ie.Type = ie.Var.Type;  // resolve ie here