BML allows one to write both lightweight and heavyweight
specifications. A single method can be annotated with several flat
specification cases, i.e., sequences of method specification
cases. At source code level, these specification cases are joined by
also keyword, whereas at bytecode level, each method is
annotated with a list of specification cases. If necessary, these
specifications can be desugared into a single heavyweight
behavior specification; see [Raghavan-Leavens05] for a
description of the desugaring algorithm. We leave the choice whether
this is necessary to tool builders; we only remark that the
specification desugaring algorithm at bytecode level essentially works
the same as at source code level.
However, at source code level, method specifications can be nested, i.e., they can be of the form:
where GenSpecCase can be a nested specification again. Fortunately, there is a simple desugaring for such specifications into a sequence of flat specification cases:
For specifications at bytecode level, we assume this desugaring has been applied, i.e., all specifications are flat (thus, this desugaring has to be implemented by a compiler from JML to BML specifications, see JML to BML Compiler).
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.