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 still have to check explicitly that all
predicates are side-effect-free.