Next: Annotation (of) Statements, Previous: Class and Interface Specifications, Up: Top
BML predicates are written as source level Java/JML expressions. Since
we know that the expression grammar is only used to write
specification expressions, all expressions that are sure to have
side-effects are removed from the grammar. Notice that this means that
in BML, one is unable to write a predicate like: (x++)-- ==
24. However, since we do not want to exclude method calls from the
expression grammar, BML tools (and in particular the type checker, see
Type Checking BML) still have to check explicitly that all
predicates are side-effect-free, i.e., all methods used in
specifications are annotated pure.