1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
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 *
{ }
}
|
