Dafny:

* Added "decreases" clauses to methods.
* Interpret the filename stdin.dfy as an indication to read the program from standard input.

11 files changed, 301 insertions, 192 deletions

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index fe2e6a8c..d6f3aeae 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -61,10 +61,16 @@ private static Expression! ConvertToLocal(Expression! e)
 /// Note: first initialize the Scanner.

 ///</summary>

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

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

-    BoogiePL.Buffer.Fill(reader);

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

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

     Scanner.Init(filename);

     return Parse(classes);

+  } else {

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

+      BoogiePL.Buffer.Fill(reader);

+      Scanner.Init(filename);

+      return Parse(classes);

+    }

   }

 }

 

@@ -260,6 +266,7 @@ MethodDecl<MemberModifiers mmod, out Method! m>
      List<MaybeFreeExpression!> req = new List<MaybeFreeExpression!>();

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

      List<MaybeFreeExpression!> ens = new List<MaybeFreeExpression!>();

+     List<Expression!> dec = new List<Expression!>();

      Statement! bb;  Statement body = null;

   .)

   "method"

@@ -274,16 +281,17 @@ MethodDecl<MemberModifiers mmod, out Method! m>
     Formals<false, outs>

   ]

 

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

-  | { MethodSpec<req, mod, ens> } BlockStmt<out bb>    (. body = bb; .)

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

+  | { MethodSpec<req, mod, ens, dec> } BlockStmt<out bb>    (. body = bb; .)

   )

   

   (. parseVarScope.PopMarker();

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

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

   .)

   .

 

-MethodSpec<List<MaybeFreeExpression!\>! req, List<Expression!\>! mod, List<MaybeFreeExpression!\>! ens>

+MethodSpec<List<MaybeFreeExpression!\>! req, List<Expression!\>! mod, List<MaybeFreeExpression!\>! ens,

+           List<Expression!\>! decreases>

 = (. Expression! e;  bool isFree = false;

   .)

   ( "modifies" [ Expression<out e>                           (. mod.Add(e); .)

@@ -295,6 +303,7 @@ MethodSpec<List<MaybeFreeExpression!\>! req, List<Expression!\>! mod, List<Maybe
     ( "requires" Expression<out e> ";"                       (. req.Add(new MaybeFreeExpression(e, isFree)); .)

     | "ensures" Expression<out e> ";"                        (. ens.Add(new MaybeFreeExpression(e, isFree)); .)

     )

+  | "decreases" PossiblyWildExpressions<decreases> ";"

   )

   .

 

diff --git a/Dafny/DafnyAst.ssc b/Dafny/DafnyAst.ssc
index 549a32e0..b22e9cf6 100644
--- a/Dafny/DafnyAst.ssc
+++ b/Dafny/DafnyAst.ssc
@@ -494,6 +494,7 @@ namespace Microsoft.Dafny
     public readonly List<MaybeFreeExpression!>! Req;

     public readonly List<Expression!>! Mod;

     public readonly List<MaybeFreeExpression!>! Ens;

+    public readonly List<Expression!>! Decreases;

     public readonly Statement Body;

     

     public Method(Token! tok, string! name,

@@ -501,6 +502,7 @@ namespace Microsoft.Dafny
                   [Captured] List<TypeParameter!>! typeArgs,

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

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

+                  [Captured] List<Expression!>! decreases,

                   [Captured] Statement body,

                   Attributes attributes) {

       this.IsClass = isClass;

@@ -511,6 +513,7 @@ namespace Microsoft.Dafny
       this.Req = req;

       this.Mod = mod;

       this.Ens = ens;

+      this.Decreases = decreases;

       this.Body = body;

       base(tok, name, attributes);

     }

diff --git a/Dafny/Parser.ssc b/Dafny/Parser.ssc
index ec3e44f4..0560a45b 100644
--- a/Dafny/Parser.ssc
+++ b/Dafny/Parser.ssc
@@ -59,10 +59,16 @@ private static Expression! ConvertToLocal(Expression! e)
 /// Note: first initialize the Scanner.

 ///</summary>

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

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

-    BoogiePL.Buffer.Fill(reader);

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

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

     Scanner.Init(filename);

     return Parse(classes);

+  } else {

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

+      BoogiePL.Buffer.Fill(reader);

+      Scanner.Init(filename);

+      return Parse(classes);

+    }

   }

 }

 

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

 		if (t.kind == 11) {

 			FieldDecl(mmod, mm);

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

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

 			FunctionDecl(mmod, out f);

 			mm.Add(f); 

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

@@ -279,7 +285,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		List<Expression!> decreases = new List<Expression!>();

 		Expression! bb;  Expression body = null;

 		

-		Expect(29);

+		Expect(30);

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

 		

 		while (t.kind == 5) {

@@ -295,11 +301,11 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		Type(out returnType);

 		if (t.kind == 10) {

 			Get();

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

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

 				FunctionSpec(reqs, reads, decreases);

 			}

 		} else if (StartOf(2)) {

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

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

 				FunctionSpec(reqs, reads, decreases);

 			}

 			FunctionBody(out bb);

@@ -319,6 +325,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		List<MaybeFreeExpression!> req = new List<MaybeFreeExpression!>();

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

 		List<MaybeFreeExpression!> ens = new List<MaybeFreeExpression!>();

+		List<Expression!> dec = new List<Expression!>();

 		Statement! bb;  Statement body = null;

 		

 		Expect(16);

@@ -340,17 +347,17 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		if (t.kind == 10) {

 			Get();

 			while (StartOf(3)) {

-				MethodSpec(req, mod, ens);

+				MethodSpec(req, mod, ens, dec);

 			}

 		} else if (StartOf(4)) {

 			while (StartOf(3)) {

-				MethodSpec(req, mod, ens);

+				MethodSpec(req, mod, ens, dec);

 			}

 			BlockStmt(out bb);

 			body = bb; 

 		} else Error(96);

 		parseVarScope.PopMarker();

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

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

 		

 	}

 

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

 		}

 		parseVarScope.PushMarker(); 

-		if (t.kind == 22) {

+		if (t.kind == 23) {

 			FormalsOptionalIds(formals);

 		}

 		parseVarScope.PopMarker();

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

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

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

-		Expect(22);

+		Expect(23);

 		if (StartOf(5)) {

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

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

@@ -389,7 +396,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 				formals.Add(new Formal(id, name, ty, true));  parseVarScope.Push(name, name); 

 			}

 		}

-		Expect(23);

+		Expect(24);

 	}

 

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

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

 		List<Type!>! gt;

 		

-		if (t.kind == 24) {

+		if (t.kind == 25) {

 			Get();

 			tok = token; 

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

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

 			Get();

 			tok = token;  ty = new IntType(); 

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

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

 			Get();

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

 			GenericInstantiation(gt);

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

 			ty = new SetType(gt[0]);

 			

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

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

 			Get();

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

 			GenericInstantiation(gt);

@@ -465,14 +472,14 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			}

 			ty = new SeqType(gt[0]);

 			

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

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

 			ReferenceType(out tok, out ty);

 		} else Error(97);

 	}

 

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

 		Token! id;  Type! ty; 

-		Expect(22);

+		Expect(23);

 		if (t.kind == 1) {

 			IdentType(out id, out ty);

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

@@ -482,10 +489,11 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 				formals.Add(new Formal(id, id.val, ty, incoming));  parseVarScope.Push(id.val, id.val); 

 			}

 		}

-		Expect(23);

+		Expect(24);

 	}

 

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

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

+List<Expression!>! decreases) {

 		Expression! e;  bool isFree = false;

 		

 		if (t.kind == 18) {

@@ -516,6 +524,10 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 				Expect(10);

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

 			} else Error(98);

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

+			Get();

+			PossiblyWildExpressions(decreases);

+			Expect(10);

 		} else Error(99);

 	}

 

@@ -553,6 +565,17 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		} else Error(100);

 	}

 

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

+		Expression! e; 

+		PossiblyWildExpression(out e);

+		args.Add(e); 

+		while (t.kind == 12) {

+			Get();

+			PossiblyWildExpression(out e);

+			args.Add(e); 

+		}

+	}

+

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

 		Type! ty; 

 		Expect(14);

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

 		List<Type!>! gt;

 		

-		if (t.kind == 28) {

+		if (t.kind == 29) {

 			Get();

 			tok = token;  ty = new ObjectType(); 

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

@@ -590,13 +613,13 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			Expression(out e);

 			Expect(10);

 			reqs.Add(e); 

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

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

 			Get();

 			if (StartOf(9)) {

 				PossiblyWildExpressions(reads);

 			}

 			Expect(10);

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

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

 			Get();

 			Expressions(decreases);

 			Expect(10);

@@ -614,17 +637,6 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		Expect(6);

 	}

 

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

-		Expression! e; 

-		PossiblyWildExpression(out e);

-		args.Add(e); 

-		while (t.kind == 12) {

-			Get();

-			PossiblyWildExpression(out e);

-			args.Add(e); 

-		}

-	}

-

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

 		Expression! e; 

 		Expression(out e);

@@ -679,7 +691,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		Expect(34);

 		x = token;  parseVarScope.PushMarker(); 

 		Ident(out id);

-		if (t.kind == 22) {

+		if (t.kind == 23) {

 			Get();

 			Ident(out arg);

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

@@ -690,7 +702,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 				arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));

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

 			}

-			Expect(23);

+			Expect(24);

 		}

 		Expect(35);

 		Expression(out body);

@@ -729,7 +741,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			UseStmt(out s);

 			break;

 		}

-		case 1: case 22: case 85: case 86: {

+		case 1: case 23: case 85: case 86: {

 			AssignStmt(out s);

 			break;

 		}

@@ -947,7 +959,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		x = token; 

 		Guard(out guard);

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

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

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

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

 				isFree = false; 

 				if (t.kind == 19) {

@@ -982,7 +994,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		range = new LiteralExpr(x, true);

 		ty = new InferredTypeProxy();

 		

-		Expect(22);

+		Expect(23);

 		Ident(out boundVar);

 		if (t.kind == 13) {

 			Get();

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

 			Expression(out range);

 		}

-		Expect(23);

+		Expect(24);

 		Expect(5);

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

 			if (t.kind == 50) {

@@ -1044,7 +1056,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		Token! id;  e = dummyExpr; 

 		if (t.kind == 1) {

 			IdentOrFuncExpression(out e);

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

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

 			ObjectExpression(out e);

 		} else Error(111);

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

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

 	static void Guard(out Expression e) {

 		Expression! ee;  e = null; 

-		Expect(22);

+		Expect(23);

 		if (t.kind == 32) {

 			Get();

 			e = null; 

@@ -1089,14 +1101,14 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			Expression(out ee);

 			e = ee; 

 		} else Error(112);

-		Expect(23);

+		Expect(24);

 	}

 

 	static void CallStmtSubExpr(out Expression! e) {

 		e = dummyExpr; 

 		if (t.kind == 1) {

 			IdentOrFuncExpression(out e);

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

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

 			ObjectExpression(out e);

 			SelectOrCallSuffix(ref e);

 		} else Error(113);

@@ -1370,12 +1382,12 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			Expect(80);

 			Ident(out id);

 			elements = new List<Expression!>(); 

-			if (t.kind == 22) {

+			if (t.kind == 23) {

 				Get();

 				if (StartOf(6)) {

 					Expressions(elements);

 				}

-				Expect(23);

+				Expect(24);

 			}

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

 			break;

@@ -1383,9 +1395,9 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		case 81: {

 			Get();

 			x = token; 

-			Expect(22);

-			Expression(out e);

 			Expect(23);

+			Expression(out e);

+			Expect(24);

 			e = new FreshExpr(x, e); 

 			break;

 		}

@@ -1435,13 +1447,13 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 	static void IdentOrFuncExpression(out Expression! e) {

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

 		Ident(out id);

-		if (t.kind == 22) {

+		if (t.kind == 23) {

 			Get();

 			args = new List<Expression!>(); 

 			if (StartOf(6)) {

 				Expressions(args);

 			}

-			Expect(23);

+			Expect(24);

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

 		}

 		if (e == dummyExpr) {

@@ -1462,18 +1474,18 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		} else if (t.kind == 86) {

 			Get();

 			x = token; 

-			Expect(22);

-			Expression(out e);

 			Expect(23);

+			Expression(out e);

+			Expect(24);

 			e = new OldExpr(x, e); 

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

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

 			Get();

 			if (StartOf(15)) {

 				QuantifierGuts(out e);

 			} else if (StartOf(6)) {

 				Expression(out e);

 			} else Error(124);

-			Expect(23);

+			Expect(24);

 		} else Error(125);

 	}

 

@@ -1485,13 +1497,13 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 		if (t.kind == 80) {

 			Get();

 			Ident(out id);

-			if (t.kind == 22) {

+			if (t.kind == 23) {

 				Get();

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

 				if (StartOf(6)) {

 					Expressions(args);

 				}

-				Expect(23);

+				Expect(24);

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

 			}

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

@@ -1682,16 +1694,16 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 			case 19: s = "free expected"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@@ -1802,22 +1814,22 @@ public static int Parse (List<TopLevelDecl!>! classes) {
 

 	static bool[,]! set = {

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 

 	};

 

diff --git a/Dafny/Printer.ssc b/Dafny/Printer.ssc
index 89b9f62e..23e6dfce 100644
--- a/Dafny/Printer.ssc
+++ b/Dafny/Printer.ssc
@@ -137,24 +137,9 @@ namespace Microsoft.Dafny {
       } else {

         wr.WriteLine();

       }

-      foreach (Expression r in f.Req) {

-        Indent(2 * IndentAmount);

-        wr.Write("requires ");

-        PrintExpression(r);

-        wr.WriteLine(";");

-      }

-      foreach (Expression r in f.Reads) {

-        Indent(2 * IndentAmount);

-        wr.Write("reads ");

-        PrintExpression(r);

-        wr.WriteLine(";");

-      }

-      foreach (Expression r in f.Decreases) {

-        Indent(2 * IndentAmount);

-        wr.Write("decreases ");

-        PrintExpression(r);

-        wr.WriteLine(";");

-      }

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

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

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

       if (f.Body != null) {

         Indent(IndentAmount);

         wr.WriteLine("{");

@@ -205,8 +190,9 @@ namespace Microsoft.Dafny {
       wr.WriteLine(method.Body == null ? ";" : ":");

       

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

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

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

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

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

       

       if (method.Body != null) {

         Indent(IndentAmount);

@@ -242,6 +228,15 @@ namespace Microsoft.Dafny {
       }

     }

 

+    void PrintSpecLine(string! kind, List<Expression!>! ee, int indent) {

+      if (ee.Count != 0) {

+        Indent(indent);

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

+        PrintExpressionList(ee);

+        wr.WriteLine(";");

+      }

+    }

+

     void PrintSpec(string! kind, List<MaybeFreeExpression!>! ee, int indent) {

       foreach (MaybeFreeExpression e in ee) {

         Indent(indent);

@@ -377,16 +372,7 @@ namespace Microsoft.Dafny {
 

         int ind = indent + IndentAmount;

         PrintSpec("invariant", s.Invariants, ind);

-        if (s.Decreases.Count != 0) {

-          Indent(indent);

-          string sep = "decreases ";

-          foreach (Expression e in s.Decreases) {

-            wr.Write(sep);

-            sep = ", ";

-            PrintExpression(e);

-          }

-          wr.WriteLine(";");

-        }

+        PrintSpecLine("decreases", s.Decreases, indent);

         Indent(indent);

         PrintStatement(s.Body, indent);

         

diff --git a/Dafny/Resolver.ssc b/Dafny/Resolver.ssc
index 8bbc1d29..d53bf450 100644
--- a/Dafny/Resolver.ssc
+++ b/Dafny/Resolver.ssc
@@ -343,6 +343,10 @@ namespace Microsoft.Dafny {
           Error(e, "a modifies-clause expression must denote an object or a collection of objects (instead got {0})", e.Type);

         }

       }

+      foreach (Expression e in m.Decreases) {

+        ResolveExpression(e, false);

+        // any type is fine

+      }

       

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

       foreach (Formal p in m.Outs) {

diff --git a/Dafny/Scanner.ssc b/Dafny/Scanner.ssc
index 921ef4f6..a1895c0c 100644
--- a/Dafny/Scanner.ssc
+++ b/Dafny/Scanner.ssc
@@ -286,14 +286,14 @@ public class Scanner {
 			case "free": t.kind = 19; break;

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

 			case "ensures": t.kind = 21; break;

-			case "bool": t.kind = 24; break;

-			case "int": t.kind = 25; break;

-			case "set": t.kind = 26; break;

-			case "seq": t.kind = 27; break;

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

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

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

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

+			case "decreases": t.kind = 22; break;

+			case "bool": t.kind = 25; break;

+			case "int": t.kind = 26; break;

+			case "set": t.kind = 27; break;

+			case "seq": t.kind = 28; break;

+			case "object": t.kind = 29; break;

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

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

 			case "match": t.kind = 33; break;

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

 			case "label": t.kind = 36; break;

@@ -366,9 +366,9 @@ public class Scanner {
 				if (ch == '=') {buf.Append(ch); NextCh(); goto case 31;}

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

 			case 12:

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

-			case 13:

 				{t.kind = 23; goto done;}

+			case 13:

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

 			case 14:

 				{t.kind = 32; goto done;}

 			case 15:

diff --git a/Dafny/Translator.ssc b/Dafny/Translator.ssc
index aef2ad9b..185a81ee 100644
--- a/Dafny/Translator.ssc
+++ b/Dafny/Translator.ssc
@@ -897,8 +897,9 @@ namespace Microsoft.Dafny {
         CheckWellformed(p, 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 the syntax is

-      // not rich enough for programmers to specify reads clauses and always being absolutely well-defined.

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

+      // be that the syntax was not rich enough for programmers to specify reads clauses and always being

+      // absolutely well-defined.

       // check well-formedness of the decreases clauses

       foreach (Expression p in f.Decreases) {

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

@@ -1153,58 +1154,15 @@ namespace Microsoft.Dafny {
           builder.Add(Assert(expr.tok, q, "insufficient reads clause to invoke function"));

   

           // finally, check that the decreases measure goes down

-          Bpl.Expr decrExpr;

-          int N = min{e.Function.Decreases.Count, func.Decreases.Count};

-          if (N != 0) {

-            // both functions have explicit decreases clauses, so use them

-            List<Type!> types = new List<Type!>();

-            List<Bpl.Expr!> calleeTotal = new List<Bpl.Expr!>();

-            List<Bpl.Expr!> callee = new List<Bpl.Expr!>();

-            List<Bpl.Expr!> caller = new List<Bpl.Expr!>();

-            for (int i = 0; i < N; i++) {

-              Expression e0 = Substitute(e.Function.Decreases[i], e.Receiver, substMap);

-              Expression e1 = func.Decreases[i];

-              if (!CompatibleDecreasesTypes((!)e0.Type, (!)e1.Type)) {

-                break;

-              }

-              types.Add(e0.Type);

-              calleeTotal.Add(IsTotal(e0, etran));

-              callee.Add(etran.TrExpr(e0));

-              caller.Add(etran.TrExpr(e1));

-            }

-            decrExpr = DecreasesCheck(expr.tok, types, calleeTotal, callee, caller, builder, etran, "");

-          } else {

-            // todo:  include totality checks for callee in this branch!

-            List<Expression!> d0 = null, d1 = null;

-            if (e.Function.Decreases.Count == 0) {

-              d0 = e.Function.Reads;  // use its reads clause instead

-            } else if (e.Function.Decreases[0].Type is SetType) {

-              d0 = new List<Expression!>(1);

-              d0.Add(e.Function.Decreases[0]);  // use the first component of the declared decreases clause

-            } else {

-              d0 = null;  // there is a declared decreases clause, but its first component has a type that is incomparable with a reads clause

-            }

-            if (func.Decreases.Count == 0) {

-              d1 = func.Reads;  // use its reads clause instead

-            } else if (func.Decreases[0].Type is SetType) {

-              d1 = new List<Expression!>(1);

-              d1.Add(func.Decreases[0]);  // use the first component of the declared decreases clause

-            } else {

-              d1 = null;  // there is a declared decreases clause, but its first component has a type that is incomparable with a reads clause

-            }

-            if (d0 == null || d1 == null) {

-              decrExpr = Bpl.Expr.False;

-            } else {

-              oVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$d", predef.RefType));

-              o = new Bpl.IdentifierExpr(expr.tok, oVar);

-              Bpl.Expr r0 = InRWClause(expr.tok, o, d0, etran, e.Receiver, substMap);

-              Bpl.Expr r1 = InRWClause(expr.tok, o, d1, etran, null, null);

-              Bpl.Expr qSubset = new Bpl.ForallExpr(expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(r0, r1));

-              Bpl.Expr qProper = new Bpl.ExistsExpr(expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.And(Bpl.Expr.Not(r0), r1));

-              decrExpr = Bpl.Expr.And(qSubset, qProper);

-            }

+          List<Expression!> contextDecreases = func.Decreases;

+          if (contextDecreases.Count == 0) {

+            contextDecreases = func.Reads;  // use its reads clause instead

           }

-          builder.Add(Assert(expr.tok, decrExpr, "failure to decrease termination measure"));

+          List<Expression!> calleeDecreases = e.Function.Decreases;

+          if (calleeDecreases.Count == 0) {

+            calleeDecreases = e.Function.Reads;  // use its reads clause instead

+          }

+          CheckCallTermination(expr.tok, contextDecreases, calleeDecreases, e.Receiver, substMap, etran, builder);

         }

       } else if (expr is DatatypeValue) {

         DatatypeValue dtv = (DatatypeValue)expr;

@@ -1775,7 +1733,28 @@ namespace Microsoft.Dafny {
             outs.Add(etran.TrExpr(e));

           }

         }

-        

+

+        if (currentMethod.Decreases.Count == 0 || exists{Expression e in currentMethod.Decreases; e is WildcardExpr}) {

+          // omit termination checking for calls in this context

+        } else {

+          // Check termination.  Ideally, this would be checked after the precondition check.        

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

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

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

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

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

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

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

+            substMap.Add(p, ie);

+            locals.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.UniqueName, TrType(local.Type))));

+            Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie);  // TODO: is this cast always justified?

+            Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.TrExpr(s.Args[i]));

+            builder.Add(cmd);

+          }

+          CheckCallTermination(stmt.Tok, currentMethod.Decreases, s.Method.Decreases, s.Receiver, substMap, etran, builder);

+        }

+

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

         builder.Add(call);

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

@@ -1918,6 +1897,7 @@ namespace Microsoft.Dafny {
           // time for the actual loop body

           TrStmt(s.Body, loopBodyBuilder, locals, etran);

           // check definedness of decreases expressions

+          List<Token!> toks = new List<Token!>();

           List<Type!> types = new List<Type!>();

           List<Bpl.Expr!> decrsTotal = new List<Bpl.Expr!>();

           List<Bpl.Expr!> decrs = new List<Bpl.Expr!>();

@@ -1925,11 +1905,12 @@ namespace Microsoft.Dafny {
             // The following totality check implies that the loop invariant stating the same property will hold;

             // thus, an alternative (perhaps preferable) design would be:  add the totality check also just before

             // the loop, and change the loop invariant to be free.

+            toks.Add(e.tok);

             types.Add((!)e.Type);

             decrsTotal.Add(IsTotal(e, etran));

             decrs.Add(etran.TrExpr(e));

           }

-          Bpl.Expr decrCheck = DecreasesCheck(stmt.Tok, types, decrsTotal, decrs, oldBfs, loopBodyBuilder, etran, "at end of loop iteration");

+          Bpl.Expr decrCheck = DecreasesCheck(toks, types, decrsTotal, decrs, oldBfs, loopBodyBuilder, etran, " at end of loop iteration");

           loopBodyBuilder.Add(Assert(stmt.Tok, decrCheck, "decreases expression might not decrease"));

         }

         Bpl.StmtList body = loopBodyBuilder.Collect(stmt.Tok);

@@ -2032,11 +2013,41 @@ namespace Microsoft.Dafny {
       }

     }

     

+    void CheckCallTermination(Token! tok, List<Expression!>! contextDecreases, List<Expression!>! calleeDecreases,

+                              Expression receiverReplacement, Dictionary<IVariable,Expression!>! substMap,

+                              ExpressionTranslator! etran, Bpl.StmtListBuilder! builder)

+    {

+      if (exists{Expression e in contextDecreases; e is WildcardExpr}) {

+        // omit termination checking for calls in this context

+        return;

+      }

+      int N = min{contextDecreases.Count, calleeDecreases.Count};

+      List<Token!> toks = new List<Token!>();

+      List<Type!> types = new List<Type!>();

+      List<Bpl.Expr!> calleeTotal = new List<Bpl.Expr!>();

+      List<Bpl.Expr!> callee = new List<Bpl.Expr!>();

+      List<Bpl.Expr!> caller = new List<Bpl.Expr!>();

+      for (int i = 0; i < N; i++) {

+        Expression e0 = Substitute(calleeDecreases[i], receiverReplacement, substMap);

+        Expression e1 = contextDecreases[i];

+        if (!CompatibleDecreasesTypes((!)e0.Type, (!)e1.Type)) {

+          break;

+        }

+        toks.Add(tok);

+        types.Add(e0.Type);

+        calleeTotal.Add(IsTotal(e0, etran));

+        callee.Add(etran.TrExpr(e0));

+        caller.Add(etran.TrExpr(e1));

+      }

+      Bpl.Expr decrExpr = DecreasesCheck(toks, types, calleeTotal, callee, caller, builder, etran, "");

+      builder.Add(Assert(tok, decrExpr, "failure to decrease termination measure"));

+    }

+    

     /// <summary>

     /// Returns the expression that says whether or not the decreases function has gone down.  ee0 represents the new

     /// values and ee1 represents old values.

     /// </summary>

-    Bpl.Expr! DecreasesCheck(Token! tok, List<Type!>! types, List<Bpl.Expr!>! total0, List<Bpl.Expr!>! ee0, List<Bpl.Expr!>! ee1,

+    Bpl.Expr! DecreasesCheck(List<Token!>! toks, List<Type!>! types, List<Bpl.Expr!>! total0, List<Bpl.Expr!>! ee0, List<Bpl.Expr!>! ee1,

                              Bpl.StmtListBuilder! builder, ExpressionTranslator! etran, string! suffixMsg)

       requires predef != null;

       requires types.Count == ee0.Count && ee0.Count == ee1.Count;

@@ -2048,7 +2059,7 @@ namespace Microsoft.Dafny {
       List<Bpl.Expr!> Less = new List<Bpl.Expr!>(N);

       for (int i = 0; i < N; i++) {

         Bpl.Expr! less, eq;

-        ComputeLessEq(tok, types[i], ee0[i], ee1[i], out less, out eq, etran);

+        ComputeLessEq(toks[i], types[i], ee0[i], ee1[i], out less, out eq, etran);

         Eq.Add(eq);

         Less.Add(less);

       }

@@ -2060,12 +2071,13 @@ namespace Microsoft.Dafny {
       // more precisely, for component k of the lexicographic decreases function, check:

       //   ee0[0] < ee1[0] || ee0[1] < ee1[1] || ... || ee0[k-1] < ee1[k-1] || ee0[k] == ee1[k] || 0 <= ee1[k]

       for (int k = 0; k < N; k++) {

-        // we only need to check lower bound for integers--sets, sequences, booleans, and references all have natural lower bounds

+        // we only need to check lower bound for integers--sets, sequences, booleans, references, and datatypes all have natural lower bounds

         Bpl.Expr prefixIsLess = Bpl.Expr.False;

         for (int i = 0; i < k; i++) {

           prefixIsLess = Bpl.Expr.Or(prefixIsLess, Less[i]);

         }

-        Bpl.Cmd cmd = Assert(ee0[k].tok, Bpl.Expr.Or(prefixIsLess, total0[k]), "decreases expression (component " + k + ") must be well-defined" + suffixMsg);

+        string component = N == 1 ? "" : " (component " + k + ")";

+        Bpl.Cmd cmd = Assert(toks[k], Bpl.Expr.Or(prefixIsLess, total0[k]), "decreases expression" + component + " must be well-defined" + suffixMsg);

         builder.Add(cmd);

         

         if (types[k] is IntType) {

@@ -2073,7 +2085,7 @@ namespace Microsoft.Dafny {
           for (int i = 0; i < k; i++) {

             bounded = Bpl.Expr.Or(bounded, Less[i]);

           }

-          cmd = Assert(ee0[k].tok, Bpl.Expr.Or(bounded, Eq[k]), "decreases expression (component " + k + ") must be bounded below by 0" + suffixMsg);

+          cmd = Assert(toks[k], Bpl.Expr.Or(bounded, Eq[k]), "decreases expression" + component + " must be bounded below by 0" + suffixMsg);

           builder.Add(cmd);

         }

       }

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 540bcb4b..95302b05 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -8,8 +8,7 @@ class MyClass<T, U> {
   method M(s: bool, lotsaObjects: set<object>)

       returns (t: object, u: set<int>, v: seq<MyClass<bool,U>>):

     requires s;

-    modifies this;

-    modifies lotsaObjects;

+    modifies this, lotsaObjects;

     ensures t == t;

     ensures old(null) != this;

   {

@@ -195,3 +194,7 @@ Dafny program verifier finished with 7 verified, 0 errors
 -------------------- SumOfCubes.dfy --------------------

 

 Dafny program verifier finished with 10 verified, 0 errors

+

+-------------------- TerminationDemos.dfy --------------------

+

+Dafny program verifier finished with 7 verified, 0 errors

diff --git a/Test/dafny0/BinaryTree.dfy b/Test/dafny0/BinaryTree.dfy
index 54a98a56..5f56cf40 100644
--- a/Test/dafny0/BinaryTree.dfy
+++ b/Test/dafny0/BinaryTree.dfy
@@ -1,6 +1,6 @@
 class IntSet {

-  var contents: set<int>;

-  var footprint: set<object>;

+  ghost var contents: set<int>;

+  ghost var footprint: set<object>;

 

   var root: Node;

 

@@ -48,7 +48,7 @@ class IntSet {
     footprint := root.footprint + {this};

   }

 

-  method InsertHelper(x: int, n: Node) returns (m: Node)

+  class method InsertHelper(x: int, n: Node) returns (m: Node)

     requires n == null || n.Valid();

     modifies n.footprint;

     ensures m != null && m.Valid();

@@ -97,9 +97,9 @@ class IntSet {
 }

 

 class Node {

-  var contents: set<int>;

-  var footprint: set<object>;

-  

+  ghost var contents: set<int>;

+  ghost var footprint: set<object>;

+

   var data: int;

   var left: Node;

   var right: Node;

diff --git a/Test/dafny0/TerminationDemos.dfy b/Test/dafny0/TerminationDemos.dfy
new file mode 100644
index 00000000..6b63bfec
--- /dev/null
+++ b/Test/dafny0/TerminationDemos.dfy
@@ -0,0 +1,80 @@
+class Example {

+  method M(n: int)

+  {

+    var i := 0;

+    while (i < n)

+      decreases n - i;

+    {

+      i := i + 1;

+    }

+  }

+}

+

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

+

+class Fibonacci {

+  function Fib(n: int): int

+    decreases n;

+  {

+    if n < 2 then n else Fib(n-2) + Fib(n-1)

+  }

+}

+

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

+

+class Ackermann {

+  function F(m: int, n: int): int

+    decreases m, n;

+  {

+    if m <= 0 then

+      n + 1

+    else if n <= 0 then

+      F(m - 1, 1)

+    else

+      F(m - 1, F(m, n - 1))

+  }

+}

+

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

+

+class List {

+  var data: int;

+  var next: List;

+  ghost var ListNodes: set<List>;

+  function IsAcyclic(): bool

+    reads *;

+    decreases ListNodes;

+  {

+    this in ListNodes &&

+    (next != null ==>

+      next.ListNodes <= ListNodes && this !in next.ListNodes &&

+      next.IsAcyclic())

+  }

+

+  method Singleton(x: int) returns (list: List)

+    ensures list != null && list.IsAcyclic();

+  {

+    list := new List;

+    list.data := x;

+    list.next := null;

+    list.ListNodes := {list};

+  }

+

+  method Prepend(x: int, tail: List) returns (list: List)

+    requires tail == null || tail.IsAcyclic();

+    ensures list != null && list.IsAcyclic();

+  {

+    list := new List;

+    list.data := x;

+    list.next := tail;

+    list.ListNodes := if tail == null then {list} else {list} + tail.ListNodes;

+  }

+

+  function Sum(): int

+    requires IsAcyclic();

+    reads *;

+    decreases ListNodes;

+  {

+    if next == null then data else data + next.Sum()

+  }

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 64efe27b..c1837b43 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -21,7 +21,7 @@ for %%f in (TypeTests.dfy SmallTests.dfy Queue.dfy ListCopy.dfy
             BinaryTree.dfy ListReverse.dfy ListContents.dfy

             SchorrWaite.dfy Termination.dfy Use.dfy DTypes.dfy

             TypeParameters.dfy Datatypes.dfy UnboundedStack.dfy

-            SumOfCubes.dfy) do (

+            SumOfCubes.dfy TerminationDemos.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% %* %%f