[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

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.


[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

This document was generated by U-leavens-nd\leavens on May, 31 2013 using texi2html