Next: , Previous: Class and Interface Specifications, Up: Top

5 Predicates and Specification Expressions

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.