Added test cases and fixes for overrides termination checks

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

4 files changed, 144 insertions, 7 deletions

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