Next: Method Specifications, Previous: Class Member Declarations, Up: Class and Interface Specifications
Every class file can annotations that specify the behaviour of the class or interface in the file (see Class Attributes). The annotations that BML supports 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
[AS 28052008: initially and represents clauses not in grammar.] [AS 28052008: shoudn't we add modifiers in front of these.]
Each of these declarations can be decorated with several modifiers, added as access flags to the attributes describing the annotations.
Invariants are properties that have to hold in all visible states, while constraints specify a relationship that should hold for the combination of each visible state and any visible state that occurs later in the program's execution. Initially clauses describe the initial relation between various elements of the class. They are supposed to hold just after the appropriate initializer is finished: class static initializers for static clauses and constructors for instance clauses. Represents clauses describe what is represented by a given model field. Notice that BML only supports the functional version of the represents clause. The semantics of these keywords is the same as described in