Previous: Class and Interface Behaviour, Up: Class and Interface Specifications

4.5 Method Specifications

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 the 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: 

     spec-header
     {|
         GenSpecCase1
       also
          ...
       also
         GenSpecCasen
     |}

where GenSpecCase can be a nested specification again. Fortunately, there is a simple desugaring for such specifications into a sequence of flat specification cases: 

     spec-header
     GenSpecCase1
     also
     ...
     also
     spec-header
     GenSpecCasen

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.