| 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; |
| } |
| } |