Added test cases and fixes for overrides termination checks

Removed syntactic presence checks for specifications--these will be checked semantically by the verifier

6 files changed, 210 insertions, 71 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index bf417de7..727011e8 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2952,25 +2952,6 @@ namespace Microsoft.Dafny
                             classMethod.OverriddenMethod = traitMethod;

                             //adding a call graph edge from the trait method to that of class

                             cl.Module.CallGraph.AddEdge(traitMethod, classMethod);

-

-                            //checking specifications

-                            //class method must provide its own specifications in case the overriden method has provided any

-                            if ((classMethod.Req == null || classMethod.Req.Count == 0) && (classMethod.OverriddenMethod.Req != null && classMethod.OverriddenMethod.Req.Count > 0))  //it means m.OverriddenMethod.Req =>  m.Req

-                            {

-                                Error(classMethod, "Method must provide its own Requires clauses anew");

-                            }

-                            if ((classMethod.Ens == null || classMethod.Ens.Count == 0) && (classMethod.OverriddenMethod.Ens != null && classMethod.OverriddenMethod.Ens.Count > 0))  //it means m.OverriddenMethod.Ens =>  m.Ens

-                            {

-                                Error(classMethod, "Method must provide its own Ensures clauses anew");

-                            }

-                            if ((classMethod.Mod == null || classMethod.Mod.Expressions == null || classMethod.Mod.Expressions.Count == 0) && (classMethod.OverriddenMethod.Mod != null && classMethod.OverriddenMethod.Mod.Expressions != null && classMethod.OverriddenMethod.Mod.Expressions.Count > 0))  //it means m.OverriddenMethod.Mod =>  m.Mod

-                            {

-                                Error(classMethod, "Method must provide its own Modifies clauses anew");

-                            }

-                            if ((classMethod.Decreases == null || classMethod.Decreases.Expressions == null || classMethod.Decreases.Expressions.Count == 0) && (classMethod.OverriddenMethod.Decreases != null && classMethod.OverriddenMethod.Decreases.Expressions != null && classMethod.OverriddenMethod.Decreases.Expressions.Count > 0))  //it means m.OverriddenMethod.Decreases =>  m.Decreases

-                            {

-                                Error(classMethod, "Method must provide its own Decreases clauses anew");

-                            }

                         }

                     }

                     else if (traitMem.Value is Function)

@@ -2985,25 +2966,6 @@ namespace Microsoft.Dafny
                             classFunction.OverriddenFunction = traitFunction;

                             //adding a call graph edge from the trait function to that of class

                             cl.Module.CallGraph.AddEdge(traitFunction, classFunction);

-

-                            //checking specifications

-                            //class function must provide its own specifications in case the overriden function has provided any

-                            if ((classFunction.Req == null || classFunction.Req.Count == 0) && (classFunction.OverriddenFunction.Req != null && classFunction.OverriddenFunction.Req.Count > 0))  //it means m.OverriddenMethod.Req =>  m.Req

-                            {

-                                Error(classFunction, "Function must provide its own Requires clauses anew");

-                            }

-                            if ((classFunction.Ens == null || classFunction.Ens.Count == 0) && (classFunction.OverriddenFunction.Ens != null && classFunction.OverriddenFunction.Ens.Count > 0))  //it means m.OverriddenMethod.Ens =>  m.Ens

-                            {

-                                Error(classFunction, "Function must provide its own Ensures clauses anew");

-                            }

-                            if ((classFunction.Reads == null || classFunction.Reads.Count == 0) && (classFunction.OverriddenFunction.Reads != null && classFunction.OverriddenFunction.Reads.Count > 0))  //it means m.OverriddenMethod.Mod =>  m.Mod

-                            {

-                                Error(classFunction, "Function must provide its own Reads clauses anew");

-                            }

-                            if ((classFunction.Decreases == null || classFunction.Decreases.Expressions == null || classFunction.Decreases.Expressions.Count == 0) && (classFunction.OverriddenFunction.Decreases != null && classFunction.OverriddenFunction.Decreases.Expressions != null && classFunction.OverriddenFunction.Decreases.Expressions.Count > 0))  //it means m.OverriddenMethod.Decreases =>  m.Decreases

-                            {

-                                Error(classFunction, "Function must provide its own Decreases clauses anew");

-                            }

                         }

                     }

                     else if (traitMem.Value is Field)

@@ -3058,6 +3020,11 @@ namespace Microsoft.Dafny
                         {

                             Method classMethod = (Method)classMem;

                             refinementTransformer.CheckOverride_MethodParameters(classMethod, traitMethod);

+                            var traitMethodAllowsNonTermination = Contract.Exists(traitMethod.Decreases.Expressions, e => e is WildcardExpr);

+                            var classMethodAllowsNonTermination = Contract.Exists(classMethod.Decreases.Expressions, e => e is WildcardExpr);

+                            if (classMethodAllowsNonTermination && !traitMethodAllowsNonTermination) {

+                              Error(classMethod.tok, "not allowed to override a terminating method with a possibly non-terminating method ('{0}')", classMethod.Name);

+                            }

                         }

                         if (!cl.Module.IsAbstract && traitMethod.Body == null && classMem == null)

                             Error(cl, "class: {0} does not implement trait member: {1}", cl.CompileName, traitMethod.CompileName);

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 96405daf..8678e2c3 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -3405,33 +3405,68 @@ namespace Microsoft.Dafny {
         }

     }

 

-    private void AddMethodOverrideTerminationChk(Method m, Bpl.StmtListBuilder builder, ExpressionTranslator etran, Dictionary<IVariable, Expression> substMap)

-    {

-        var decrToks = new List<IToken>();

-        var decrTypes1 = new List<Type>();

-        var decrTypes2 = new List<Type>();

-        var decrClass = new List<Expr>();

-        var decrTrait = new List<Expr>();

-        if (m.Decreases != null)

-        {

-            foreach (var decC in m.Decreases.Expressions)

-            {

-                decrToks.Add(decC.tok);

-                decrTypes1.Add(decC.Type);

-                decrClass.Add(etran.TrExpr(decC));

-            }

-        }

-        if (m.OverriddenMethod.Decreases != null)

-        {

-            foreach (var decT in m.OverriddenMethod.Decreases.Expressions)

-            {

-                var decCNew = Substitute(decT, null, substMap);

-                decrTypes2.Add(decCNew.Type);

-                decrTrait.Add(etran.TrExpr(decCNew));

-            }

+    private void AddMethodOverrideTerminationChk(Method m, Bpl.StmtListBuilder builder, ExpressionTranslator etran, Dictionary<IVariable, Expression> substMap) {

+      Contract.Requires(m != null);

+      Contract.Requires(builder != null);

+      Contract.Requires(etran != null);

+      Contract.Requires(substMap != null);

+      // Note, it is as if the trait's method is calling the class's method.

+      var contextDecreases = m.OverriddenMethod.Decreases.Expressions;

+      var calleeDecreases = m.Decreases.Expressions;

+      // We want to check:  calleeDecreases <= contextDecreases (note, we can allow equality, since there is a bounded, namely 1, number of dynamic dispatches)

+      if (Contract.Exists(contextDecreases, e => e is WildcardExpr)) {

+        // no check needed

+        return;

+      }

+

+      int N = Math.Min(contextDecreases.Count, calleeDecreases.Count);

+      var toks = new List<IToken>();

+      var types0 = new List<Type>();

+      var types1 = new List<Type>();

+      var callee = new List<Expr>();

+      var caller = new List<Expr>();

+

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

+        Expression e0 = calleeDecreases[i];

+        Expression e1 = Substitute(contextDecreases[i], null, substMap);

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

+          N = i;

+          break;

         }

-        var decrChk = DecreasesCheck(decrToks, decrTypes1, decrTypes2, decrClass, decrTrait, null, null, true, false);

-        builder.Add(new Bpl.AssertCmd(m.tok, decrChk));

+        toks.Add(new NestedToken(m.tok, e1.tok));

+        types0.Add(e0.Type.NormalizeExpand());

+        types1.Add(e1.Type.NormalizeExpand());

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

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

+      }

+

+      var decrCountT = contextDecreases.Count;

+      var decrCountC = calleeDecreases.Count;

+      // Generally, we want to produce a check "decrClass <= decrTrait", allowing (the common case where) they are equal.

+      // * If N < decrCountC && N < decrCountT, then "decrClass <= decrTrait" if the comparison ever gets beyond the

+      //   parts that survived truncation.  Thus, we compare with "allowNoChange" set to "false".

+      // Otherwise:

+      // * If decrCountC == decrCountT, then the truncation we did above had no effect and we pass in "allowNoChange" as "true".

+      // * If decrCountC > decrCountT, then we will have truncated decrClass above.  Let x,y and x' denote decrClass and

+      //   decrTrait, respectively, where x and x' have the same length.  Considering how Dafny in effect pads the end of

+      //   decreases tuples with a \top, we were supposed to evaluate (x,(y,\top)) <= (x',\top), which by lexicographic pairs

+      //   we can expand to:

+      //       x <= x' && (x == x' ==> (y,\top) <= \top)

+      //   which is equivalent to just x <= x'.  Thus, we called DecreasesCheck to compare x and x' and we pass in "allowNoChange"

+      //   as "true".

+      // * If decrCountC < decrCountT, then we will have truncated decrTrait above.  Let x and x',y' denote decrClass and

+      //   decrTrait, respectively, where x and x' have the same length.  We then want to check (x,\top) <= (x',(y',\top)), which

+      //   expands to:

+      //       x <= x' && (x == x' ==> \top <= (y',\top))

+      //    =      { \top is strictly larger than a pair }

+      //       x <= x' && (x == x' ==> false)

+      //    =

+      //       x < x'

+      //   So we perform our desired check by calling DecreasesCheck to strictly compare x and x', so we pass in "allowNoChange"

+      //   as "false".

+      bool allowNoChange = N == decrCountT && decrCountT <= decrCountC;

+      var decrChk = DecreasesCheck(toks, types0, types1, callee, caller, null, null, allowNoChange, false);

+      builder.Add(Assert(m.tok, decrChk, "method's decreases clause must be below or equal to that in the trait"));

     }

 

     private void AddMethodOverrideSubsetChk(Method m, Bpl.StmtListBuilder builder, ExpressionTranslator etran, List<Variable> localVariables, Dictionary<IVariable, Expression> substMap)

diff --git a/Test/dafny0/Trait/TraitSpecsOverride0.dfy b/Test/dafny0/Trait/TraitSpecsOverride0.dfy
index 614adc2d..7e16c630 100644
--- a/Test/dafny0/Trait/TraitSpecsOverride0.dfy
+++ b/Test/dafny0/Trait/TraitSpecsOverride0.dfy
@@ -7,6 +7,7 @@ trait J
 	function method F(k:int, y: array<int>): int

 	  reads y;

 	  decreases k;

+	  ensures F(k, y) < 100

 	

 	function method G(y: int): int 

 	{ 

@@ -36,12 +37,14 @@ trait J
 

 class C extends J 

 {

+	// F's postcondition (true) is too weak, but that won't be detected until verification time

 	function method F(kk:int, yy: array<int>): int

 	{ 

 	  200 

 	}

 

-	method M(kk:int) returns (ksos:int) //errors here, M must provide its own specifications

+	// M's postcondition (true) is too weak, but that won't be detected until verification time

+	method M(kk:int) returns (ksos:int)

 	{

 		ksos:=10;	

 	}

@@ -56,4 +59,16 @@ class C extends J
 	    y1[0] := a1 + b1;

             c1 := a1 + b1;

         }	

-}
\ No newline at end of file
+}

+

+module BadNonTermination {

+  trait TT1 {

+    method N(x: int)

+      decreases x

+  }

+  class CC1 extends TT1 {

+    method N(x: int)

+      decreases *  // error: can't override a terminating method with a possibly non-terminating method

+    { }

+  }

+}

diff --git a/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect b/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect
index 750e13e0..2281c604 100644
--- a/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect
+++ b/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect
@@ -1,5 +1,2 @@
-TraitSpecsOverride0.dfy(39,17): Error: Function must provide its own Reads clauses anew

-TraitSpecsOverride0.dfy(39,17): Error: Function must provide its own Decreases clauses anew

-TraitSpecsOverride0.dfy(44,8): Error: Method must provide its own Requires clauses anew

-TraitSpecsOverride0.dfy(44,8): Error: Method must provide its own Ensures clauses anew

-4 resolution/type errors detected in TraitSpecsOverride0.dfy

+TraitSpecsOverride0.dfy(70,11): Error: not allowed to override a terminating method with a possibly non-terminating method ('N')

+1 resolution/type errors detected in TraitSpecsOverride0.dfy

diff --git a/Test/dafny0/Trait/TraitsDecreases.dfy b/Test/dafny0/Trait/TraitsDecreases.dfy
new file mode 100644
index 00000000..53ce28be
--- /dev/null
+++ b/Test/dafny0/Trait/TraitsDecreases.dfy
@@ -0,0 +1,108 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+trait Trait {

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

+  method A0(x: nat)

+  // default decreases: x

+  method A1(x: nat)

+  // default decreases: x

+  method A2(x: nat)

+    decreases x

+  method A3(x: nat)

+    decreases x

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

+  method G0(x: nat, y: bool)

+    decreases x, y

+  method G1(x: nat, y: bool)

+    decreases x+1, y

+  method G2(x: nat, y: bool)

+    decreases x

+  method G3(x: nat, y: bool)

+    decreases x+1, y

+  method G4(x: nat, y: bool)

+    decreases y, x

+  method G5(x: nat, y: bool)

+    decreases y, x

+  method G6(x: nat, y: bool)

+    decreases true, x

+  method G7(x: nat, y: bool)

+    decreases false, x

+  method G8(x: nat, y: bool)

+    requires x < 100

+    decreases 120, y

+  method G9(x: nat, y: bool)

+    requires x < 100

+    decreases 120, y

+  method G10(x: nat, y: bool)

+    requires x < 100

+    decreases x, y

+}

+

+class Class extends Trait {

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

+  method A0(x: nat)

+  // default decreases: x

+  { }

+  method A1(x: nat)

+    decreases x

+  { }

+  method A2(x: nat)

+  // default decreases: x

+  { }

+  method A3(x: nat)

+    decreases x

+  { }

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

+  method G0(x: nat, y: bool)

+    decreases y, x  // error: opposite order from default

+  { }

+  method G1(x: nat, y: bool)

+    decreases x, x  // fine -- it's below the one in the trait

+  { }

+  method G2(x: nat, y: bool)  // fine -- (x,y) is below the trait's (x,\top)

+  // default decreases: x, y

+  { }

+  method G3(x: nat, y: bool)

+    decreases x, y  // fine -- trait decrease is above this one

+  { }

+  method G4(x: nat, y: bool)

+    decreases y, x+1  // error: this decreases is above the trait's decreases

+  { }

+  method G5(x: nat, y: bool)

+    decreases y  // error: this is above the trait's decreases clause

+  { }

+  method G6(x: nat, y: bool)

+    decreases y, x  // good -- this is the same or below the one in the trait

+  { }

+  method G7(x: nat, y: bool)

+    decreases y, x  // error: this might be above the one in the trait

+  { }

+  method G8(x: nat, y: bool)

+    decreases x, y  // fine -- given the precondition in the trait, this is below the one in the trait

+  { }

+  method G9(x: nat, y: bool)

+    requires x < 105

+    decreases 120, y  // fine -- given the precondition in the trait, this is below the one in the trait

+  { }

+  method G10(x: nat, y: bool)

+    requires x < 100

+    decreases 120, y  // error: this is above the one in the trait

+  { }

+}

+

+

+trait TT {

+  method M(x: int)

+    decreases *

+  method P(x: int)

+    decreases *

+}

+class CC extends TT {

+  method M(x: int)

+    decreases x

+  { }

+  method P(x: int)

+    decreases *

+  { }

+}

diff --git a/Test/dafny0/Trait/TraitsDecreases.dfy.expect b/Test/dafny0/Trait/TraitsDecreases.dfy.expect
new file mode 100644
index 00000000..6c76f9a8
--- /dev/null
+++ b/Test/dafny0/Trait/TraitsDecreases.dfy.expect
@@ -0,0 +1,17 @@
+TraitsDecreases.dfy(57,10): Error: method's decreases clause must be below or equal to that in the trait

+Execution trace:

+    (0,0): anon0

+TraitsDecreases.dfy(69,10): Error: method's decreases clause must be below or equal to that in the trait

+Execution trace:

+    (0,0): anon0

+TraitsDecreases.dfy(72,10): Error: method's decreases clause must be below or equal to that in the trait

+Execution trace:

+    (0,0): anon0

+TraitsDecreases.dfy(78,10): Error: method's decreases clause must be below or equal to that in the trait

+Execution trace:

+    (0,0): anon0

+TraitsDecreases.dfy(88,10): Error: method's decreases clause must be below or equal to that in the trait

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 63 verified, 5 errors