Next: Method specifications, Previous: Java Member Declarations, Up: Class and Interface Specifications
Every class file can contain a list of attributes containing annotations that describe the behaviour of the class or interface in the file. The annotations that BML allows here are a subset of the annotations JML provides to specify classes and interfaces. The syntax of these bml-declarations is as follows.
bml-declaration ::= invariant
| history-constraint
| represents-decl
| initially-clause
Each of these declarations can be decorated with several modifiers, added as access flags to the attributes describing the decorations. Notice that BML only supports the functional version of the represent clause. The semantics of these keywords is the same as described in