D. Modifier Summary

This table summarizes which Java and JML modifiers may be used in various grammatical contexts.

Grammatical construct		Java modifiers		JML modifiers
All modifiers		public protected private abstract static final synchronized transient volatile native strictfp		spec_public spec_protected model ghost pure instance helper non_null nullable nullable_by_default monitored uninitialized
Class declaration		public final abstract strictfp		pure model nullable_by_default spec_public spec_protected
Interface declaration		public strictfp		pure model nullable_by_default spec_public spec_protected
Nested Class declaration		public protected private static final abstract strictfp		spec_public spec_protected model pure
Nested interface declaration		public protected private static strictfp		spec_public spec_protected model pure
Local Class (and local model class) declaration		final abstract strictfp		pure model
Type specification (e.g. invariant)		public protected private static		instance
Field declaration		public protected private final volatile transient static		spec_public spec_protected non_null nullable instance monitored
Ghost Field declaration		public protected private static final		non_null nullable instance monitored
Model Field declaration		public protected private static		non_null nullable instance
Method declaration in a class		public protected private abstract final static synchronized native strictfp		spec_public spec_protected pure non_null nullable helper extract
Method declaration in an interface		public abstract		spec_public spec_protected pure non_null nullable helper
Constructor declaration		public protected private		spec_public spec_protected helper pure extract
Model method (in a class or interface)		public protected private abstract static final synchronized strictfp		pure non_null nullable helper extract
Model constructor		public protected private		pure helper extract
Java initialization block		static		-
JML initializer and static_initializer annotation		-		-
Formal parameter		final		non_null nullable
Local variable and local ghost variable declaration		final		ghost non_null nullable uninitialized

Note that within interfaces, fields are implicitly public, static and final [Gosling-etal00]. In an interface, ghost and model fields are implicitly public and static, though they may be declared as instance fields, which makes them not static.

Also within an interface, methods may not be static and are implicitly abstract. Model methods in interfaces, however, are not implicitly abstract and may be declared static.