Curtis Clifton
-
2009-06-05
- priority: 5 --> 7
From the JML Ref Manual:
The ability to use a .spec file (see section 16.1 File Name Suffixes) to give a separate specification for a compilation unit that only appears in binary form (e.g., in a .class file) is a level 0 feature. Use of the refine-prefix (see section 16. Refinement) is a level 1 feature.