diff options
| author |  leino <unknown> | 2015-04-03 21:44:11 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-04-03 21:44:11 -0700 |
| commit | 9c8ad44b64373fb9d85aef5a05809e8e25416684 (patch) | |
| tree | b1e03bd6ac48c26e659bebe1e56180d34b8fcc8a /Test/dafny0/Trait/TraitsDecreases.dfy | |
| parent | 8a332057c2c9fc76e5fb112d430404d1aa47ea0d (diff) | |
Added test cases and fixes for overrides termination checks
Removed syntactic presence checks for specifications--these will be checked semantically by the verifier
Diffstat (limited to 'Test/dafny0/Trait/TraitsDecreases.dfy')
| -rw-r--r-- | Test/dafny0/Trait/TraitsDecreases.dfy | 108 |
1 files changed, 108 insertions, 0 deletions
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 *
+ { }
+}
|