Dafny: added ensures clauses to functions

14 files changed, 621 insertions, 331 deletions

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index eeb8024a..ef7164bc 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -574,6 +574,7 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
      List<Formal/*!*/> formals = new List<Formal/*!*/>();

      Type/*!*/ returnType;

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

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

      List<FrameExpression/*!*/> reads = new List<FrameExpression/*!*/>();

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

      Expression/*!*/ bb;  Expression body = null;

@@ -594,18 +595,18 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
   ":"

   Type<out returnType>

   ( ";"

-    { FunctionSpec<reqs, reads, decreases> }

-  | { FunctionSpec<reqs, reads, decreases> }

+    { FunctionSpec<reqs, reads, ens, decreases> }

+  | { FunctionSpec<reqs, reads, ens, decreases> }

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

   )

   (. parseVarScope.PopMarker();

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

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

      f.BodyStartTok = bodyStart;

      f.BodyEndTok = bodyEnd;

   .)

   .

 

-FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ decreases.>

+FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases.>

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

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

   ( "requires" Expression<out e> ";"      (. reqs.Add(e); .)

@@ -613,6 +614,7 @@ FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ r
               { "," PossiblyWildFrameExpression<out fe>        (. reads.Add(fe); .)

               }

 	        ] ";"

+  | "ensures" Expression<out e> ";"      (. ens.Add(e); .)

   | "decreases" Expressions<decreases> ";"

   )

   .

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index d2c955c1..9eec1e39 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -1014,6 +1014,7 @@ namespace Microsoft.Dafny {
     public readonly Type/*!*/ ResultType;

     public readonly List<Expression/*!*/>/*!*/ Req;

     public readonly List<FrameExpression/*!*/>/*!*/ Reads;

+    public readonly List<Expression/*!*/>/*!*/ Ens;

     public readonly List<Expression/*!*/>/*!*/ Decreases;

     public readonly Expression Body;  // an extended expression

     [ContractInvariantMethod]

@@ -1023,13 +1024,14 @@ namespace Microsoft.Dafny {
       Contract.Invariant(ResultType != null);

       Contract.Invariant(cce.NonNullElements(Req));

       Contract.Invariant(cce.NonNullElements(Reads));

+      Contract.Invariant(cce.NonNullElements(Ens));

       Contract.Invariant(cce.NonNullElements(Decreases));

     }

 

 

     public Function(IToken tok, string name, bool isStatic, bool isGhost, bool isUnlimited, [Captured] List<TypeParameter/*!*/>/*!*/ typeArgs,

                     [Captured] List<Formal/*!*/>/*!*/ formals, Type/*!*/ resultType, List<Expression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/*!*/ reads,

-                    List<Expression/*!*/>/*!*/ decreases, Expression body, Attributes attributes)

+                    List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases, Expression body, Attributes attributes)

       : base(tok, name, attributes) {

 

       Contract.Requires(tok != null);

@@ -1039,6 +1041,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(resultType != null);

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

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

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

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

       this.IsStatic = isStatic;

       this.IsGhost = isGhost;

@@ -1048,6 +1051,7 @@ namespace Microsoft.Dafny {
       this.ResultType = resultType;

       this.Req = req;

       this.Reads = reads;

+      this.Ens = ens;

       this.Decreases = decreases;

       this.Body = body;

 

@@ -1783,7 +1787,8 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public class IdentifierExpr : Expression {

+  public class IdentifierExpr : Expression

+  {

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Name != null);

diff --git a/Dafny/Makefile b/Dafny/Makefile
index cc36590c..2013b4f9 100644
--- a/Dafny/Makefile
+++ b/Dafny/Makefile
@@ -10,17 +10,13 @@ FRAME_DIR = ..\..\..\boogiepartners\CocoR\Modified
 # "all" depends on 2 files, really (Parser.cs and Scanner.cs), but they

 # are both generated in one go and I don't know a better way to tell

 # nmake that.  --KRML

-all: Parser.ssc 

+all: Parser.cs

 

-Parser.ssc: $(FRAME_DIR)\Scanner.frame $(FRAME_DIR)\Parser.frame Dafny.atg

+Parser.cs: $(FRAME_DIR)\Scanner.frame $(FRAME_DIR)\Parser.frame Dafny.atg

 	$(COCO) Dafny.atg -namespace Microsoft.Dafny -frames $(FRAME_DIR)

-	copy Parser.cs Parser.ssc

-	copy Scanner.cs Scanner.ssc

 

 clean:

-	if exist Scanner.ssc del Scanner.ssc

 	if exist Scanner.cs del Scanner.cs

 	if exist Scanner.cs.old del Scanner.cs.old

-	if exist Parser.ssc del Parser.ssc

 	if exist Parser.cs del Parser.cs

 	if exist Parser.cs.old del Parser.cs.old

diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index ff6f2690..1837ea9e 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -25,7 +25,7 @@ public class Parser {
 	const bool T = true;

 	const bool x = false;

 	const int minErrDist = 2;

-

+	

 	public Scanner/*!*/ scanner;

 	public Errors/*!*/  errors;

 

@@ -161,10 +161,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (errDist >= minErrDist) errors.SemErr(t, msg);

 		errDist = 0;

 	}

-

-	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {

-	  Contract.Requires(tok != null);

-	  Contract.Requires(msg != null);

+	

+    public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {

+      Contract.Requires(tok != null);

+      Contract.Requires(msg != null);

 	  errors.SemErr(tok, msg);

 	}

 

@@ -177,15 +177,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			la = t;

 		}

 	}

-

+	

 	void Expect (int n) {

 		if (la.kind==n) Get(); else { SynErr(n); }

 	}

-

+	

 	bool StartOf (int s) {

 		return set[s, la.kind];

 	}

-

+	

 	void ExpectWeak (int n, int follow) {

 		if (la.kind == n) Get();

 		else {

@@ -209,7 +209,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		}

 	}

 

-

+	

 	void Dafny() {

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

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

@@ -449,6 +449,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		List<Formal/*!*/> formals = new List<Formal/*!*/>();

 		Type/*!*/ returnType;

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

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

 		List<FrameExpression/*!*/> reads = new List<FrameExpression/*!*/>();

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

 		Expression/*!*/ bb;  Expression body = null;

@@ -476,18 +477,18 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		Type(out returnType);

 		if (la.kind == 15) {

 			Get();

-			while (la.kind == 27 || la.kind == 29 || la.kind == 38) {

-				FunctionSpec(reqs, reads, decreases);

+			while (StartOf(3)) {

+				FunctionSpec(reqs, reads, ens, decreases);

 			}

-		} else if (StartOf(3)) {

-			while (la.kind == 27 || la.kind == 29 || la.kind == 38) {

-				FunctionSpec(reqs, reads, decreases);

+		} else if (StartOf(4)) {

+			while (StartOf(3)) {

+				FunctionSpec(reqs, reads, ens, decreases);

 			}

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

 			body = bb; 

 		} else SynErr(105);

 		parseVarScope.PopMarker();

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

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

 		f.BodyStartTok = bodyStart;

 		f.BodyEndTok = bodyEnd;

 		

@@ -532,11 +533,11 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		}

 		if (la.kind == 15) {

 			Get();

-			while (StartOf(4)) {

+			while (StartOf(5)) {

 				MethodSpec(req, mod, ens, dec);

 			}

-		} else if (StartOf(5)) {

-			while (StartOf(4)) {

+		} else if (StartOf(6)) {

+			while (StartOf(5)) {

 				MethodSpec(req, mod, ens, dec);

 			}

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

@@ -610,7 +611,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 	void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {

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

 		Expect(30);

-		if (StartOf(6)) {

+		if (StartOf(7)) {

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

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

 			while (la.kind == 17) {

@@ -642,7 +643,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			Expect(53);

 			Expression(out e1);

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

-		} else if (StartOf(7)) {

+		} else if (StartOf(8)) {

 			EquivExpression(out e);

 		} else SynErr(108);

 	}

@@ -759,7 +760,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		

 		if (la.kind == 25) {

 			Get();

-			if (StartOf(8)) {

+			if (StartOf(9)) {

 				FrameExpression(out fe);

 				mod.Add(fe); 

 				while (la.kind == 17) {

@@ -799,7 +800,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		parseVarScope.PushMarker(); 

 		Expect(7);

 		bodyStart = t; 

-		while (StartOf(9)) {

+		while (StartOf(10)) {

 			Stmt(body);

 		}

 		Expect(8);

@@ -874,7 +875,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else SynErr(112);

 	}

 

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

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

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

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

 		if (la.kind == 27) {

@@ -884,7 +885,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			reqs.Add(e); 

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

 			Get();

-			if (StartOf(10)) {

+			if (StartOf(11)) {

 				PossiblyWildFrameExpression(out fe);

 				reads.Add(fe); 

 				while (la.kind == 17) {

@@ -894,6 +895,11 @@ List<Expression/*!*/>/*!*/ decreases) {
 				}

 			}

 			Expect(15);

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

+			Get();

+			Expression(out e);

+			Expect(15);

+			ens.Add(e); 

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

 			Get();

 			Expressions(decreases);

@@ -907,7 +913,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		bodyStart = t; 

 		if (la.kind == 41) {

 			MatchExpression(out e);

-		} else if (StartOf(8)) {

+		} else if (StartOf(9)) {

 			Expression(out e);

 		} else SynErr(114);

 		Expect(8);

@@ -919,7 +925,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (la.kind == 39) {

 			Get();

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

-		} else if (StartOf(8)) {

+		} else if (StartOf(9)) {

 			FrameExpression(out fe);

 		} else SynErr(115);

 	}

@@ -930,7 +936,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (la.kind == 39) {

 			Get();

 			e = new WildcardExpr(t); 

-		} else if (StartOf(8)) {

+		} else if (StartOf(9)) {

 			Expression(out e);

 		} else SynErr(116);

 	}

@@ -984,7 +990,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			BlockStmt(out s, out bodyStart, out bodyEnd);

 			ss.Add(s); 

 		}

-		if (StartOf(11)) {

+		if (StartOf(12)) {

 			OneStmt(out s);

 			ss.Add(s); 

 		} else if (la.kind == 11 || la.kind == 16) {

@@ -1342,7 +1348,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 				if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } 

 			}

 		}

-		if (StartOf(12)) {

+		if (StartOf(13)) {

 			AssignStmt(out s);

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

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

@@ -1384,7 +1390,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 				UserDefinedType tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);

 				

 			}

-		} else if (StartOf(8)) {

+		} else if (StartOf(9)) {

 			Expression(out e);

 			ee = new List<Expression>(); ee.Add(e); 

 		} else SynErr(121);

@@ -1440,7 +1446,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (la.kind == 39) {

 			Get();

 			e = null; 

-		} else if (StartOf(8)) {

+		} else if (StartOf(9)) {

 			Expression(out ee);

 			e = ee; 

 		} else SynErr(123);

@@ -1471,7 +1477,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		}

 		Expect(43);

 		parseVarScope.PushMarker(); 

-		while (StartOf(9)) {

+		while (StartOf(10)) {

 			Stmt(body);

 		}

 		parseVarScope.PopMarker(); 

@@ -1497,7 +1503,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (la.kind == 4) {

 			Get();

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

-		} else if (StartOf(8)) {

+		} else if (StartOf(9)) {

 			Expression(out e);

 			arg = new Attributes.Argument(e); 

 		} else SynErr(125);

@@ -1536,7 +1542,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 	void LogicalExpression(out Expression/*!*/ e0) {

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

 		RelationalExpression(out e0);

-		if (StartOf(13)) {

+		if (StartOf(14)) {

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

 				AndOp();

 				x = t; 

@@ -1574,7 +1580,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 	void RelationalExpression(out Expression/*!*/ e0) {

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

 		Term(out e0);

-		if (StartOf(14)) {

+		if (StartOf(15)) {

 			RelOp(out x, out op);

 			Term(out e1);

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

@@ -1707,9 +1713,9 @@ List<Expression/*!*/>/*!*/ decreases) {
 			x = t; 

 			UnaryExpression(out e);

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

-		} else if (StartOf(12)) {

+		} else if (StartOf(13)) {

 			SelectExpression(out e);

-		} else if (StartOf(15)) {

+		} else if (StartOf(16)) {

 			ConstAtomExpression(out e);

 		} else SynErr(132);

 	}

@@ -1770,7 +1776,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			elements = new List<Expression/*!*/>(); 

 			if (la.kind == 30) {

 				Get();

-				if (StartOf(8)) {

+				if (StartOf(9)) {

 					Expressions(elements);

 				}

 				Expect(31);

@@ -1798,7 +1804,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		case 7: {

 			Get();

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

-			if (StartOf(8)) {

+			if (StartOf(9)) {

 				Expressions(elements);

 			}

 			e = new SetDisplayExpr(x, elements); 

@@ -1808,7 +1814,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		case 49: {

 			Get();

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

-			if (StartOf(8)) {

+			if (StartOf(9)) {

 				Expressions(elements);

 			}

 			e = new SeqDisplayExpr(x, elements); 

@@ -1836,7 +1842,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (la.kind == 30) {

 			Get();

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

-			if (StartOf(8)) {

+			if (StartOf(9)) {

 				Expressions(args);

 			}

 			Expect(31);

@@ -1866,9 +1872,9 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new OldExpr(x, e); 

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

 			Get();

-			if (StartOf(16)) {

+			if (StartOf(17)) {

 				QuantifierGuts(out e);

-			} else if (StartOf(8)) {

+			} else if (StartOf(9)) {

 				Expression(out e);

 			} else SynErr(136);

 			Expect(31);

@@ -1887,7 +1893,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			if (la.kind == 30) {

 				Get();

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

-				if (StartOf(8)) {

+				if (StartOf(9)) {

 					Expressions(args);

 				}

 				Expect(31);

@@ -1897,13 +1903,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (la.kind == 49) {

 			Get();

 			x = t; 

-			if (StartOf(8)) {

+			if (StartOf(9)) {

 				Expression(out ee);

 				e0 = ee; 

 				if (la.kind == 94) {

 					Get();

 					anyDots = true; 

-					if (StartOf(8)) {

+					if (StartOf(9)) {

 						Expression(out ee);

 						e1 = ee; 

 					}

@@ -2012,7 +2018,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expect(7);

 		if (la.kind == 20) {

 			AttributeBody(ref attrs);

-		} else if (StartOf(8)) {

+		} else if (StartOf(9)) {

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

 			Expressions(es);

 			trigs = new Triggers(es, trigs); 

@@ -2036,7 +2042,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expect(20);

 		Expect(1);

 		aName = t.val; 

-		if (StartOf(17)) {

+		if (StartOf(18)) {

 			AttributeArg(out aArg);

 			aArgs.Add(aArg); 

 			while (la.kind == 17) {

@@ -2052,18 +2058,19 @@ List<Expression/*!*/>/*!*/ decreases) {
 

 	public void Parse() {

 		la = new Token();

-		la.val = "";

+		la.val = "";		

 		Get();

 		Dafny();

 

-		Expect(0);

+    Expect(0);

 	}

-

+	

 	static readonly 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, x},

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

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

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

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

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

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

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

@@ -2086,20 +2093,18 @@ List<Expression/*!*/>/*!*/ decreases) {
 public class Errors {

 	public int count = 0;                                    // number of errors detected

 	public System.IO.TextWriter/*!*/ errorStream = Console.Out;   // error messages go to this stream

-	public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text

-	public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text

-

+  public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text

+  public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text

+  

 	public void SynErr(string filename, int line, int col, int n) {

-		SynErr(filename, line, col, GetSyntaxErrorString(n));

-	}

-

-	public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {

-		Contract.Requires(msg != null);

+    SynErr(filename, line, col, GetSyntaxErrorString(n));

+  }

+	public virtual void SynErr(string filename, int line, int col, string msg) {

+	  Contract.Requires(msg != null);

 		errorStream.WriteLine(errMsgFormat, filename, line, col, msg);

 		count++;

-	}

-

-	string GetSyntaxErrorString(int n) {

+  }

+  string GetSyntaxErrorString(int n) {

 		string s;

 		switch (n) {

 			case 0: s = "EOF expected"; break;

@@ -2251,7 +2256,7 @@ public class Errors {
 

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

 		}

-		return s;

+    return s;

 	}

 

 	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {  // semantic errors

@@ -2259,9 +2264,8 @@ public class Errors {
 		Contract.Requires(msg != null);

 		SemErr(tok.filename, tok.line, tok.col, msg);

 	}

-

 	public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {

-		Contract.Requires(msg != null);

+	  Contract.Requires(msg != null);

 		errorStream.WriteLine(errMsgFormat, filename, line, col, msg);

 		count++;

 	}

diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index 012d402a..c9c2e7fc 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -234,6 +234,7 @@ namespace Microsoft.Dafny {
       int ind = indent + IndentAmount;

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

       PrintFrameSpecLine("reads", f.Reads, ind);

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

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

       if (f.Body != null) {

         Indent(indent);

@@ -668,7 +669,7 @@ namespace Microsoft.Dafny {
     {

       Contract.Requires( -1 <= indent);

     

-    Contract.Requires(expr != null);

+      Contract.Requires(expr != null);

       if (expr is LiteralExpr) {

         LiteralExpr e = (LiteralExpr)expr;

         if (e.Value == null) {

@@ -681,7 +682,7 @@ namespace Microsoft.Dafny {
       

       } else if (expr is ThisExpr) {

         wr.Write("this");

-        

+  

       } else if (expr is IdentifierExpr) {

         wr.Write(((IdentifierExpr)expr).Name);

       

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index c2d1480a..459be877 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -89,7 +89,7 @@ namespace Microsoft.Dafny {
           } else if (other == m) {

             Error(m, "module must not import itself: {0}", imp);

           } else {

-            Contract.Assert( other != null);  // follows from postcondition of TryGetValue

+            Contract.Assert(other != null);  // follows from postcondition of TryGetValue

             importGraph.AddEdge(m, other);

           }

         }

@@ -109,7 +109,7 @@ namespace Microsoft.Dafny {
       } else {

         // fill in module heights

         List<ModuleDecl> mm = importGraph.TopologicallySortedComponents();

-        Contract.Assert( mm.Count == prog.Modules.Count);  // follows from the fact that there are no cycles

+        Contract.Assert(mm.Count == prog.Modules.Count);  // follows from the fact that there are no cycles

         int h = 0;

         foreach (ModuleDecl m in mm) {

           m.Height = h;

@@ -274,8 +274,8 @@ namespace Microsoft.Dafny {
     void ResolveClassMemberTypes(ClassDecl/*!*/ cl)

     {

       Contract.Requires(cl != null);

-      Contract.Requires( currentClass == null);

-      Contract.Ensures(  currentClass == null);

+      Contract.Requires(currentClass == null);

+      Contract.Ensures(currentClass == null);

     

       currentClass = cl;

       foreach (MemberDecl member in cl.Members) {

@@ -302,7 +302,7 @@ namespace Microsoft.Dafny {
           if (currentClass is ClassRefinementDecl) {      

             ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;

             if (refined != null) {

-              Contract.Assert( classMembers.ContainsKey(refined));

+              Contract.Assert(classMembers.ContainsKey(refined));

               Dictionary<string,MemberDecl> members = classMembers[refined];

             

               // resolve abstracted fields in the refined class

@@ -592,8 +592,8 @@ namespace Microsoft.Dafny {
     /// </summary>

     void ResolveFunction(Function f){

       Contract.Requires(f != null);

-      Contract.Requires( currentFunction == null);

-      Contract.Ensures(  currentFunction == null);

+      Contract.Requires(currentFunction == null);

+      Contract.Ensures(currentFunction == null);

       scope.PushMarker();

       currentFunction = f;

       if (f.IsStatic) {

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

       foreach (Expression r in f.Req) {

         ResolveExpression(r, false, true);

-        Contract.Assert( r.Type != null);  // follows from postcondition of ResolveExpression

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

         }

@@ -612,13 +612,20 @@ namespace Microsoft.Dafny {
       foreach (FrameExpression fr in f.Reads) {

         ResolveFrameExpression(fr, "reads");

       }

+      foreach (Expression r in f.Ens) {

+        ResolveExpression(r, false, true);  // since this is a function, the postcondition is still a one-state predicate

+        Contract.Assert(r.Type != null);  // follows from postcondition of ResolveExpression

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

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

+        }

+      }

       foreach (Expression r in f.Decreases) {

         ResolveExpression(r, false, true);

         // any type is fine

       }

       if (f.Body != null) {

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

-        Contract.Assert( f.Body.Type != null);  // follows from postcondition of ResolveExpression

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

         }

@@ -632,7 +639,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(kind != null);

       ResolveExpression(fe.E, false, true);

       Type t = fe.E.Type;

-      Contract.Assert( t != null);  // follows from postcondition of ResolveExpression

+      Contract.Assert(t != null);  // follows from postcondition of ResolveExpression

       if (t is CollectionType) {

         t = ((CollectionType)t).Arg;

       }

@@ -651,7 +658,7 @@ namespace Microsoft.Dafny {
           } else if (!(member is Field)) {

             Error(fe.E, "member {0} in class {1} does not refer to a field", fe.FieldName, cce.NonNull(ctype).Name);

           } else {

-            Contract.Assert( ctype != null && ctype.ResolvedClass != null);  // follows from postcondition of ResolveMember

+            Contract.Assert(ctype != null && ctype.ResolvedClass != null);  // follows from postcondition of ResolveMember

             fe.Field = (Field)member;

           }

         }

@@ -700,7 +707,7 @@ namespace Microsoft.Dafny {
       // Start resolving specification...

       foreach (MaybeFreeExpression e in m.Req) {

         ResolveExpression(e.E, false, true);

-        Contract.Assert( e.E.Type != null);  // follows from postcondition of ResolveExpression

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

         }

@@ -723,7 +730,7 @@ namespace Microsoft.Dafny {
       // ... continue resolving specification

       foreach (MaybeFreeExpression e in m.Ens) {

         ResolveExpression(e.E, true, true);

-        Contract.Assert( e.E.Type != null);  // follows from postcondition of ResolveExpression

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

         }

@@ -845,7 +852,7 @@ namespace Microsoft.Dafny {
         UserDefinedType bb = (UserDefinedType)b;

         if (aa.ResolvedClass != null && aa.ResolvedClass == bb.ResolvedClass) {

           // these are both resolved class/datatype types

-          Contract.Assert( aa.TypeArgs.Count == bb.TypeArgs.Count);

+          Contract.Assert(aa.TypeArgs.Count == bb.TypeArgs.Count);

           bool successSoFar = true;

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

             if (!UnifyTypes(aa.TypeArgs[i], bb.TypeArgs[i])) {

@@ -855,7 +862,7 @@ namespace Microsoft.Dafny {
           return successSoFar;

         } else if (aa.ResolvedParam != null && aa.ResolvedParam == bb.ResolvedParam) {

           // these are both resolved type parameters

-          Contract.Assert( aa.TypeArgs.Count == 0 && bb.TypeArgs.Count == 0);

+          Contract.Assert(aa.TypeArgs.Count == 0 && bb.TypeArgs.Count == 0);

           return true;

         } else {

           // something is wrong; either aa or bb wasn't properly resolved, or they don't unify

@@ -1074,7 +1081,7 @@ namespace Microsoft.Dafny {
         }

         

       } else if (a is IndexableTypeProxy) {

-        Contract.Assert( b is IndexableTypeProxy);  // else we have unexpected restricted-proxy type

+        Contract.Assert(b is IndexableTypeProxy);  // else we have unexpected restricted-proxy type

         a.T = b;

         return UnifyTypes(((IndexableTypeProxy)a).Arg, ((IndexableTypeProxy)b).Arg);

         

@@ -1089,7 +1096,7 @@ namespace Microsoft.Dafny {
         UseStmt s = (UseStmt)stmt;

         s.IsGhost = true;

         ResolveExpression(s.Expr, true, true);

-        Contract.Assert( s.Expr.Type != null);  // follows from postcondition of ResolveExpression

+        Contract.Assert(s.Expr.Type != null);  // follows from postcondition of ResolveExpression

         Expression expr = s.Expr;

         while (true) {

           if (expr is OldExpr) {

@@ -1102,7 +1109,7 @@ namespace Microsoft.Dafny {
         PredicateStmt s = (PredicateStmt)stmt;

         s.IsGhost = true;

         ResolveExpression(s.Expr, true, true);

-        Contract.Assert( s.Expr.Type != null);  // follows from postcondition of ResolveExpression

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

         }

@@ -1134,7 +1141,7 @@ namespace Microsoft.Dafny {
           ResolveExpression(s.Lhs, true, true);  // allow ghosts for now, but see FieldSelectExpr LHS case below

         }

         bool lhsResolvedSuccessfully = ErrorCount == prevErrorCount;

-        Contract.Assert( s.Lhs.Type != null);  // follows from postcondition of ResolveExpression

+        Contract.Assert(s.Lhs.Type != null);  // follows from postcondition of ResolveExpression

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

         bool lvalueIsGhost = false;

         if (s.Lhs is IdentifierExpr) {

@@ -1175,7 +1182,7 @@ namespace Microsoft.Dafny {
           SeqSelectExpr lhs = (SeqSelectExpr)s.Lhs;

           // LHS is fine, provided the "sequence" is really an array

           if (lhsResolvedSuccessfully) {

-            Contract.Assert( lhs.Seq.Type != null);

+            Contract.Assert(lhs.Seq.Type != null);

             Type elementType = new InferredTypeProxy();

             if (!UnifyTypes(lhs.Seq.Type, builtIns.ArrayType(1, elementType))) {

               Error(lhs.Seq, "LHS of array assignment must denote an array element (found {0})", lhs.Seq.Type);

@@ -1236,7 +1243,7 @@ namespace Microsoft.Dafny {
           if (s.Rhs is ExprRhs) {

             ExprRhs rr = (ExprRhs)s.Rhs;

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

-            Contract.Assert( rr.Expr.Type != null);  // follows from postcondition of ResolveExpression

+            Contract.Assert(rr.Expr.Type != null);  // follows from postcondition of ResolveExpression

             rhsType = rr.Expr.Type;

           } else if (s.Rhs is TypeRhs) {

             TypeRhs rr = (TypeRhs)s.Rhs;

@@ -1260,7 +1267,7 @@ namespace Microsoft.Dafny {
 

         // resolve receiver

         ResolveReceiver(s.Receiver, true, false);

-        Contract.Assert( s.Receiver.Type != null);  // follows from postcondition of ResolveExpression

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

@@ -1312,7 +1319,7 @@ namespace Microsoft.Dafny {
         } else if (callee.Outs.Count != s.Lhs.Count) {

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

         } else {

-          Contract.Assert( ctype != null);  // follows from postcondition of ResolveMember above

+          Contract.Assert(ctype != null);  // follows from postcondition of ResolveMember above

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

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

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

@@ -1372,7 +1379,7 @@ namespace Microsoft.Dafny {
         if (s.Guard != null) {

           int prevErrorCount = ErrorCount;

           ResolveExpression(s.Guard, true, true);

-          Contract.Assert( s.Guard.Type != null);  // follows from postcondition of ResolveExpression

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

@@ -1393,7 +1400,7 @@ namespace Microsoft.Dafny {
         if (s.Guard != null) {

           int prevErrorCount = ErrorCount;

           ResolveExpression(s.Guard, true, true);

-          Contract.Assert( s.Guard.Type != null);  // follows from postcondition of ResolveExpression

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

@@ -1404,7 +1411,7 @@ namespace Microsoft.Dafny {
         }

         foreach (MaybeFreeExpression inv in s.Invariants) {

           ResolveExpression(inv.E, true, true);

-          Contract.Assert( inv.E.Type != null);  // follows from postcondition of ResolveExpression

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

           }

@@ -1420,19 +1427,19 @@ namespace Microsoft.Dafny {
         ForeachStmt s = (ForeachStmt)stmt;

 

         ResolveExpression(s.Collection, true, true);

-        Contract.Assert( s.Collection.Type != null);  // follows from postcondition of ResolveExpression

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

         }

         

         scope.PushMarker();

         bool b = scope.Push(s.BoundVar.Name, s.BoundVar);

-        Contract.Assert( b);  // since we just pushed a marker, we expect the Push to succeed

+        Contract.Assert(b);  // since we just pushed a marker, we expect the Push to succeed

         ResolveType(s.BoundVar.Type);

         int prevErrorCount = ErrorCount;

         

         ResolveExpression(s.Range, true, true);

-        Contract.Assert( s.Range.Type != null);  // follows from postcondition of ResolveExpression

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

         }

@@ -1462,7 +1469,7 @@ namespace Microsoft.Dafny {
         bool bodyIsSpecOnly = specContextOnly;

         int prevErrorCount = ErrorCount;

         ResolveExpression(s.Source, true, true);

-        Contract.Assert( s.Source.Type != null);  // follows from postcondition of ResolveExpression

+        Contract.Assert(s.Source.Type != null);  // follows from postcondition of ResolveExpression

         bool successfullyResolved = ErrorCount == prevErrorCount;

         if (!specContextOnly && successfullyResolved) {

           bodyIsSpecOnly = UsesSpecFeatures(s.Source);

@@ -1479,9 +1486,9 @@ namespace Microsoft.Dafny {
           Error(s.Source, "the type of the match source expression must be a datatype");

           ctors = null;

         } else {

-          Contract.Assert( sourceType != null);  // dtd and sourceType are set together above

+          Contract.Assert(sourceType != null);  // dtd and sourceType are set together above

           ctors = datatypeCtors[dtd];

-          Contract.Assert( ctors != null);  // dtd should have been inserted into datatypeCtors during a previous resolution stage

+          Contract.Assert(ctors != null);  // dtd should have been inserted into datatypeCtors during a previous resolution stage

           

           // build the type-parameter substitution map for this use of the datatype

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

@@ -1494,11 +1501,11 @@ namespace Microsoft.Dafny {
         foreach (MatchCaseStmt mc in s.Cases) {

           DatatypeCtor ctor = null;

           if (ctors != null) {

-            Contract.Assert( dtd != null);

+            Contract.Assert(dtd != null);

             if (!ctors.TryGetValue(mc.Id, out ctor)) {

               Error(mc.tok, "member {0} does not exist in datatype {1}", mc.Id, dtd.Name);

             } else {

-              Contract.Assert( ctor != null);  // follows from postcondition of TryGetValue

+              Contract.Assert(ctor != null);  // follows from postcondition of TryGetValue

               mc.Ctor = ctor;

               if (ctor.Formals.Count != mc.Arguments.Count) {

                 Error(mc.tok, "member {0} has wrong number of formals (found {1}, expected {2})", mc.Arguments.Count, ctor.Formals.Count);

@@ -1558,7 +1565,7 @@ namespace Microsoft.Dafny {
           LabelStmt ls = (LabelStmt)ss;

           labeledStatements.PushMarker();

           bool b = labeledStatements.Push(ls.Label, ls);

-          Contract.Assert( b);  // since we just pushed a marker, we expect the Push to succeed

+          Contract.Assert(b);  // since we just pushed a marker, we expect the Push to succeed

           labelsToPop++;

         } else {

           ResolveStatement(ss, specContextOnly, method);

@@ -1604,8 +1611,8 @@ namespace Microsoft.Dafny {
       if (ctype == null) {

         Error(tok, "receiver (of type {0}) must be of a class type", receiverType);

       } else {

-        Contract.Assert( ctype.ResolvedClass is ClassDecl);  // follows from postcondition of DenotesClass

-        Contract.Assert( ctype.TypeArgs.Count == ctype.ResolvedClass.TypeArgs.Count);  // follows from the fact that ctype was resolved

+        Contract.Assert(ctype.ResolvedClass is ClassDecl);  // follows from postcondition of DenotesClass

+        Contract.Assert(ctype.TypeArgs.Count == ctype.ResolvedClass.TypeArgs.Count);  // follows from the fact that ctype was resolved

         MemberDecl member;

         if (!classMembers[(ClassDecl)ctype.ResolvedClass].TryGetValue(memberName, out member)) {

           Error(tok, "member {0} does not exist in class {1}", memberName, ctype.Name);

@@ -1639,7 +1646,7 @@ namespace Microsoft.Dafny {
       } else if (type is UserDefinedType) {

         UserDefinedType t = (UserDefinedType)type;

         if (t.ResolvedParam != null) {

-          Contract.Assert( t.TypeArgs.Count == 0);

+          Contract.Assert(t.TypeArgs.Count == 0);

           Type s;

           if (subst.TryGetValue(t.ResolvedParam, out s)) {

             return cce.NonNull(s);

@@ -1702,9 +1709,9 @@ namespace Microsoft.Dafny {
     /// "twoState" implies that "old" and "fresh" expressions are allowed

     /// </summary>

     void ResolveExpression(Expression expr, bool twoState, bool specContext){

-     Contract.Requires(expr != null);

-      Contract.Requires( currentClass != null);

-      Contract.Ensures(  expr.Type != null);

+      Contract.Requires(expr != null);

+      Contract.Requires(currentClass != null);

+      Contract.Ensures(expr.Type != null);

       if (expr.Type != null) {

         // expression has already been resovled

         return;

@@ -1770,7 +1777,7 @@ namespace Microsoft.Dafny {
           if (!datatypeCtors[dt].TryGetValue(dtv.MemberName, out ctor)) {

             Error(expr.tok, "undeclared constructor {0} in datatype {1}", dtv.MemberName, dtv.DatatypeName);

           } else {

-            Contract.Assert( ctor != null);  // follows from postcondition of TryGetValue

+            Contract.Assert(ctor != null);  // follows from postcondition of TryGetValue

             dtv.Ctor = ctor;

             if (ctor.Formals.Count != dtv.Arguments.Count) {

               Error(expr.tok, "wrong number of arguments to datatype constructor {0} (found {1}, expected {2})", dtv.DatatypeName, dtv.Arguments.Count, ctor.Formals.Count);

@@ -1786,7 +1793,7 @@ namespace Microsoft.Dafny {
           foreach (Expression arg in dtv.Arguments) {

             Formal formal = ctor != null && j < ctor.Formals.Count ? ctor.Formals[j] : null;

             ResolveExpression(arg, twoState, specContext || (formal != null && formal.IsGhost));

-            Contract.Assert( arg.Type != null);  // follows from postcondition of ResolveExpression

+            Contract.Assert(arg.Type != null);  // follows from postcondition of ResolveExpression

             if (formal != null) {

               Type st = SubstType(formal.Type, subst);

               if (!UnifyTypes(arg.Type, st)) {

@@ -1802,7 +1809,7 @@ namespace Microsoft.Dafny {
         Type elementType = new InferredTypeProxy();

         foreach (Expression ee in e.Elements) {

           ResolveExpression(ee, twoState, specContext);

-          Contract.Assert( ee.Type != null);  // follows from postcondition of ResolveExpression

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

           }

@@ -1816,7 +1823,7 @@ namespace Microsoft.Dafny {
       } else if (expr is FieldSelectExpr) {

         FieldSelectExpr e = (FieldSelectExpr)expr;

         ResolveExpression(e.Obj, twoState, specContext);

-        Contract.Assert( e.Obj.Type != null);  // follows from postcondition of ResolveExpression

+        Contract.Assert(e.Obj.Type != null);  // follows from postcondition of ResolveExpression

         UserDefinedType ctype;

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

         if (member == null) {

@@ -1824,7 +1831,7 @@ namespace Microsoft.Dafny {
         } else if (!(member is Field)) {

           Error(expr, "member {0} in class {1} does not refer to a field", e.FieldName, cce.NonNull(ctype).Name);

         } else {

-          Contract.Assert( ctype != null && ctype.ResolvedClass != null);  // follows from postcondition of ResolveMember

+          Contract.Assert(ctype != null && ctype.ResolvedClass != null);  // follows from postcondition of ResolveMember

           e.Field = (Field)member;

           // build the type substitution map

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

@@ -1873,12 +1880,12 @@ namespace Microsoft.Dafny {
           seqErr = true;

         }

         ResolveExpression(e.Index, twoState, specContext);

-        Contract.Assert( e.Index.Type != null);  // follows from postcondition of ResolveExpression

+        Contract.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, specContext);

-        Contract.Assert( e.Value.Type != null);  // follows from postcondition of ResolveExpression

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

         }

@@ -1889,7 +1896,7 @@ namespace Microsoft.Dafny {
       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

         ResolveReceiver(e.Receiver, twoState, specContext);

-        Contract.Assert( e.Receiver.Type != null);  // follows from postcondition of ResolveExpression

+        Contract.Assert(e.Receiver.Type != null);  // follows from postcondition of ResolveExpression

         UserDefinedType ctype;

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

         if (member == null) {

@@ -1905,7 +1912,7 @@ namespace Microsoft.Dafny {
           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 {

-            Contract.Assert( ctype != null);  // follows from postcondition of ResolveMember

+            Contract.Assert(ctype != null);  // follows from postcondition of ResolveMember

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

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

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

@@ -1928,7 +1935,7 @@ namespace Microsoft.Dafny {
             for (int i = 0; i < function.Formals.Count; i++) {

               Expression farg = e.Args[i];

               ResolveExpression(farg, twoState, specContext);

-              Contract.Assert( farg.Type != null);  // follows from postcondition of ResolveExpression

+              Contract.Assert(farg.Type != null);  // follows from postcondition of ResolveExpression

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

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

                 Error(expr, "incorrect type of function argument {0} (expected {1}, got {2})", i, s, farg.Type);

@@ -1973,7 +1980,7 @@ namespace Microsoft.Dafny {
         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;

-        Contract.Assert( t != null);  // follows from postcondition of ResolveExpression

+        Contract.Assert(t != null);  // follows from postcondition of ResolveExpression

         if (t is CollectionType) {

           t = ((CollectionType)t).Arg;

         }

@@ -1989,7 +1996,7 @@ namespace Microsoft.Dafny {
       } else if (expr is UnaryExpr) {

         UnaryExpr e = (UnaryExpr)expr;

         ResolveExpression(e.E, twoState, specContext);

-        Contract.Assert( e.E.Type != null);  // follows from postcondition of ResolveExpression

+        Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression

         switch (e.Op) {

           case UnaryExpr.Opcode.Not:

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

@@ -2010,9 +2017,9 @@ namespace Microsoft.Dafny {
       } else if (expr is BinaryExpr) {

         BinaryExpr e = (BinaryExpr)expr;

         ResolveExpression(e.E0, twoState, specContext);

-        Contract.Assert( e.E0.Type != null);  // follows from postcondition of ResolveExpression

+        Contract.Assert(e.E0.Type != null);  // follows from postcondition of ResolveExpression

         ResolveExpression(e.E1, twoState, specContext);

-        Contract.Assert( e.E1.Type != null);  // follows from postcondition of ResolveExpression

+        Contract.Assert(e.E1.Type != null);  // follows from postcondition of ResolveExpression

         switch (e.Op) {

           case BinaryExpr.Opcode.Iff:

           case BinaryExpr.Opcode.Imp:

@@ -2145,7 +2152,7 @@ namespace Microsoft.Dafny {
           ResolveType(v.Type);

         }

         ResolveExpression(e.Body, twoState, specContext);

-        Contract.Assert( e.Body.Type != null);  // follows from postcondition of ResolveExpression

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

         }

@@ -2162,11 +2169,11 @@ namespace Microsoft.Dafny {
       } else if (expr is ITEExpr) {

         ITEExpr e = (ITEExpr)expr;

         ResolveExpression(e.Test, twoState, specContext);

-        Contract.Assert( e.Test.Type != null);  // follows from postcondition of ResolveExpression

+        Contract.Assert(e.Test.Type != null);  // follows from postcondition of ResolveExpression

         ResolveExpression(e.Thn, twoState, specContext);

-        Contract.Assert( e.Thn.Type != null);  // follows from postcondition of ResolveExpression

+        Contract.Assert(e.Thn.Type != null);  // follows from postcondition of ResolveExpression

         ResolveExpression(e.Els, twoState, specContext);

-        Contract.Assert( e.Els.Type != null);  // follows from postcondition of ResolveExpression

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

         }

@@ -2178,9 +2185,9 @@ namespace Microsoft.Dafny {
       

       } else if (expr is MatchExpr) {

         MatchExpr me = (MatchExpr)expr;

-        Contract.Assert( !twoState);  // currently, match expressions are allowed only at the outermost level of function bodies

+        Contract.Assert(!twoState);  // currently, match expressions are allowed only at the outermost level of function bodies

         ResolveExpression(me.Source, twoState, specContext);

-        Contract.Assert( me.Source.Type != null);  // follows from postcondition of ResolveExpression

+        Contract.Assert(me.Source.Type != null);  // follows from postcondition of ResolveExpression

         UserDefinedType sourceType = null;

         DatatypeDecl dtd = null;

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

@@ -2193,9 +2200,9 @@ namespace Microsoft.Dafny {
           Error(me.Source, "the type of the match source expression must be a datatype");

           ctors = null;

         } else {

-          Contract.Assert( sourceType != null);  // dtd and sourceType are set together above

+          Contract.Assert(sourceType != null);  // dtd and sourceType are set together above

           ctors = datatypeCtors[dtd];

-          Contract.Assert( ctors != null);  // dtd should have been inserted into datatypeCtors during a previous resolution stage

+          Contract.Assert(ctors != null);  // dtd should have been inserted into datatypeCtors during a previous resolution stage

           

           IdentifierExpr ie = me.Source as IdentifierExpr;

           if (ie == null || !(ie.Var is Formal)) {

@@ -2213,11 +2220,11 @@ namespace Microsoft.Dafny {
         foreach (MatchCaseExpr mc in me.Cases) {

           DatatypeCtor ctor = null;

           if (ctors != null) {

-            Contract.Assert( dtd != null);

+            Contract.Assert(dtd != null);

             if (!ctors.TryGetValue(mc.Id, out ctor)) {

               Error(mc.tok, "member {0} does not exist in datatype {1}", mc.Id, dtd.Name);

             } else {

-              Contract.Assert( ctor != null);  // follows from postcondition of TryGetValue

+              Contract.Assert(ctor != null);  // follows from postcondition of TryGetValue

               mc.Ctor = ctor;

               if (ctor.Formals.Count != mc.Arguments.Count) {

                 Error(mc.tok, "member {0} has wrong number of formals (found {1}, expected {2})", mc.Id, mc.Arguments.Count, ctor.Formals.Count);

@@ -2253,7 +2260,7 @@ namespace Microsoft.Dafny {
             i++;

           }

           ResolveExpression(mc.Body, twoState, specContext);

-          Contract.Assert( mc.Body.Type != null);  // follows from postcondition of ResolveExpression

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

           }

@@ -2292,7 +2299,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(e != null);

       bool seqErr = false;

       ResolveExpression(e.Seq, twoState, specContext);

-      Contract.Assert( e.Seq.Type != null);  // follows from postcondition of ResolveExpression

+      Contract.Assert(e.Seq.Type != null);  // follows from postcondition of ResolveExpression

       Type elementType = new InferredTypeProxy();

       Type expectedType;

       if (e.SelectOne || allowNonUnitArraySelection) {

@@ -2306,14 +2313,14 @@ namespace Microsoft.Dafny {
       }

       if (e.E0 != null) {

         ResolveExpression(e.E0, twoState, specContext);

-        Contract.Assert( e.E0.Type != null);  // follows from postcondition of ResolveExpression

+        Contract.Assert(e.E0.Type != null);  // follows from postcondition of ResolveExpression

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

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

         }

       }

       if (e.E1 != null) {

         ResolveExpression(e.E1, twoState, specContext);

-        Contract.Assert( e.E1.Type != null);  // follows from postcondition of ResolveExpression

+        Contract.Assert(e.E1.Type != null);  // follows from postcondition of ResolveExpression

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

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

         }

@@ -2567,7 +2574,7 @@ namespace Microsoft.Dafny {
           }

         } else if (names[n] == name) {

           Thing t = things[n];

-          Contract.Assert( t != null);

+          Contract.Assert(t != null);

           return t;

         }

       }

diff --git a/Dafny/Scanner.cs b/Dafny/Scanner.cs
index 42c4f661..de87c6ad 100644
--- a/Dafny/Scanner.cs
+++ b/Dafny/Scanner.cs
@@ -19,7 +19,7 @@ public class Buffer {
 	//    a) whole stream in buffer

 	//    b) part of stream in buffer

 	// 2) non seekable stream (network, console)

-

+  

 	public const int EOF = 65535 + 1; // char.MaxValue + 1;

 	const int MIN_BUFFER_LENGTH = 1024; // 1KB

 	const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB

@@ -31,17 +31,15 @@ public class Buffer {
 	Stream/*!*/ stream;      // input stream (seekable)

 	bool isUserStream;  // was the stream opened by the user?

 

-	[ContractInvariantMethod]

-	void ObjectInvariant(){

-		Contract.Invariant(buf != null);

-		Contract.Invariant(stream != null);

-	}

-

-//  [NotDelayed]

-	public Buffer (Stream/*!*/ s, bool isUserStream) : base() {

+[ContractInvariantMethod]

+void ObjectInvariant(){

+  Contract.Invariant(buf != null);

+  Contract.Invariant(stream != null);}

+    [NotDelayed]

+	public Buffer (Stream/*!*/ s, bool isUserStream) :base() {

 	  Contract.Requires(s != null);

 		stream = s; this.isUserStream = isUserStream;

-

+		

 		int fl, bl;

 		if (s.CanSeek) {

 			fl = (int) s.Length;

@@ -53,12 +51,12 @@ public class Buffer {
 

 		buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];

 		fileLen = fl;  bufLen = bl;

-

+		

 		if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start)

 		else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid

 		if (bufLen == fileLen && s.CanSeek) Close();

 	}

-

+	

 	protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor

 	  Contract.Requires(b != null);

 		buf = b.buf;

@@ -75,14 +73,14 @@ public class Buffer {
 	}

 

 	~Buffer() { Close(); }

-

+	

 	protected void Close() {

 		if (!isUserStream && stream != null) {

 			stream.Close();

 			//stream = null;

 		}

 	}

-

+	

 	public virtual int Read () {

 		if (bufPos < bufLen) {

 			return buf[bufPos++];

@@ -102,7 +100,7 @@ public class Buffer {
 		Pos = curPos;

 		return ch;

 	}

-

+	

 	public string/*!*/ GetString (int beg, int end) {

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

 		int len = 0;

@@ -141,7 +139,7 @@ public class Buffer {
 			}

 		}

 	}

-

+	

 	// Read the next chunk of bytes from the stream, increases the buffer

 	// if needed and updates the fields fileLen and bufLen.

 	// Returns the number of bytes read.

@@ -215,20 +213,19 @@ public class Scanner {
 	const int noSym = 103;

 

 

-	[ContractInvariantMethod]

-	void objectInvariant(){

-		Contract.Invariant(buffer!=null);

-		Contract.Invariant(t != null);

-		Contract.Invariant(start != null);

-		Contract.Invariant(tokens != null);

-		Contract.Invariant(pt != null);

-		Contract.Invariant(tval != null);

-		Contract.Invariant(Filename != null);

-		Contract.Invariant(errorHandler != null);

-	}

-

+[ContractInvariantMethod]

+void objectInvariant(){

+  Contract.Invariant(buffer!=null);

+  Contract.Invariant(t != null);

+  Contract.Invariant(start != null);

+  Contract.Invariant(tokens != null);

+  Contract.Invariant(pt != null);

+  Contract.Invariant(tval != null);

+  Contract.Invariant(Filename != null);

+  Contract.Invariant(errorHandler != null);

+}

 	public Buffer/*!*/ buffer; // scanner buffer

-

+	

 	Token/*!*/ t;          // current token

 	int ch;           // current input character

 	int pos;          // byte position of current character

@@ -239,13 +236,13 @@ public class Scanner {
 

 	Token/*!*/ tokens;     // list of tokens already peeked (first token is a dummy)

 	Token/*!*/ pt;         // current peek token

-

+	

 	char[]/*!*/ tval = new char[128]; // text of current token

 	int tlen;         // length of current token

-

+	

 	private string/*!*/ Filename;

 	private Errors/*!*/ errorHandler;

-

+	

 	static Scanner() {

 		start = new Hashtable(128);

 		for (int i = 39; i <= 39; ++i) start[i] = 1;

@@ -294,9 +291,9 @@ public class Scanner {
 		start[Buffer.EOF] = -1;

 

 	}

-

-//	[NotDelayed]

-	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() {

+	

+	[NotDelayed]

+	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){

 	  Contract.Requires(fileName != null);

 	  Contract.Requires(errorHandler != null);

 		this.errorHandler = errorHandler;

@@ -306,14 +303,15 @@ public class Scanner {
 			Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);

 			buffer = new Buffer(stream, false);

 			Filename = fileName;

+			

 			Init();

 		} catch (IOException) {

 			throw new FatalError("Cannot open file " + fileName);

 		}

 	}

-

-//	[NotDelayed]

-	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() {

+	

+	[NotDelayed]

+	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){

 	  Contract.Requires(s != null);

 	  Contract.Requires(errorHandler != null);

 	  Contract.Requires(fileName != null);

@@ -322,9 +320,10 @@ public class Scanner {
 		buffer = new Buffer(s, true);

 		this.errorHandler = errorHandler;

 		this.Filename = fileName;

+		

 		Init();

 	}

-

+	

 	void Init() {

 		pos = -1; line = 1; col = 0;

 		oldEols = 0;

@@ -345,11 +344,11 @@ public class Scanner {
 	Contract.Ensures(Contract.Result<string>() != null);

 	  int p = buffer.Pos;

 	  int ch = buffer.Read();

-	  // replace isolated '\r' by '\n' in order to make

+      // replace isolated '\r' by '\n' in order to make

 	  // eol handling uniform across Windows, Unix and Mac

 	  if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

 	  while (ch != EOL && ch != Buffer.EOF){

-		ch = buffer.Read();

+	    ch = buffer.Read();

 		// replace isolated '\r' by '\n' in order to make

 		// eol handling uniform across Windows, Unix and Mac

 		if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

@@ -360,7 +359,7 @@ public class Scanner {
 	}

 

 	void NextCh() {

-		if (oldEols > 0) { ch = EOL; oldEols--; }

+		if (oldEols > 0) { ch = EOL; oldEols--; } 

 		else {

 //			pos = buffer.Pos;

 //			ch = buffer.Read(); col++;

@@ -368,9 +367,9 @@ public class Scanner {
 //			// eol handling uniform across Windows, Unix and Mac

 //			if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

 //			if (ch == EOL) { line++; col = 0; }

-

+			

 			while (true) {

-				pos = buffer.Pos;

+			    pos = buffer.Pos;

 				ch = buffer.Read(); col++;

 				// replace isolated '\r' by '\n' in order to make

 				// eol handling uniform across Windows, Unix and Mac

@@ -420,7 +419,7 @@ public class Scanner {
 				return;

 			  }

 

-

+			

 		}

 

 	}

@@ -556,13 +555,10 @@ public class Scanner {
 		t.pos = pos; t.col = col; t.line = line;

 		t.filename = this.Filename;

 		int state;

-		if (start.ContainsKey(ch)) {

-			Contract.Assert(start[ch] != null);

-			state = (int) start[ch];

-		}

+		if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }

 		else { state = 0; }

 		tlen = 0; AddCh();

-

+		

 		switch (state) {

 			case -1: { t.kind = eofSym; break; } // NextCh already done

 			case 0: {

@@ -769,14 +765,14 @@ public class Scanner {
 		t.val = new String(tval, 0, tlen);

 		return t;

 	}

-

+	

 	private void SetScannerBehindT() {

 		buffer.Pos = t.pos;

 		NextCh();

 		line = t.line; col = t.col;

 		for (int i = 0; i < tlen; i++) NextCh();

 	}

-

+	

 	// get the next token (possibly a token already seen during peeking)

 	public Token/*!*/ Scan () {

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

@@ -797,7 +793,7 @@ public class Scanner {
 			}

 			pt = pt.next;

 		} while (pt.kind > maxT); // skip pragmas

-

+	

 		return pt;

 	}

 

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 6c21ecd0..609e555d 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -514,17 +514,21 @@ namespace Microsoft.Dafny {
         } else if (member is Function) {

           Function f = (Function)member;

           AddFunction(f);

-          if (f.Body != null) {

+          if (f.Body != null || f.Ens.Count != 0) {

             if (f.Body is MatchExpr) {

               MatchExpr me = (MatchExpr)f.Body;

               Formal formal = (Formal)((IdentifierExpr)me.Source).Var;  // correctness of casts follows from what resolution checks

               foreach (MatchCaseExpr mc in me.Cases) {

                 Contract.Assert( mc.Ctor != null);  // the field is filled in by resolution

-                Bpl.Axiom ax = FunctionAxiom(f, mc.Body, formal, mc.Ctor, mc.Arguments);

+                Bpl.Axiom ax = FunctionAxiom(f, mc.Body, new List<Expression>(), formal, mc.Ctor, mc.Arguments);

+                sink.TopLevelDeclarations.Add(ax);

+              }

+              if (f.Ens.Count != 0) {

+                Bpl.Axiom ax = FunctionAxiom(f, null, f.Ens, null, null, null);

                 sink.TopLevelDeclarations.Add(ax);

               }

             } else {

-              Bpl.Axiom ax = FunctionAxiom(f, f.Body, null, null, null);

+              Bpl.Axiom ax = FunctionAxiom(f, f.Body, f.Ens, null, null, null);

               sink.TopLevelDeclarations.Add(ax);

             }

             if (f.IsRecursive && !f.IsUnlimited) {

@@ -561,31 +565,34 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

-    Bpl.Axiom/*!*/ FunctionAxiom(Function/*!*/ f, Expression/*!*/ body, Formal specializationFormal,

-                             DatatypeCtor ctor, List<BoundVar/*!*/> specializationReplacementFormals){

+

+    Bpl.Axiom/*!*/ FunctionAxiom(Function/*!*/ f, Expression body, List<Expression/*!*/>/*!*/ ens,

+                                 Formal specializationFormal,

+                                 DatatypeCtor ctor, List<BoundVar/*!*/> specializationReplacementFormals){

       Contract.Requires(f != null);

-      Contract.Requires(body != null);

+      Contract.Requires(specializationFormal == null || body != null);

+      Contract.Requires(ens != null);

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

-     Contract.Requires( predef != null);

-     Contract.Requires( specializationFormal == null && ctor == null);

-     Contract.Requires( specializationFormal == null && specializationReplacementFormals == null);

-     Contract.Requires( f.EnclosingClass != null);

-    

+      Contract.Requires(predef != null);

+      Contract.Requires((specializationFormal == null) == (ctor == null));

+      Contract.Requires((specializationFormal == null) == (specializationReplacementFormals == null));

+      Contract.Requires(f.EnclosingClass != null);

+ 

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);

       

       // axiom

       //   mh < ModuleContextHeight || (mh == ModuleContextHeight && (fh < FunctionContextHeight || InMethodContext))

       //   ==>

-      //   (forall $Heap, formals :: this != null && $IsHeap($Heap) && Pre($Heap,args) ==> f(args) == body);

+      //   (forall $Heap, formals :: this != null && $IsHeap($Heap) && Pre($Heap,args) ==>

+      //       f(args) == body && ens);

       //

       // The variables "formals" are the formals of function "f"; except, if a specialization is provided, then

       // "specializationFormal" (which is expected to be among the formals of "f") is excluded and replaced by

       // "specializationReplacementFormals".

       // The list "args" is the list of formals of function "f"; except, if a specialization is provided, then

       // "specializationFormal" is replaced by the expression "ctor(specializationReplacementFormals)".

-      // If a specialization is provided, occurrences of "specializationFormal" in "body" are also replaced by

-      // that expression.

+      // If a specialization is provided, occurrences of "specializationFormal" in "body", "f.Req", and "f.Ens"

+      // are also replaced by that expression.

       //

       // The translation of "body" uses the #limited form whenever the callee is in the same SCC of the call graph.

       //

@@ -612,7 +619,7 @@ namespace Microsoft.Dafny {
       }

       DatatypeValue r = null;

       if (specializationReplacementFormals != null) {

-        Contract.Assert( ctor != null);  // follows from if guard and the precondition

+        Contract.Assert(ctor != null);  // follows from if guard and the precondition

         List<Expression> rArgs = new List<Expression>();

         foreach (BoundVar p in specializationReplacementFormals) {

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

@@ -630,7 +637,7 @@ namespace Microsoft.Dafny {
           formals.Add(bv);

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

         } else {

-          Contract.Assert( r != null);  // it is set above

+          Contract.Assert(r != null);  // it is set above

           args.Add(etran.TrExpr(r));

         }

       }

@@ -647,30 +654,44 @@ namespace Microsoft.Dafny {
       

       Bpl.Expr ante = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr);

       if (!f.IsStatic) {

-        Contract.Assert( bvThisIdExpr != null);  // set to non-null value above when !f.IsStatic

+        Contract.Assert(bvThisIdExpr != null);  // set to non-null value above when !f.IsStatic

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

       }

-      foreach (Expression req in f.Req) {

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

+

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

+      if (specializationFormal != null) {

+        Contract.Assert(r != null);

+        substMap.Add(specializationFormal, r);

       }

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

+

+      foreach (Expression req in f.Req) {

+        ante = Bpl.Expr.And(ante, etran.TrExpr(Substitute(req, null, substMap)));

+      }

       Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(funcAppl));

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

-      if (specializationFormal != null) {

-        Contract.Assert( r != null);

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

-        substMap.Add(specializationFormal, r);

-        body = Substitute(body, null, substMap);

+      Bpl.Expr meat = null;

+      if (body != null) {

+        meat = Bpl.Expr.Eq(funcAppl, etran.LimitedFunctions(f).TrExpr(Substitute(body, null, substMap)));

+      }

+      foreach (Expression p in ens) {

+        Bpl.Expr q = etran.LimitedFunctions(f).TrExpr(Substitute(p, null, substMap));

+        if (meat == null) {

+          meat = q;

+        } else {

+          meat = Bpl.Expr.And(meat, q);

+        }

       }

-      Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Imp(ante, Bpl.Expr.Eq(funcAppl, etran.LimitedFunctions(f).TrExpr(body))));

+      Contract.Assert(meat != null);

+      Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Imp(ante, meat));

       return new Bpl.Axiom(f.tok, Bpl.Expr.Imp(activate, ax));

     }

     

     void AddLimitedAxioms(Function f){

       Contract.Requires(f != null);

-     Contract.Requires( f.IsRecursive && !f.IsUnlimited);

-     Contract.Requires( sink != null && predef != null);

+      Contract.Requires(f.IsRecursive && !f.IsUnlimited);

+      Contract.Requires(sink != null && predef != null);

       // axiom (forall formals :: { f(args) } f(args) == f#limited(args))

 

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

@@ -869,12 +890,12 @@ namespace Microsoft.Dafny {
       Bpl.StmtList stmts;

       if (!wellformednessProc) {

         // translate the body of the method

-        Contract.Assert( m.Body != null);  // follows from method precondition and the if guard

+        Contract.Assert(m.Body != null);  // follows from method precondition and the if guard

         stmts = TrStmt2StmtList(builder, m.Body, localVariables, etran);

       } else {

         // check well-formedness of the preconditions, and then assume each one of them

         foreach (MaybeFreeExpression p in m.Req) {

-          CheckWellformed(p.E, null, Position.Positive, localVariables, builder, etran);

+          CheckWellformed(p.E, null, null, Position.Positive, localVariables, builder, etran);

           builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));

         }

         // Note: the modifies clauses are not checked for well-formedness (is that sound?), because it used to

@@ -882,7 +903,7 @@ namespace Microsoft.Dafny {
         // absolutely well-defined.

         // check well-formedness of the decreases clauses

         foreach (Expression p in m.Decreases) {

-          CheckWellformed(p, null, Position.Positive, localVariables, builder, etran);

+          CheckWellformed(p, null, null, Position.Positive, localVariables, builder, etran);

         }

 

         // play havoc with the heap according to the modifies clause

@@ -914,7 +935,7 @@ namespace Microsoft.Dafny {
 

         // check wellformedness of postconditions

         foreach (MaybeFreeExpression p in m.Ens) {

-          CheckWellformed(p.E, null, Position.Positive, localVariables, builder, etran);

+          CheckWellformed(p.E, null, null, Position.Positive, localVariables, builder, etran);

           builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));

         }

 

@@ -1210,9 +1231,9 @@ namespace Microsoft.Dafny {
     }

     

     void AddWellformednessCheck(Function f){

-    Contract.Requires(f != null);

-     Contract.Requires( sink != null && predef != null);

-     Contract.Requires( f.EnclosingClass != null);

+      Contract.Requires(f != null);

+      Contract.Requires(sink != null && predef != null);

+      Contract.Requires(f.EnclosingClass != null);

     

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);

       // parameters of the procedure

@@ -1242,6 +1263,7 @@ namespace Microsoft.Dafny {
         req, new Bpl.IdentifierExprSeq(), new Bpl.EnsuresSeq());

       sink.TopLevelDeclarations.Add(proc);

 

+      VariableSeq implInParams = Bpl.Formal.StripWhereClauses(proc.InParams);

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

       Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();

       // todo: include CEV information of parameters and the heap

@@ -1250,7 +1272,7 @@ namespace Microsoft.Dafny {
       foreach (Expression p in f.Req) {

         // Note, in this well-formedness check, function is passed in as null.  This will cause there to be

         // no reads checks or decreases checks.  This seems like a good idea, and I hope it is also sound.

-        CheckWellformed(p, null, Position.Positive, locals, builder, etran);

+        CheckWellformed(p, null, null, Position.Positive, locals, builder, etran);

         builder.Add(new Bpl.AssumeCmd(p.tok, etran.TrExpr(p)));

       }

       // Note: the reads clauses are not checked for well-formedness (is that sound?), because it used to

@@ -1260,21 +1282,72 @@ namespace Microsoft.Dafny {
       foreach (Expression p in f.Decreases) {

         // Note, in this well-formedness check, function is passed in as null.  This will cause there to be

         // no reads checks or decreases checks.  This seems like a good idea, and I hope it is also sound.

-        CheckWellformed(p, null, Position.Positive, locals, builder, etran);

+        CheckWellformed(p, null, null, Position.Positive, locals, builder, etran);

+      }

+      // Generate:

+      //   if (*) {

+      //     check well-formedness of postcondition

+      //   } else {

+      //     check well-formedness of body and check the postconditions themselves

+      //   }

+      // Here go the postconditions

+      StmtListBuilder postCheckBuilder = new StmtListBuilder();

+      foreach (Expression p in f.Ens) {

+        // Note, in this well-formedness check, function is passed in as null.  This will cause there to be

+        // no reads checks or decreases checks.  This seems like a good idea, and I hope it is also sound.

+        CheckWellformed(p, null, null, Position.Positive, locals, postCheckBuilder, etran);

+        // assume the postcondition for the benefit of checking the remaining postconditions

+        postCheckBuilder.Add(new Bpl.AssumeCmd(p.tok, etran.TrExpr(p)));

       }

-      // check well-formedness of the body

+      // Here goes the body

+      StmtListBuilder bodyCheckBuilder = new StmtListBuilder();

       if (f.Body != null) {

-        DefineFrame(f.tok, f.Reads, builder, locals);

-        CheckWellformed(f.Body, f, Position.Positive, locals, builder, etran);

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

+        Bpl.ExprSeq args = new Bpl.ExprSeq();

+        args.Add(etran.HeapExpr);

+        foreach (Variable p in implInParams) {

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

+        }

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

+

+        DefineFrame(f.tok, f.Reads, bodyCheckBuilder, locals);

+        CheckWellformed(f.Body, f, funcAppl, Position.Positive, locals, bodyCheckBuilder, etran);

+

+        // check that postconditions hold

+        foreach (Expression p in f.Ens) {

+          bodyCheckBuilder.Add(Assert(p.tok, etran.TrExpr(p), "possible violation of function postcondition"));

+        }

       }

+      // Combine the two

+      builder.Add(new Bpl.IfCmd(f.tok, null, postCheckBuilder.Collect(f.tok), null, bodyCheckBuilder.Collect(f.tok)));

 

       Bpl.Implementation impl = new Bpl.Implementation(f.tok, proc.Name,

-        typeParams,

-        Bpl.Formal.StripWhereClauses(proc.InParams),

-        Bpl.Formal.StripWhereClauses(proc.OutParams),

+        typeParams, implInParams, new Bpl.VariableSeq(),

         locals, builder.Collect(f.tok));

       sink.TopLevelDeclarations.Add(impl);

     }

+

+    Bpl.Expr CtorInvocation(MatchCaseExpr mc, ExpressionTranslator etran, Bpl.VariableSeq locals) {

+      Contract.Requires(mc != null);

+      Contract.Requires(etran != null);

+      Contract.Requires(locals != null);

+      Contract.Requires(predef != null);

+      Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

+

+      Bpl.ExprSeq args = new Bpl.ExprSeq();

+      for (int i = 0; i < mc.Arguments.Count; i++) {

+        BoundVar p = mc.Arguments[i];

+        Bpl.Variable local = new Bpl.LocalVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));

+        locals.Add(local);

+        IdentifierExpr ie = new IdentifierExpr(p.tok, p.UniqueName);

+        ie.Var = p; ie.Type = ie.Var.Type;  // resolve it here

+

+        Type t = mc.Ctor.Formals[i].Type;

+        args.Add(etran.CondApplyBox(mc.tok, new Bpl.IdentifierExpr(p.tok, local), cce.NonNull(p.Type), t));

+      }

+      Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(mc.tok, mc.Ctor.FullName, predef.DatatypeType);

+      return new Bpl.NAryExpr(mc.tok, new Bpl.FunctionCall(id), args);

+    }

     

     Bpl.Expr IsTotal(Expression expr, ExpressionTranslator etran){

       Contract.Requires(expr != null);Contract.Requires(etran != null);

@@ -1467,7 +1540,11 @@ namespace Microsoft.Dafny {
       }

     }

 

-    void CheckWellformed(Expression expr, Function func, Position pos, Bpl.VariableSeq locals, Bpl.StmtListBuilder builder, ExpressionTranslator etran){

+    /// <summary>

+    /// If "result" is non-null, then after checking the well-formedness of "expr", the generated code will

+    /// assume the equivalent of "result == expr".

+    /// </summary>

+    void CheckWellformed(Expression expr, Function func, Bpl.Expr result, Position pos, Bpl.VariableSeq locals, Bpl.StmtListBuilder builder, ExpressionTranslator etran){

       Contract.Requires(expr != null);

       Contract.Requires(locals != null);

       Contract.Requires(builder != null);

@@ -1479,11 +1556,11 @@ namespace Microsoft.Dafny {
       } else if (expr is DisplayExpression) {

         DisplayExpression e = (DisplayExpression)expr;

         foreach (Expression el in e.Elements) {

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

+          CheckWellformed(el, func, null, Position.Neither, locals, builder, etran);

         }

       } else if (expr is FieldSelectExpr) {

         FieldSelectExpr e = (FieldSelectExpr)expr;

-        CheckWellformed(e.Obj, func, Position.Neither, locals, builder, etran);

+        CheckWellformed(e.Obj, func, null, Position.Neither, locals, builder, etran);

         CheckNonNull(expr.tok, e.Obj, builder, etran);

         if (func != null && e.Field.IsMutable) {

           builder.Add(Assert(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), etran.TrExpr(e.Obj), GetField(e)), "insufficient reads clause to read field"));

@@ -1491,16 +1568,16 @@ namespace Microsoft.Dafny {
       } else if (expr is SeqSelectExpr) {

         SeqSelectExpr e = (SeqSelectExpr)expr;

         bool isSequence = e.Seq.Type is SeqType;

-        CheckWellformed(e.Seq, func, Position.Neither, locals, builder, etran);

+        CheckWellformed(e.Seq, func, null, Position.Neither, locals, builder, etran);

         Bpl.Expr seq = etran.TrExpr(e.Seq);

         Bpl.Expr e0 = null;

         if (e.E0 != null) {

           e0 = etran.TrExpr(e.E0);

-          CheckWellformed(e.E0, func, Position.Neither, locals, builder, etran);

+          CheckWellformed(e.E0, func, null, Position.Neither, locals, builder, etran);

           builder.Add(Assert(expr.tok, InSeqRange(expr.tok, e0, seq, isSequence, null, !e.SelectOne), "index out of range"));

         }

         if (e.E1 != null) {

-          CheckWellformed(e.E1, func, Position.Neither, locals, builder, etran);

+          CheckWellformed(e.E1, func, null, Position.Neither, locals, builder, etran);

           builder.Add(Assert(expr.tok, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, isSequence, e0, true), "end-of-range beyond length of " + (isSequence ? "sequence" : "array")));

         }

         if (func != null && cce.NonNull(e.Seq.Type).IsArrayType) {

@@ -1510,11 +1587,11 @@ namespace Microsoft.Dafny {
         }

       } else if (expr is MultiSelectExpr) {

         MultiSelectExpr e = (MultiSelectExpr)expr;

-        CheckWellformed(e.Array, func, Position.Neither, locals, builder, etran);

+        CheckWellformed(e.Array, func, null, Position.Neither, locals, builder, etran);

         Bpl.Expr array = etran.TrExpr(e.Array);

         int i = 0;

         foreach (Expression idx in e.Indices) {

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

+          CheckWellformed(idx, func, null, Position.Neither, locals, builder, etran);

 

           Bpl.Expr index = etran.TrExpr(idx);

           Bpl.Expr lower = Bpl.Expr.Le(Bpl.Expr.Literal(0), index);

@@ -1525,23 +1602,23 @@ namespace Microsoft.Dafny {
         }

       } else if (expr is SeqUpdateExpr) {

         SeqUpdateExpr e = (SeqUpdateExpr)expr;

-        CheckWellformed(e.Seq, func, Position.Neither, locals, builder, etran);

+        CheckWellformed(e.Seq, func, null, Position.Neither, locals, builder, etran);

         Bpl.Expr seq = etran.TrExpr(e.Seq);

         Bpl.Expr index = etran.TrExpr(e.Index);

-        CheckWellformed(e.Index, func, Position.Neither, locals, builder, etran);

+        CheckWellformed(e.Index, func, null, Position.Neither, locals, builder, etran);

         builder.Add(Assert(expr.tok, InSeqRange(expr.tok, index, seq, true, null, false), "index out of range"));

-        CheckWellformed(e.Value, func, Position.Neither, locals, builder, etran);

+        CheckWellformed(e.Value, func, null, Position.Neither, locals, builder, etran);

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

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

+        CheckWellformed(e.Receiver, func, null, Position.Neither, locals, builder, etran);

         if (!e.Function.IsStatic && !(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);

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

         }

         // create a local variable for each formal parameter, and assign each actual parameter to the corresponding local

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

@@ -1581,46 +1658,46 @@ namespace Microsoft.Dafny {
       } else if (expr is DatatypeValue) {

         DatatypeValue dtv = (DatatypeValue)expr;

         foreach (Expression arg in dtv.Arguments) {

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

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

         }

       } else if (expr is OldExpr) {

         OldExpr e = (OldExpr)expr;

-        CheckWellformed(e.E, func, pos, locals, builder, etran.Old);

+        CheckWellformed(e.E, func, null, pos, locals, builder, etran.Old);

       } else if (expr is FreshExpr) {

         FreshExpr e = (FreshExpr)expr;

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

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

       } else if (expr is UnaryExpr) {

         UnaryExpr e = (UnaryExpr)expr;

-        CheckWellformed(e.E, func, e.Op == UnaryExpr.Opcode.Not ? Negate(pos) : Position.Neither, locals, builder, etran);

+        CheckWellformed(e.E, func, null, e.Op == UnaryExpr.Opcode.Not ? Negate(pos) : Position.Neither, locals, builder, etran);

         if (e.Op == UnaryExpr.Opcode.SeqLength && !(e.E.Type is SeqType)) {

           CheckNonNull(expr.tok, e.E, builder, etran);

         }

       } else if (expr is BinaryExpr) {

         BinaryExpr e = (BinaryExpr)expr;

-        CheckWellformed(e.E0, func, e.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp ? Negate(pos) : pos, locals, builder, etran);

+        CheckWellformed(e.E0, func, null, e.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp ? Negate(pos) : pos, locals, builder, etran);

         switch (e.ResolvedOp) {

           case BinaryExpr.ResolvedOpcode.And:

           case BinaryExpr.ResolvedOpcode.Imp:

             {

               Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();

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

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

               builder.Add(new Bpl.IfCmd(expr.tok, etran.TrExpr(e.E0), b.Collect(expr.tok), null, null));

             }

             break;

           case BinaryExpr.ResolvedOpcode.Or:

             {

               Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();

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

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

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

+            CheckWellformed(e.E1, func, null, 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);

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

             break;

         }

 

@@ -1636,46 +1713,47 @@ namespace Microsoft.Dafny {
           locals.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.UniqueName, TrType(local.Type))));

         }

         Expression body = Substitute(e.Body, null, substMap);

-        CheckWellformed(body, func, pos, locals, builder, etran);

+        CheckWellformed(body, func, null, pos, locals, builder, etran);

 

       } else if (expr is ITEExpr) {

         ITEExpr e = (ITEExpr)expr;

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

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

         Bpl.StmtListBuilder bThen = new Bpl.StmtListBuilder();

         Bpl.StmtListBuilder bElse = new Bpl.StmtListBuilder();

-        CheckWellformed(e.Thn, func, pos, locals, bThen, etran);

-        CheckWellformed(e.Els, func, pos, locals, bElse, etran);

+        CheckWellformed(e.Thn, func, null, pos, locals, bThen, etran);

+        CheckWellformed(e.Els, func, null, pos, locals, bElse, etran);

         builder.Add(new Bpl.IfCmd(expr.tok, etran.TrExpr(e.Test), bThen.Collect(expr.tok), null, bElse.Collect(expr.tok)));

       

       } else if (expr is MatchExpr) {

         MatchExpr me = (MatchExpr)expr;

-        CheckWellformed(me.Source, func, pos, locals, builder, etran);

+        CheckWellformed(me.Source, func, null, pos, locals, builder, etran);

         Bpl.Expr src = etran.TrExpr(me.Source);

-        foreach (MatchCaseExpr mc in me.Cases) {

-          Contract.Assert( mc.Ctor != null);  // follows from the fact that mc has been successfully resolved

-          Bpl.ExprSeq args = new Bpl.ExprSeq();

-          for (int i = 0; i < mc.Arguments.Count; i++) {

-            BoundVar p = mc.Arguments[i];

-            Bpl.Variable local = new Bpl.LocalVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));

-            locals.Add(local);

-            IdentifierExpr ie = new IdentifierExpr(p.tok, p.UniqueName);

-            ie.Var = p;  ie.Type = ie.Var.Type;  // resolve it here

-

-            Type t = mc.Ctor.Formals[i].Type;

-            args.Add(etran.CondApplyBox(expr.tok, new Bpl.IdentifierExpr(p.tok, local), cce.NonNull(p.Type), t));

-          }

-          Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(mc.tok, mc.Ctor.FullName, predef.DatatypeType);

-          Bpl.Expr ct = new Bpl.NAryExpr(mc.tok, new Bpl.FunctionCall(id), args);

-

-          // generate:  if (src == ctor(args)) { mc.Body is well-formed }

+        Bpl.IfCmd ifcmd = null;

+        StmtListBuilder elsBldr = new StmtListBuilder();

+        elsBldr.Add(new Bpl.AssumeCmd(expr.tok, Bpl.Expr.False));

+        StmtList els = elsBldr.Collect(expr.tok);

+        for (int i = me.Cases.Count; 0 <= --i; ) {

+          MatchCaseExpr mc = me.Cases[i];

+          Bpl.Expr ct = CtorInvocation(mc, etran, locals);

+          // generate:  if (src == ctor(args)) { mc.Body is well-formed; assume Result == TrExpr(case); } else ...

           Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();

-          CheckWellformed(mc.Body, func, pos, locals, b, etran);

-          builder.Add(new Bpl.IfCmd(mc.tok, Bpl.Expr.Eq(src, ct), b.Collect(mc.tok), null, null));

+          CheckWellformed(mc.Body, func, null, pos, locals, b, etran);

+          if (result != null) {

+            b.Add(new Bpl.AssumeCmd(mc.tok, Bpl.Expr.Eq(result, etran.TrExpr(mc.Body))));

+          }

+          ifcmd = new Bpl.IfCmd(mc.tok, Bpl.Expr.Eq(src, ct), b.Collect(mc.tok), ifcmd, els);

+          els = null;

         }

+        builder.Add(ifcmd);

+        result = null;

         

       } else {

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

       }

+

+      if (result != null) {

+        builder.Add(new Bpl.AssumeCmd(expr.tok, Bpl.Expr.Eq(result, etran.TrExpr(expr))));

+      }

     }

 

     List<Expression> MethodDecreasesWithDefault(Method m, out bool inferredDecreases) {

@@ -1897,7 +1975,7 @@ namespace Microsoft.Dafny {
     void AddFunction(Function f)

     {

       Contract.Requires(f != null);

-      Contract.Requires( predef != null && sink != null);

+      Contract.Requires(predef != null && sink != null);

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

@@ -1923,14 +2001,13 @@ namespace Microsoft.Dafny {
     /// In addition, it is used once to generate refinement conditions.

     /// </summary>    

     Bpl.Procedure AddMethod(Method m, bool wellformednessProc, bool skipEnsures)

-     {

+    {

       Contract.Requires(m != null);

-      Contract.Requires( predef != null);

-      Contract.Requires( m.EnclosingClass != null);

-     Contract.Requires( !skipEnsures || !wellformednessProc);

+      Contract.Requires(predef != null);

+      Contract.Requires(m.EnclosingClass != null);

+      Contract.Requires(!skipEnsures || !wellformednessProc);

       Contract.Ensures(Contract.Result<Bpl.Procedure>() != null);

 

-

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok);

       

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

@@ -2016,6 +2093,13 @@ namespace Microsoft.Dafny {
         }

       }

 

+#if COMING_SOON

+      // For ghost methods, add postcondition that the heap is not modified whatsoever

+      if (m.IsGhost && !wellformednessProc) {

+        ens.Add(Ensures(m.tok, false, Bpl.Expr.Eq(etran.HeapExpr, etran.Old.HeapExpr), "ghost methods are not allowed to modify the heap whatsoever", "ghost methods have no effect on heap"));

+      }

+#endif

+

       // CEV information

       // free requires #cev_pc == 0;

       req.Add(Requires(m.tok, true, Bpl.Expr.Eq(Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int), Bpl.Expr.Literal(0)), null, "CEV information"));

@@ -3121,12 +3205,12 @@ void ObjectInvariant()
       Contract.Requires(locals != null);

       Contract.Requires(etran != null);

       Contract.Requires(varPrefix != null);

-    Contract.Requires(builder != null);

-    Contract.Requires(decreases != null);

+      Contract.Requires(builder != null);

+      Contract.Requires(decreases != null);

       List<Bpl.Expr> oldBfs = new List<Bpl.Expr>();

       int c = 0;

       foreach (Expression e in decreases) {

-    Contract.Assert(e != null);

+        Contract.Assert(e != null);

         Bpl.LocalVariable bfVar = new Bpl.LocalVariable(e.tok, new Bpl.TypedIdent(e.tok, varPrefix + c, TrType(cce.NonNull(e.Type))));

         locals.Add(bfVar);

         Bpl.IdentifierExpr bf = new Bpl.IdentifierExpr(e.tok, bfVar);

@@ -3466,7 +3550,7 @@ void ObjectInvariant()
         if (tRhs.ArrayDimensions != null) {

           int i = 0;

           foreach (Expression dim in tRhs.ArrayDimensions) {

-            CheckWellformed(dim, null, Position.Positive, locals, builder, etran);

+            CheckWellformed(dim, null, null, Position.Positive, locals, builder, etran);

             if (tRhs.ArrayDimensions.Count == 1) {

               builder.Add(Assert(tok, Bpl.Expr.Le(Bpl.Expr.Literal(0), etran.TrExpr(dim)),

                 tRhs.ArrayDimensions.Count == 1 ? "array size might be negative" : string.Format("array size (dimension {0}) might be negative", i)));

@@ -3531,15 +3615,14 @@ void ObjectInvariant()
       public readonly string This;

       readonly Function applyLimited_CurrentFunction;

       [ContractInvariantMethod]

-void ObjectInvariant() 

-{

-    Contract.Invariant(HeapExpr!=null);

+      void ObjectInvariant() 

+      {

+        Contract.Invariant(HeapExpr!=null);

         Contract.Invariant(predef != null);

         Contract.Invariant(translator != null);

         Contract.Invariant(This != null);

-}

+      }

 

-      

       public ExpressionTranslator(Translator translator, PredefinedDecls predef, IToken heapToken) {

         Contract.Requires(translator != null);

         Contract.Requires(predef != null);

@@ -3601,7 +3684,7 @@ void ObjectInvariant()
 

         return new ExpressionTranslator(translator, predef, HeapExpr, applyLimited_CurrentFunction);

       }

-      

+

       public Bpl.IdentifierExpr TheFrame(IToken tok)

       {

         Contract.Requires(tok != null);

@@ -3633,9 +3716,9 @@ void ObjectInvariant()
       }

 

       public Bpl.Expr TrExpr(Expression expr)

-       {

+      {

         Contract.Requires(expr != null);

-       Contract.Requires( predef != null);

+        Contract.Requires( predef != null);

         if (expr is LiteralExpr) {

           LiteralExpr e = (LiteralExpr)expr;

           if (e.Value == null) {

@@ -3650,7 +3733,7 @@ void ObjectInvariant()
           

         } else if (expr is ThisExpr) {

           return new Bpl.IdentifierExpr(expr.tok, This, predef.RefType);

-          

+        

         } else if (expr is IdentifierExpr) {

           IdentifierExpr e = (IdentifierExpr)expr;

           return TrVar(expr.tok, cce.NonNull(e.Var));

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 4b4bf920..34b9a0be 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -87,17 +87,17 @@ Execution trace:
     (0,0): anon0

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

 Execution trace:

-    (0,0): anon10_Then

+    (0,0): anon12_Then

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

 Execution trace:

-    (0,0): anon10_Else

+    (0,0): anon12_Else

     (0,0): anon3

-    (0,0): anon11_Else

+    (0,0): anon13_Else

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

 Execution trace:

-    (0,0): anon10_Then

+    (0,0): anon12_Then

     (0,0): anon3

-    (0,0): anon11_Then

+    (0,0): anon13_Then

     (0,0): anon6

 SmallTests.dfy(82,20): Error: decreases expression must be well defined at top of each loop iteration

 Execution trace:

@@ -129,7 +129,7 @@ Dafny program verifier finished with 28 verified, 9 errors
 -------------------- Definedness.dfy --------------------

 Definedness.dfy(8,7): Error: possible division by zero

 Execution trace:

-    (0,0): anon0

+    (0,0): anon3_Else

 Definedness.dfy(15,16): Error: possible division by zero

 Execution trace:

     (0,0): anon0

@@ -263,8 +263,22 @@ Execution trace:
 Definedness.dfy(210,23): Error BP5004: This loop invariant might not hold on entry.

 Execution trace:

     (0,0): anon0

+Definedness.dfy(231,30): Error: possible violation of function postcondition

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Else

+Definedness.dfy(238,22): Error: target object may be null

+Execution trace:

+    (0,0): anon5_Then

+    (0,0): anon2

+    (0,0): anon6_Then

+Definedness.dfy(254,24): Error: possible violation of function postcondition

+Execution trace:

+    (0,0): anon7_Then

+    (0,0): anon2

+    (0,0): anon8_Else

 

-Dafny program verifier finished with 21 verified, 29 errors

+Dafny program verifier finished with 23 verified, 32 errors

 

 -------------------- Array.dfy --------------------

 Array.dfy(10,12): Error: assignment may update an array element not in the enclosing method's modifies clause

@@ -293,14 +307,14 @@ Execution trace:
     (0,0): anon0

 Array.dfy(107,6): Error: insufficient reads clause to read array element

 Execution trace:

-    (0,0): anon0

-    (0,0): anon4_Then

-    (0,0): anon5_Then

+    (0,0): anon7_Else

+    (0,0): anon8_Then

+    (0,0): anon9_Then

 Array.dfy(115,6): Error: insufficient reads clause to read array element

 Execution trace:

-    (0,0): anon0

-    (0,0): anon4_Then

-    (0,0): anon5_Then

+    (0,0): anon7_Else

+    (0,0): anon8_Then

+    (0,0): anon9_Then

 Array.dfy(131,10): Error: assignment may update an array element not in the enclosing method's modifies clause

 Execution trace:

     (0,0): anon0

@@ -348,7 +362,7 @@ Dafny program verifier finished with 16 verified, 2 errors
 -------------------- BadFunction.dfy --------------------

 BadFunction.dfy(6,3): Error: failure to decrease termination measure

 Execution trace:

-    (0,0): anon0

+    (0,0): anon3_Else

 

 Dafny program verifier finished with 2 verified, 1 error

 

@@ -437,7 +451,7 @@ DTypes.dfy(54,18): Error: assertion violation
 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 13 verified, 3 errors

+Dafny program verifier finished with 14 verified, 3 errors

 

 -------------------- TypeParameters.dfy --------------------

 TypeParameters.dfy(41,22): Error: assertion violation

diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy
index c6f0737c..d925587b 100644
--- a/Test/dafny0/DTypes.dfy
+++ b/Test/dafny0/DTypes.dfy
@@ -74,3 +74,16 @@ class Node { }
 

 class CP<T,U> {

 }

+

+datatype Data {

+  Lemon;

+  Kiwi(int);

+}

+

+function G(d: Data): int

+  requires d != #Data.Lemon;

+{

+  match d

+  case Lemon => G(d)

+  case Kiwi(x) => 7

+}

diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy
index d557de21..1cb74b1d 100644
--- a/Test/dafny0/Definedness.dfy
+++ b/Test/dafny0/Definedness.dfy
@@ -213,3 +213,45 @@ class StatementTwoShoes {
     }

   }

 }

+

+// ----------------- function postconditions ----------------------

+

+class Mountain { var x: int; }

+

+function Postie0(c: Mountain): Mountain

+  requires c != null;

+  ensures Postie0(c) != null && Postie0(c).x <= Postie0(c).x;

+  ensures Postie0(c).x == Postie0(c).x;

+{

+  c

+}

+

+function Postie1(c: Mountain): Mountain

+  requires c != null;

+  ensures Postie1(c) != null && Postie1(c).x == 5;  // error: postcondition violation (but no well-formedness problem)

+{

+  c

+}

+

+function Postie2(c: Mountain): Mountain

+  requires c != null && c.x == 5;

+  ensures Postie2(c).x == 5;  // well-formedness error (null dereference)

+{

+  c

+}

+

+function Postie3(c: Mountain): Mountain  // all is cool

+  requires c != null && c.x == 5;

+  ensures Postie3(c) != null && Postie3(c).x < 10;

+  ensures Postie3(c).x == 5;

+{

+  c

+}

+

+function Postie4(c: Mountain): Mountain

+  requires c != null && c.x <= 5;

+  ensures Postie4(c) != null && Postie4(c).x < 10;

+  ensures Postie4(c).x == 5;  // error: postcondition might not hold

+{

+  c

+}

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index b8f9591f..5b51b3e4 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -9,7 +9,7 @@ Dafny program verifier finished with 22 verified, 0 errors
 

 -------------------- PriorityQueue.dfy --------------------

 

-Dafny program verifier finished with 12 verified, 0 errors

+Dafny program verifier finished with 24 verified, 0 errors

 

 -------------------- BinaryTree.dfy --------------------

 

diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy
index 76e4b1d6..4a9ba220 100644
--- a/Test/dafny1/PriorityQueue.dfy
+++ b/Test/dafny1/PriorityQueue.dfy
@@ -49,7 +49,7 @@ class PriorityQueue {
     requires 1 <= k && k <= n;

     requires MostlyValid();

     requires (forall j :: 2 <= j && j <= n && j != k ==> a[j/2] <= a[j]);

-    requires (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j != k ==> a[j/2/2] <= a[j]);

+    requires (forall j :: 1 <= j && j <= n ==> j/2 != k);  // k is a child

     modifies a;

     ensures Valid();

   {

@@ -58,7 +58,7 @@ class PriorityQueue {
     while (1 < i)

       invariant i <= k && MostlyValid();

       invariant (forall j :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);

-      invariant (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j != i ==> a[j/2/2] <= a[j]);

+      invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);

     {

       if (a[i/2] <= a[i]) {

         return;

@@ -84,7 +84,7 @@ class PriorityQueue {
     requires 1 <= k;

     requires MostlyValid();

     requires (forall j :: 2 <= j && j <= n && j/2 != k ==> a[j/2] <= a[j]);

-    requires (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != k ==> a[j/2/2] <= a[j]);

+    requires k == 1;

     modifies a;

     ensures Valid();

   {

@@ -92,7 +92,121 @@ class PriorityQueue {
     while (2*i <= n)  // while i is not a leaf

       invariant 1 <= i && MostlyValid();

       invariant (forall j :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);

-      invariant (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != i ==> a[j/2/2] <= a[j]);

+      invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);

+    {

+      var smallestChild;

+      if (2*i + 1 <= n && a[2*i + 1] < a[2*i]) {

+        smallestChild := 2*i + 1;

+      } else {

+        smallestChild := 2*i;

+      }

+      if (a[i] <= a[smallestChild]) {

+        return;

+      }

+      var tmp := a[i];  a[i] := a[smallestChild];  a[smallestChild] := tmp;

+      i := smallestChild;

+      assert 1 <= i/2/2 ==> a[i/2/2] <= a[i];

+    }

+  }

+}

+

+// ---------- Alternative specifications ----------

+

+class PriorityQueue_Alternative {

+  var N: int;  // capacity

+  var n: int;  // current size

+  ghost var Repr: set<object>;  // set of objects that make up the representation of a PriorityQueue

+

+  var a: array<int>;  // private implementation of PriorityQueu

+

+  function Valid(): bool

+    reads this, Repr;

+  {

+    MostlyValid() &&

+    (forall j :: 2 <= j && j <= n ==> a[j/2] <= a[j])

+  }

+

+  function MostlyValid(): bool

+    reads this, Repr;

+  {

+    this in Repr && a in Repr &&

+    a != null && a.Length == N+1 &&

+    0 <= n && n <= N

+  }

+

+  method Init(capacity: int)

+    requires 0 <= capacity;

+    modifies this;

+    ensures Valid() && fresh(Repr - {this});

+    ensures N == capacity;

+  {

+    N := capacity;

+    var arr := new int[N+1];

+    a := arr;

+    n := 0;

+    Repr := {this};

+    Repr := Repr + {a};

+  }

+

+  method Insert(x: int)

+    requires Valid() && n < N;

+    modifies this, a;

+    ensures Valid() && fresh(Repr - old(Repr));

+    ensures n == old(n) + 1 && N == old(N);

+  {

+    n := n + 1;

+    a[n] := x;

+    call SiftUp(n);

+  }

+

+  method SiftUp(k: int)

+    requires 1 <= k && k <= n;

+    requires MostlyValid();

+    requires (forall j :: 2 <= j && j <= n && j != k ==> a[j/2] <= a[j]);

+    requires (forall j :: 1 <= j && j <= n ==> j/2 != k);  // k is a child

+    modifies a;

+    ensures Valid();

+  {

+    var i := k;

+    assert MostlyValid();

+    while (1 < i)

+      invariant i <= k && MostlyValid();

+      invariant (forall j :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);

+      invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);

+    {

+      if (a[i/2] <= a[i]) {

+        return;

+      }

+      var tmp := a[i];  a[i] := a[i/2];  a[i/2] := tmp;

+      i := i / 2;

+    }

+  }

+

+  method RemoveMin() returns (x: int)

+    requires Valid() && 1 <= n;

+    modifies this, a;

+    ensures Valid() && fresh(Repr - old(Repr));

+    ensures n == old(n) - 1;

+  {

+    x := a[1];

+    a[1] := a[n];

+    n := n - 1;

+    call SiftDown(1);

+  }

+

+  method SiftDown(k: int)

+    requires 1 <= k;

+    requires MostlyValid();

+    requires (forall j :: 2 <= j && j <= n && j/2 != k ==> a[j/2] <= a[j]);

+    requires k == 1;  // k is the root

+    modifies a;

+    ensures Valid();

+  {

+    var i := k;

+    while (2*i <= n)  // while i is not a leaf

+      invariant 1 <= i && MostlyValid();

+      invariant (forall j :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);

+      invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);

     {

       var smallestChild;

       if (2*i + 1 <= n && a[2*i + 1] < a[2*i]) {

diff --git a/Test/dafny1/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy
index fb530258..76925e8e 100644
--- a/Test/dafny1/TerminationDemos.dfy
+++ b/Test/dafny1/TerminationDemos.dfy
@@ -30,6 +30,19 @@ class Ackermann {
     else

       F(m - 1, F(m, n - 1))

   }

+/*

+  function G(m: int, n: int): int

+    requires 0 <= m && 0 <= n;

+    ensures 0 <= G(m, n);

+  {

+    if m == 0 then

+      n + 1

+    else if n == 0 then

+      G(m - 1, 1)

+    else

+      G(m - 1, G(m, n - 1))

+  }

+*/

 }

 

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