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

B. 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 Werner M. Dietl on July, 21 2008 using texi2html 1.78.