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
|
import org.checkerframework.common.value.qual.*;
public class EnumValue {
enum Direction {
NORTH,
WEST,
SOUTH,
EAST
};
public enum Color {
BLUE,
RED,
GREEN
};
private enum Fruit {
APPLE,
ORANGE,
PEAR
};
void simpleTest() {
Direction @ArrayLen(4) [] myCompass = Direction.values();
Color @ArrayLen(3) [] myColors = Color.values();
Fruit @ArrayLen(3) [] myFruitBasket = Fruit.values();
// :: error: (assignment.type.incompatible)
Direction @ArrayLen(7) [] badCompass = Direction.values();
// :: error: (assignment.type.incompatible)
Color @ArrayLen(4) [] badColors = Color.values();
// :: error: (assignment.type.incompatible)
Fruit @ArrayLen(2) [] badFruit = Fruit.values();
}
public enum AdvDirection {
ANORTH {
public AdvDirection getOpposite() {
return ASOUTH;
}
},
AEAST {
public AdvDirection getOpposite() {
return AWEST;
}
},
ASOUTH {
public AdvDirection getOpposite() {
return ANORTH;
}
},
AWEST {
public AdvDirection getOpposite() {
return AEAST;
}
};
public abstract AdvDirection getOpposite();
}
void advTest() {
AdvDirection @ArrayLen(4) [] myCompass = AdvDirection.values();
// :: error: (assignment.type.incompatible)
AdvDirection @ArrayLen(3) [] badCompass = AdvDirection.values();
// :: error: (assignment.type.incompatible)
AdvDirection @ArrayLen(5) [] badCompass2 = AdvDirection.values();
}
}
|
