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
|
public class Enumerations {
// All enumeration instances are interned; there should be no need for
// an annotation.
enum StudentYear {
FRESHMAN,
SOPHOMORE,
JUNIOR,
SENIOR;
// check that receiver is OK
@org.checkerframework.dataflow.qual.Pure
public String toString() {
return "StudentYear: ...";
}
}
public boolean isSophomore(StudentYear sy) {
return sy == StudentYear.SOPHOMORE;
}
public boolean flow(StudentYear s) {
StudentYear m = StudentYear.SOPHOMORE;
return s == m;
}
StudentYear cast(Object o) {
return (StudentYear) o;
}
}
|
