[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This table summarizes which Java and JML modifiers may be used in various grammatical contexts.
Grammatical construct | Java modifiers | JML modifiers | ||
All modifiers | | | ||
Class declaration | | | ||
Interface declaration | | | ||
Nested Class declaration | | | ||
Nested interface declaration | | | ||
Local Class (and local model class) declaration | | | ||
Type specification (e.g. invariant) | | | ||
Field declaration | | | ||
Ghost Field declaration | | | ||
Model Field declaration | | | ||
Method declaration in a class | | | ||
Method declaration in an interface | | | ||
Constructor declaration | | | ||
Model method (in a class or interface) | | | ||
Model constructor | | | ||
Java initialization block | | - | ||
JML initializer and static_initializer annotation | - | - | ||
Formal parameter | | | ||
Local variable and local ghost variable declaration | | |
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.