From the JMLRefMan:
Many, but not all, of the JML additions to Java's modifiers (see section
6.2 Modifiers) are level 0 features. The following modifiers are included
in level 0.
The modifier spec_public (see section 6.2.2 Spec Public).
The modifier spec_protected (see section 6.2.3 Spec Protected).
The modifier instance (see section 6.2.7 Instance).
The modifier model (see section 6.2.5 Model), as applied to field
declarations (see section 7.1.2.1 JML Modifiers for Fields). Note that
this
modifier as applied to other declarations is not a level 0 feature.
The modifier ghost (see section 6.2.6 Ghost), as applied to both field and
variable declarations (see section 7.1.2 Field and Variable Declarations).
The modifier helper (see section 6.2.8 Helper).
Implemented Typechecking for invariants. Added rule for static and instance, besides public/protected/private invariants type checking. Also added synthesized rules for all Level 0 modifiers
This needs more work along the way, I implemented modifiers typechecking for invariants. need to modify for any construct that has modifiers.
This thing to do isn't clear. Can you please proved more
information and/or an example?
this task needs more work when other clauses that accept modifiers are implemented