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
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
|
// 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 *
{ }
}
// The following module contains various regression tests
module More {
trait A0 {
predicate P() decreases 5
}
class B0 extends A0 {
predicate P() // error: rank is not lower
}
trait A1 {
predicate P() decreases 5
}
class B1 extends A1 {
predicate P() reads this // error: rank is not lower
}
trait A2 {
predicate P(x: int)
}
class B2 extends A2 {
predicate P(x: int) reads this // error: rank is not lower
}
trait A3 {
predicate P() reads this
}
class B3 extends A3 {
predicate P() // error: rank is not lower
}
trait A4 {
predicate P(x: int) decreases 5
}
class B4 extends A4 {
predicate P(x: int) // error: rank is not lower
}
trait A5 {
method M(x: int) decreases 5
}
class B5 extends A5 {
method M(x: int) // error: rank is not lower
}
}
|
