Previous: Class and Interface Behaviour, Up: Class and Interface Specifications
BML allows one to write both lightweight and heavyweight
specifications. A single method can be annotated with several
specifications. If so, these specifications can be desugared into a
single heavyweight behavior specification; see
[Raghavan-Leavens05] for a description of the desugaring
algorithm. Typically such an algorithm will be applied at the level of
the compilation from JML to BML as there is only one pre-, post-condition
pair in the BML specifications.
The syntax and semantics for BML method specifications follows the one of JML (see Section 9.4 to Section 9.9 of the JML Reference Manual). As in JML, heavyweight specifications can contain a special access flag, to specify the visibility of the method specification. BML also follows JML for the definition of default specification clauses.
The following specification-clauses are supported by BML:
Adding more specification clauses to BML is not too complicated: they should be treated exactly the same as they are treated at source code level, for their JML counterparts.